2.1. Complex conjugate🔗

Definition 1.3.1. The complex conjugate of a complex number z = a + bi is defined as z^* = a - bi.

Define the notation conj as the star operator in complex numbers. This is already defined in Mathlib as starRingEnd ℂ.

notation "conj" => (starRingEnd ℂ)

Proposition 1.3.2. For complex numbers z\in \mathbb{C}:

(a): (z^*)^* = z.
(b): z^* = z if and only if z is real.
(c): z^* = -z if and only if z is purely imaginary.

/-- Prop. 1.3.2 part (a)
  Complex conjugate is an involution
-/
example {z : ℂ} : conj (conj z) = z := byz:ℂ⊢ (starRingEnd ℂ) ((starRingEnd ℂ) z) = z
-- Use extensionality on real and imaginary parts
  apply Complex.extaz:ℂ⊢ ((starRingEnd ℂ) ((starRingEnd ℂ) z)).re = z.reaz:ℂ⊢ ((starRingEnd ℂ) ((starRingEnd ℂ) z)).im = z.im
  ·az:ℂ⊢ ((starRingEnd ℂ) ((starRingEnd ℂ) z)).re = z.re -- real parts are equal
    simpAll goals completed! 🐙
  ·az:ℂ⊢ ((starRingEnd ℂ) ((starRingEnd ℂ) z)).im = z.im -- imaginary parts are equal
    simpAll goals completed! 🐙

example {z : ℂ} : conj (conj z) = z := byz:ℂ⊢ (starRingEnd ℂ) ((starRingEnd ℂ) z) = z
  -- prove using an existing theorem in Mathlib
  exact Complex.conj_conj zAll goals completed! 🐙

/-- Prop. 1.3.2 part (b)
    z* = z if and only if imag(z) = 0
-/
example (z : ℂ) : conj z = z ↔ z.im = 0 := byz:ℂ⊢ (starRingEnd ℂ) z = z ↔ z.im = 0
  constructormpz:ℂ⊢ (starRingEnd ℂ) z = z → z.im = 0mprz:ℂ⊢ z.im = 0 → (starRingEnd ℂ) z = z
  ·mpz:ℂ⊢ (starRingEnd ℂ) z = z → z.im = 0 -- conj z = z → z.im = 0
    intro hmpz:ℂh:(starRingEnd ℂ) z = z⊢ z.im = 0
    -- Two complex numbers are equal
    --   iff their corresponding  components are equal
    rw [Complex.ext_iff] at hmpz:ℂh:((starRingEnd ℂ) z).re = z.re ∧ ((starRingEnd ℂ) z).im = z.im⊢ z.im = 0
    -- Break h into real (h_re) and imaginary (h_im) parts
    obtain ⟨h_re, h_im⟩ := hmpz:ℂh_re:((starRingEnd ℂ) z).re = z.reh_im:((starRingEnd ℂ) z).im = z.im⊢ z.im = 0
    -- Simplify (conj z).im to -z.im
    simp at h_immpz:ℂh_re:((starRingEnd ℂ) z).re = z.reh_im:-z.im = z.im⊢ z.im = 0
    -- We now have -z.im = z.im. Arithmetic solves this.
    linarithAll goals completed! 🐙
  ·mprz:ℂ⊢ z.im = 0 → (starRingEnd ℂ) z = z -- z.im = 0 → conj z = z
    intro hmprz:ℂh:z.im = 0⊢ (starRingEnd ℂ) z = z
    -- To prove two complex numbers are equal,
    -- check components and use the hypothesis that Im(z)=0
    simp [Complex.ext_iff, h]All goals completed! 🐙

Complex.conj_eq_iff_im {z : ℂ} : (starRingEnd ℂ) z = z ↔ z.im = 0#check conj_eq_iff_im
  -- This is the same as the second part of Prop. 1.3.2

Compare with Mathlib's conj_eq_iff_im

/-- Prop. 1.3.2. part (c)
    z* = -z if and only if real(z) = 0
-/
example (z : ℂ) : conj z = -z ↔ z.re = 0 := byz:ℂ⊢ (starRingEnd ℂ) z = -z ↔ z.re = 0
  constructormpz:ℂ⊢ (starRingEnd ℂ) z = -z → z.re = 0mprz:ℂ⊢ z.re = 0 → (starRingEnd ℂ) z = -z
  ·mpz:ℂ⊢ (starRingEnd ℂ) z = -z → z.re = 0 -- conj z = -z → z.re = 0
    intro hmpz:ℂh:(starRingEnd ℂ) z = -z⊢ z.re = 0
    -- Two complex numbers are equal
    -- iff their components are equal
    rw [Complex.ext_iff] at hmpz:ℂh:((starRingEnd ℂ) z).re = (-z).re ∧ ((starRingEnd ℂ) z).im = (-z).im⊢ z.re = 0
    -- Break h into real (h_re) and imaginary (h_im) parts
    obtain ⟨h_re, h_im⟩ := hmpz:ℂh_re:((starRingEnd ℂ) z).re = (-z).reh_im:((starRingEnd ℂ) z).im = (-z).im⊢ z.re = 0
    -- Simplify (conj z).re to -z.re
    simp at h_rempz:ℂh_re:z.re = -z.reh_im:((starRingEnd ℂ) z).im = (-z).im⊢ z.re = 0
    -- We now have z.re = -z.re
    linarithAll goals completed! 🐙
  ·mprz:ℂ⊢ z.re = 0 → (starRingEnd ℂ) z = -z -- z.re = 0 → conj z = -z
    intro hmprz:ℂh:z.re = 0⊢ (starRingEnd ℂ) z = -z
    -- To prove two complex numbers are equal,
    -- we check the real and imaginary parts,
    -- and use the hypothesis that real(z)=0
    simp [Complex.ext_iff, h]All goals completed! 🐙

Complex conjugate is an automorphism of the complex field. Addition, multiplication, and inversion are preserved by complex conjugation.

Theorem 1.3.3.

(a): (z_1 + z_2)^* = z_1^* + z_2^*, for z_1, z_2\in\mathbb{C},
(b): (z_1 z_2)^* = z_1^* z_2^*, for z_1, z_2\in\mathbb{C},
(c): (1/z)^* = 1/(z^*) for z\neq 0.

/--
Theorem 1.3.3 part (a)
  (z_1 + z_2)^* = z_1^* + z_2^*
-/
theorem conj_add_conj (z₁ z₂ : ℂ) :
  conj z₁ + conj z₂ = conj (z₁ + z₂) := byz₁:ℂz₂:ℂ⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ + z₂)
  -- define a, b, c, d
  let a := z₁.rez₁:ℂz₂:ℂa:ℝ := z₁.re⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ + z₂); let b := z₁.imz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.im⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ + z₂)
  let c := z₂.rez₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.re⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ + z₂); let d := z₂.imz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ + z₂)

  calc
    -- repalce z₁ and z₂ by their definitions
    -- (a + bi) and (c + di)
    conj z₁ + conj z₂
    -- Apply conjugate definition: (a - bi) + (c - di)
    _ = Complex.mk a (-b) + Complex.mk c (-d) := byz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = { re := a, im := -b } + { re := c, im := -d } rflAll goals completed! 🐙
    -- Group real and imaginary parts: (a + c) - i(b + d)
    _ = Complex.mk (a + c) (-(b + d)) := byz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ { re := a, im := -b } + { re := c, im := -d } = { re := a + c, im := -(b + d) }
       ring_nfz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ { re := a, im := -b } + { re := c, im := -d } = { re := a + c, im := -b - d }
       rflAll goals completed! 🐙
    -- By definition, it equals conj (z₁+z₂)
    _ = conj (z₁ + z₂) := byz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ { re := a + c, im := -(b + d) } = (starRingEnd ℂ) (z₁ + z₂) rflAll goals completed! 🐙

/-- Theorem 1.3.3 part (b)
  (z_1 z_2)^* = z_1^* z_2^*
-/
theorem conj_mul_conj (z₁ z₂ : ℂ) :
  conj z₁ * conj z₂ = conj (z₁ * z₂) := byz₁:ℂz₂:ℂ⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ * z₂)
  -- define a,b,c,d
  let a := z₁.rez₁:ℂz₂:ℂa:ℝ := z₁.re⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ * z₂); let b := z₁.imz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.im⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ * z₂)
  let c := z₂.rez₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.re⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ * z₂); let d := z₂.imz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ * z₂)

  calc
    -- Expand z₁ and z₂
    conj z₁ * conj z₂
    -- Apply conjugate definition
    _ = Complex.mk a (-b) * Complex.mk c (-d) := byz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = { re := a, im := -b } * { re := c, im := -d } rflAll goals completed! 🐙
    -- Perform complex multiplication. Use extensionality
    -- to split into real and imaginary goals
    _ = Complex.mk (a * c - b * d) (-(a * d + b * c)) := byz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ { re := a, im := -b } * { re := c, im := -d } = { re := a * c - b * d, im := -(a * d + b * c) }
         apply Complex.extaz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ ({ re := a, im := -b } * { re := c, im := -d }).re = { re := a * c - b * d, im := -(a * d + b * c) }.reaz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ ({ re := a, im := -b } * { re := c, im := -d }).im = { re := a * c - b * d, im := -(a * d + b * c) }.im
         ·az₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ ({ re := a, im := -b } * { re := c, im := -d }).re = { re := a * c - b * d, im := -(a * d + b * c) }.re simpAll goals completed! 🐙
         ·az₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ ({ re := a, im := -b } * { re := c, im := -d }).im = { re := a * c - b * d, im := -(a * d + b * c) }.im simpaz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ -(a * d) + -(b * c) = -(b * c) + -(a * d)
           ringAll goals completed! 🐙
    -- The rest is true by definition
    _ = conj (z₁ * z₂)  := byz₁:ℂz₂:ℂa:ℝ := z₁.reb:ℝ := z₁.imc:ℝ := z₂.red:ℝ := z₂.im⊢ { re := a * c - b * d, im := -(a * d + b * c) } = (starRingEnd ℂ) (z₁ * z₂) rflAll goals completed! 🐙


/-- Theorem 1.3.3 part (c)
   conj z⁻¹ = (conj z)⁻¹
-/
example (z : ℂ) (hz : z ≠ 0) : conj z⁻¹ = (conj z)⁻¹ := byz:ℂhz:z ≠ 0⊢ (starRingEnd ℂ) z⁻¹ = ((starRingEnd ℂ) z)⁻¹
  symmz:ℂhz:z ≠ 0⊢ ((starRingEnd ℂ) z)⁻¹ = (starRingEnd ℂ) z⁻¹
  apply inv_eq_of_mul_eq_one_rightaz:ℂhz:z ≠ 0⊢ (starRingEnd ℂ) z * (starRingEnd ℂ) z⁻¹ = 1

  -- Now we perform the calculation: z*(1/z) = ... = 1
  calc
    conj z * conj z⁻¹
    -- Combine conjugates: (1/z)* z* = ((1/z)z)*
    _ = conj (z*z⁻¹) := byz:ℂhz:z ≠ 0⊢ (starRingEnd ℂ) z * (starRingEnd ℂ) z⁻¹ = (starRingEnd ℂ) (z * z⁻¹) rw [← map_mul]All goals completed! 🐙

    -- Simplify z(1/z) to 1
    _ = conj 1         := byz:ℂhz:z ≠ 0⊢ (starRingEnd ℂ) (z * z⁻¹) = (starRingEnd ℂ) 1 rw [Complex.mul_inv_cancel hz]All goals completed! 🐙

    -- Conjugate of 1 is 1
    _ = 1         := byz:ℂhz:z ≠ 0⊢ (starRingEnd ℂ) 1 = 1 rw [map_one]All goals completed! 🐙

Existing Mathlib theorems proving complex conjugate is an automorphism of the complex field. We can use these to give a more concise proof of the above theorems.

/-- Prove by applying existing theorems in Mathlib -/
example (z₁ z₂ : ℂ) : conj z₁ + conj z₂ = conj (z₁ + z₂) :=
  byz₁:ℂz₂:ℂ⊢ (starRingEnd ℂ) z₁ + (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ + z₂) exact Eq.symm (RingHom.map_add (starRingEnd ℂ) z₁ z₂)All goals completed! 🐙

example (z₁ z₂ : ℂ) : conj z₁ * conj z₂ = conj (z₁ * z₂) :=
  byz₁:ℂz₂:ℂ⊢ (starRingEnd ℂ) z₁ * (starRingEnd ℂ) z₂ = (starRingEnd ℂ) (z₁ * z₂) exact Eq.symm (RingHom.map_mul (starRingEnd ℂ) z₁ z₂)All goals completed! 🐙

example (z : ℂ) : conj z⁻¹ = (conj z)⁻¹ := byz:ℂ⊢ (starRingEnd ℂ) z⁻¹ = ((starRingEnd ℂ) z)⁻¹
  exact Complex.conj_inv zAll goals completed! 🐙

The next proposition justifies that the product of a complex number and its complex conjugate is a real number. (This is the notion of norm in from algebraic number theory.) It also illustrates how to recover the real and imaginary parts of a complex number using the complex conjugate.

Theorem 1.3.4. If z=a+bi for a,b\in\mathbb{R}, then

(a): z z^* = a^2+b^2.
(b): a = \frac{z + z^*}{2} and b = \frac{z - z^*}{2i}.

/-- Theorem 1.3.4, Part (a)
   z z^* = a^2 + b^2
-/
-- a detailed proof by calculation
example (z : ℂ) :
    z * conj z = (z.re)^2 + (z.im)^2 := byz:ℂ⊢ z * (starRingEnd ℂ) z = ↑z.re ^ 2 + ↑z.im ^ 2
  let a := z.rez:ℂa:ℝ := z.re⊢ z * (starRingEnd ℂ) z = ↑z.re ^ 2 + ↑z.im ^ 2; let b := z.imz:ℂa:ℝ := z.reb:ℝ := z.im⊢ z * (starRingEnd ℂ) z = ↑z.re ^ 2 + ↑z.im ^ 2

  calc
    z * conj z
    -- Apply conjugate: (a + bi)(a - bi)
    _ = (Complex.mk a b) * (Complex.mk a (-b))   := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ z * (starRingEnd ℂ) z = { re := a, im := b } * { re := a, im := -b } rflAll goals completed! 🐙

    -- Def. of multiplication: (aa - b(-b)) + i(a(-b) + ba)
    _ = Complex.mk (a * a - b * (-b)) (a * (-b) + b * a)
          := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a, im := b } * { re := a, im := -b } = { re := a * a - b * -b, im := a * -b + b * a } rflAll goals completed! 🐙

    -- Simplify Algebra: a^2 + b^2 + i(0)
    _ = Complex.mk (a ^ 2 + b ^ 2) 0  := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a * a - b * -b, im := a * -b + b * a } = { re := a ^ 2 + b ^ 2, im := 0 }
      congre_rez:ℂa:ℝ := z.reb:ℝ := z.im⊢ a * a - b * -b = a ^ 2 + b ^ 2e_imz:ℂa:ℝ := z.reb:ℝ := z.im⊢ a * -b + b * a = 0
      ·e_rez:ℂa:ℝ := z.reb:ℝ := z.im⊢ a * a - b * -b = a ^ 2 + b ^ 2 ringAll goals completed! 🐙 -- Real part: a*a - (-b^2) = a^2 + b^2
      ·e_imz:ℂa:ℝ := z.reb:ℝ := z.im⊢ a * -b + b * a = 0 ringAll goals completed! 🐙 -- Imaginary part: -ab + ab = 0

    _ = (a ^ 2 + b ^ 2 : ℂ) :=  byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a ^ 2 + b ^ 2, im := 0 } = ↑a ^ 2 + ↑b ^ 2
        apply Complex.extaz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a ^ 2 + b ^ 2, im := 0 }.re = (↑a ^ 2 + ↑b ^ 2).reaz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a ^ 2 + b ^ 2, im := 0 }.im = (↑a ^ 2 + ↑b ^ 2).im
        ·az:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a ^ 2 + b ^ 2, im := 0 }.re = (↑a ^ 2 + ↑b ^ 2).re simpaz:ℂa:ℝ := z.reb:ℝ := z.im⊢ a ^ 2 + b ^ 2 = (↑a ^ 2).re + (↑b ^ 2).re
          rw [← Complex.ofReal_pow a 2]az:ℂa:ℝ := z.reb:ℝ := z.im⊢ a ^ 2 + b ^ 2 = (↑(a ^ 2)).re + (↑b ^ 2).re
          rw[← Complex.ofReal_pow b 2]az:ℂa:ℝ := z.reb:ℝ := z.im⊢ a ^ 2 + b ^ 2 = (↑(a ^ 2)).re + (↑(b ^ 2)).re
          repeat rw [Complex.ofReal_re]All goals completed! 🐙
        ·az:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a ^ 2 + b ^ 2, im := 0 }.im = (↑a ^ 2 + ↑b ^ 2).im simpaz:ℂa:ℝ := z.reb:ℝ := z.im⊢ 0 = (↑a ^ 2).im + (↑b ^ 2).im
          rw [← Complex.ofReal_pow a 2]az:ℂa:ℝ := z.reb:ℝ := z.im⊢ 0 = (↑(a ^ 2)).im + (↑b ^ 2).im
          rw [← Complex.ofReal_pow b 2]az:ℂa:ℝ := z.reb:ℝ := z.im⊢ 0 = (↑(a ^ 2)).im + (↑(b ^ 2)).im
          repeat rw [ofReal_im]az:ℂa:ℝ := z.reb:ℝ := z.im⊢ 0 = 0 + 0
          ringAll goals completed! 🐙

We can also prove the same result using the existing theorem mul_conj in Mathlib.

Complex.mul_conj (z : ℂ) : z * (starRingEnd ℂ) z = ↑(normSq z)#check mul_conj  -- This states that z * conj z = normSq z,
                 -- where normSq z = z.re^2 + z.im^2

example (z : ℂ) : z * conj z = (z.re)^2 + (z.im)^2 := byz:ℂ⊢ z * (starRingEnd ℂ) z = ↑z.re ^ 2 + ↑z.im ^ 2
-- proof using `mul_conj`
  rw [Complex.mul_conj]z:ℂ⊢ ↑(normSq z) = ↑z.re ^ 2 + ↑z.im ^ 2
  unfold normSqz:ℂ⊢ ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq._proof_1, map_one' := normSq._proof_2,
        map_mul' := ⋯ }
      z) =
  ↑z.re ^ 2 + ↑z.im ^ 2 ;
  simpz:ℂ⊢ ↑z.re * ↑z.re + ↑z.im * ↑z.im = ↑z.re ^ 2 + ↑z.im ^ 2 ; ringAll goals completed! 🐙

/--
Theorem 1.3.4, Part (b)
  z.re = (z + conj z) / 2
-/
example (z : ℂ) : z.re = (z + conj z) / 2  := byz:ℂ⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2
-- detailed proof by calculation,
-- using the definition of conjugate
  let a := z.rez:ℂa:ℝ := z.re⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2
  let b := z.imz:ℂa:ℝ := z.reb:ℝ := z.im⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2

  symmz:ℂa:ℝ := z.reb:ℝ := z.im⊢ (z + (starRingEnd ℂ) z) / 2 = ↑z.re
  calc
    (z + conj z) / 2
    -- Expand z to Complex.mk a b
    _ = (Complex.mk a b + conj (Complex.mk a b)) / 2
        := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ (z + (starRingEnd ℂ) z) / 2 = ({ re := a, im := b } + (starRingEnd ℂ) { re := a, im := b }) / 2 rflAll goals completed! 🐙

    -- Apply definition of conjugate
    _ = (Complex.mk a b + Complex.mk a (-b)) / 2 := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ ({ re := a, im := b } + (starRingEnd ℂ) { re := a, im := b }) / 2 = ({ re := a, im := b } + { re := a, im := -b }) / 2 rflAll goals completed! 🐙

    -- Perform the addition: (a+a) + i(b-b)
    _ = (Complex.mk (a + a) (b + -b)) / 2        := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ ({ re := a, im := b } + { re := a, im := -b }) / 2 = { re := a + a, im := b + -b } / 2 rflAll goals completed! 🐙

    -- Simplify the numerator: 2a + i0
    _ = (Complex.mk (2 * a) 0) / 2   := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := a + a, im := b + -b } / 2 = { re := 2 * a, im := 0 } / 2
      congr 2e_a.e_rez:ℂa:ℝ := z.reb:ℝ := z.im⊢ a + a = 2 * ae_a.e_imz:ℂa:ℝ := z.reb:ℝ := z.im⊢ b + -b = 0 -- Focus inside the 'mk'
      ·e_a.e_rez:ℂa:ℝ := z.reb:ℝ := z.im⊢ a + a = 2 * a ringAll goals completed! 🐙 -- Real part: a + a = 2 * a
      ·e_a.e_imz:ℂa:ℝ := z.reb:ℝ := z.im⊢ b + -b = 0 ringAll goals completed! 🐙 -- Imaginary part: b + -b = 0

    -- Convert 'mk (2a) 0' to real number '(2a : ℂ)'
    _ = (2 * a : ℂ) / 2    := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ { re := 2 * a, im := 0 } / 2 = 2 * ↑a / 2
        apply Complex.extaz:ℂa:ℝ := z.reb:ℝ := z.im⊢ ({ re := 2 * a, im := 0 } / 2).re = (2 * ↑a / 2).reaz:ℂa:ℝ := z.reb:ℝ := z.im⊢ ({ re := 2 * a, im := 0 } / 2).im = (2 * ↑a / 2).im
        ·az:ℂa:ℝ := z.reb:ℝ := z.im⊢ ({ re := 2 * a, im := 0 } / 2).re = (2 * ↑a / 2).re simpAll goals completed! 🐙
        ·az:ℂa:ℝ := z.reb:ℝ := z.im⊢ ({ re := 2 * a, im := 0 } / 2).im = (2 * ↑a / 2).im simpAll goals completed! 🐙
    _ = a := byz:ℂa:ℝ := z.reb:ℝ := z.im⊢ 2 * ↑a / 2 = ↑a simpAll goals completed! 🐙

An alternate proof using by matching the real and imaginary parts

example (z : ℂ) : z.re = (z + conj z) / 2 := byz:ℂ⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2
-- prove by considering real and imaginary parts
  apply Complex.extaz:ℂ⊢ (↑z.re).re = ((z + (starRingEnd ℂ) z) / 2).reaz:ℂ⊢ (↑z.re).im = ((z + (starRingEnd ℂ) z) / 2).im
  -- Goal 1: Real parts match
  -- LHS: z.re
  -- RHS: ((z + conj z) / 2).re
  ·az:ℂ⊢ (↑z.re).re = ((z + (starRingEnd ℂ) z) / 2).re simpAll goals completed! 🐙
  -- Goal 2: Imaginary parts match
  -- LHS: 0 (since z.re is real)
  -- RHS: ((z + conj z) / 2).im
  ·az:ℂ⊢ (↑z.re).im = ((z + (starRingEnd ℂ) z) / 2).im simpAll goals completed! 🐙

/--
  Theorem 1.3.4, Part (b) z.im = (z - conj z) / (2i)
-/
example (z : ℂ) : z.im = (z - conj z) / (2*I)  := byz:ℂ⊢ ↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)
  symmz:ℂ⊢ (z - (starRingEnd ℂ) z) / (2 * I) = ↑z.im
  -- Multiply both sides by 2*I to avoid fraction headaches
  rw [div_eq_iff]z:ℂ⊢ z - (starRingEnd ℂ) z = ↑z.im * (2 * I)z:ℂ⊢ 2 * I ≠ 0
  -- Use Extensionality to check Real/Imaginary parts
  ·z:ℂ⊢ z - (starRingEnd ℂ) z = ↑z.im * (2 * I) apply Complex.extaz:ℂ⊢ (z - (starRingEnd ℂ) z).re = (↑z.im * (2 * I)).reaz:ℂ⊢ (z - (starRingEnd ℂ) z).im = (↑z.im * (2 * I)).im
    ·az:ℂ⊢ (z - (starRingEnd ℂ) z).re = (↑z.im * (2 * I)).re simpAll goals completed! 🐙 -- Real parts match (0 = 0)
    ·az:ℂ⊢ (z - (starRingEnd ℂ) z).im = (↑z.im * (2 * I)).im simpaz:ℂ⊢ z.im + z.im = z.im * 2
      ringAll goals completed! 🐙
       -- Imaginary parts match (2b = 2b)

  -- Prove denominator non-zero
  ·z:ℂ⊢ 2 * I ≠ 0 simp [I_ne_zero]All goals completed! 🐙

We can also prove the same result using the existing theorems from Mathlib.

example (z : ℂ) : z.re = (z + conj z) / 2  := byz:ℂ⊢ ↑z.re = (z + (starRingEnd ℂ) z) / 2
-- prove using and existing theorem in Mathlib
  exact re_eq_add_conj zAll goals completed! 🐙

example (z : ℂ) : z.im = (z - conj z) / (2*I)  := byz:ℂ⊢ ↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)
-- prove using and existing theorem in Mathlib
  exact im_eq_sub_conj zAll goals completed! 🐙