Theorem: RuesN4EqualsCoshCosh (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
z : ℂ
⊢ Rues 4 z = (z / (1 + I)).cosh * (z / (1 - I)).cosh
Tactic:
rw [RuesNEqualsExpSum, Complex.cosh, Complex.cosh]
State after:
z : ℂ
⊢ (∑ m ∈ range ↑4, cexp (z * cexp (2 * ↑π * (↑m / ↑↑4) * I))) / ↑↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)

State before:
z : ℂ
⊢ (∑ m ∈ range ↑4, cexp (z * cexp (2 * ↑π * (↑m / ↑↑4) * I))) / ↑↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)
Tactic:
have h₀ : (4 : ℕ+) = (4 : ℕ) := by
  rfl
State after:
z : ℂ
h₀ : ↑4 = 4
⊢ (∑ m ∈ range ↑4, cexp (z * cexp (2 * ↑π * (↑m / ↑↑4) * I))) / ↑↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)

State before:
z : ℂ
h₀ : ↑4 = 4
⊢ (∑ m ∈ range ↑4, cexp (z * cexp (2 * ↑π * (↑m / ↑↑4) * I))) / ↑↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)
Tactic:
simp_rw [h₀, Finset.sum]
State after:
z : ℂ
h₀ : ↑4 = 4
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑4) * I))) (range 4).val).sum / ↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)

State before:
z : ℂ
h₀ : ↑4 = 4
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑4) * I))) (range 4).val).sum / ↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)
Tactic:
clear h₀
State after:
z : ℂ
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑4) * I))) (range 4).val).sum / ↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)

State before:
z : ℂ
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑4) * I))) (range 4).val).sum / ↑4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)
Tactic:
simp only [range_val, Multiset.range_succ, Multiset.range_zero, Multiset.cons_zero,
  Nat.cast_ofNat, Multiset.map_cons, Nat.cast_one, one_div, Multiset.map_singleton,
  CharP.cast_eq_zero, zero_div, mul_zero, zero_mul, Complex.exp_zero, mul_one, Multiset.sum_cons,
  Multiset.sum_singleton]
State after:
z : ℂ
⊢ (cexp (z * cexp (2 * ↑π * (3 / 4) * I)) +
        (cexp (z * cexp (2 * ↑π * (2 / 4) * I)) + (cexp (z * cexp (2 * ↑π * 4⁻¹ * I)) + cexp z))) /
      4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)

State before:
z : ℂ
⊢ (cexp (z * cexp (2 * ↑π * (3 / 4) * I)) +
        (cexp (z * cexp (2 * ↑π * (2 / 4) * I)) + (cexp (z * cexp (2 * ↑π * 4⁻¹ * I)) + cexp z))) /
      4 =
    (cexp (z / (1 + I)) + cexp (-(z / (1 + I)))) / 2 * ((cexp (z / (1 - I)) + cexp (-(z / (1 - I)))) / 2)
Tactic:
ring_nf
State after:
z : ℂ
⊢ cexp (z * cexp (↑π * I * (3 / 2))) * (1 / 4) + cexp (z * cexp (↑π * I)) * (1 / 4) +
        cexp (z * cexp (↑π * I * (1 / 2))) * (1 / 4) +
      cexp z * (1 / 4) =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * (1 / 4) + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * (1 / 4) +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * (1 / 4) +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * (1 / 4)

State before:
z : ℂ
⊢ cexp (z * cexp (↑π * I * (3 / 2))) * (1 / 4) + cexp (z * cexp (↑π * I)) * (1 / 4) +
        cexp (z * cexp (↑π * I * (1 / 2))) * (1 / 4) +
      cexp z * (1 / 4) =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * (1 / 4) + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * (1 / 4) +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * (1 / 4) +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * (1 / 4)
Tactic:
simp only [one_div, exp_pi_mul_I, mul_neg, mul_one]
State after:
z : ℂ
⊢ cexp (z * cexp (↑π * I * (3 / 2))) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
⊢ cexp (z * cexp (↑π * I * (3 / 2))) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
have h₁ : cexp (↑π * I * (3 / 2)) = -I := by
  have h₁b := ExpToNatPowersOfI 3
  simp only [Nat.cast_ofNat] at h₁b
  have h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2) := by
    ring
  rw [h₁b₁] at h₁b
  rw [h₁b]
  clear h₁b h₁b₁
  have h₅ : I ^ (3 : ℕ) = I ^ (3 : ℤ) := by
    exact rfl
  rw [h₅]
  clear h₅
  have h₆ : (3 : ℤ) = 2 + 1 := by
    exact rfl
  rw [h₆]
  clear h₆
  rw [zpow_add₀ I_ne_zero]
  have h₇ : (2 : ℤ) = 1 + 1 := by
    exact rfl
  rw [h₇]
  clear h₇
  rw [zpow_add₀ I_ne_zero]
  simp only [zpow_one, I_mul_I, neg_mul, one_mul]
State after:
z : ℂ
h₁ : cexp (↑π * I * (3 / 2)) = -I
⊢ cexp (z * cexp (↑π * I * (3 / 2))) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₁ : cexp (↑π * I * (3 / 2)) = -I
⊢ cexp (z * cexp (↑π * I * (3 / 2))) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
rw [h₁]
State after:
z : ℂ
h₁ : cexp (↑π * I * (3 / 2)) = -I
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₁ : cexp (↑π * I * (3 / 2)) = -I
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
clear h₁
State after:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
have h₂ : cexp (↑π * I * 2⁻¹) = I := by
  nth_rw 2 [←ExpPiMulIHalf]
  congr 1
  simp only [ofReal_div, ofReal_ofNat]
  ring_nf
State after:
z : ℂ
h₂ : cexp (↑π * I * 2⁻¹) = I
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₂ : cexp (↑π * I * 2⁻¹) = I
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * cexp (↑π * I * 2⁻¹)) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
rw [h₂]
State after:
z : ℂ
h₂ : cexp (↑π * I * 2⁻¹) = I
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₂ : cexp (↑π * I * 2⁻¹) = I
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
clear h₂
State after:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
have h₃ : (1 + I)⁻¹ = (1 - I) / 2 := by
  rw [Inv.inv, Complex.instInv, normSq]
  simp only [MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, ofReal_inv, ofReal_add, ofReal_mul,
    map_add, map_one, conj_I, add_re, one_re, I_re, add_zero, ofReal_one, mul_one, add_im, one_im,
    I_im, zero_add]
  ring_nf
State after:
z : ℂ
h₃ : (1 + I)⁻¹ = (1 - I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₃ : (1 + I)⁻¹ = (1 - I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * (1 + I)⁻¹) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * (1 + I)⁻¹) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * (1 + I)⁻¹)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * (1 + I)⁻¹)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
rw [h₃]
State after:
z : ℂ
h₃ : (1 + I)⁻¹ = (1 - I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * ((1 - I) / 2)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₃ : (1 + I)⁻¹ = (1 - I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * ((1 - I) / 2)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
clear h₃
State after:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * ((1 - I) / 2)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * ((1 - I) / 2)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
have h₄ : (1 - I)⁻¹ = (1 + I) / 2 := by
  rw [Inv.inv, Complex.instInv, normSq]
  simp only [MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, ofReal_inv, ofReal_add, ofReal_mul,
    map_sub, map_one, conj_I, sub_neg_eq_add, sub_re, one_re, I_re, sub_zero, ofReal_one, mul_one,
    sub_im, one_im, I_im, zero_sub, ofReal_neg, mul_neg, neg_neg]
  ring_nf
State after:
z : ℂ
h₄ : (1 - I)⁻¹ = (1 + I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * ((1 - I) / 2)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹

State before:
z : ℂ
h₄ : (1 - I)⁻¹ = (1 + I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * (1 - I)⁻¹) * 4⁻¹ + cexp (z * ((1 - I) / 2)) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * (1 - I)⁻¹) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * (1 - I)⁻¹)) * 4⁻¹
Tactic:
rw [h₄]
State after:
z : ℂ
h₄ : (1 - I)⁻¹ = (1 + I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
          cexp (z * ((1 - I) / 2)) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹

State before:
z : ℂ
h₄ : (1 - I)⁻¹ = (1 + I) / 2
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
          cexp (z * ((1 - I) / 2)) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹
Tactic:
clear h₄
State after:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
          cexp (z * ((1 - I) / 2)) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹

State before:
z : ℂ
⊢ cexp (z * -I) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * ((1 - I) / 2)) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
          cexp (z * ((1 - I) / 2)) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹ +
        cexp (-(z * ((1 - I) / 2))) * cexp (z * ((1 + I) / 2)) * 4⁻¹ +
      cexp (-(z * ((1 - I) / 2))) * cexp (-(z * ((1 + I) / 2))) * 4⁻¹
Tactic:
ring_nf
State after:
z : ℂ
⊢ cexp (-(z * I)) * (1 / 4) + cexp (-z) * (1 / 4) + cexp (z * I) * (1 / 4) + cexp z * (1 / 4) =
    cexp (z * (1 / 2) + z * I * (-1 / 2)) * cexp (z * (1 / 2) + z * I * (1 / 2)) * (1 / 4) +
          cexp (z * (1 / 2) + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * (-1 / 2)) * (1 / 4) +
        cexp (z * (1 / 2) + z * I * (1 / 2)) * cexp (z * (-1 / 2) + z * I * (1 / 2)) * (1 / 4) +
      cexp (z * (-1 / 2) + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * (1 / 2)) * (1 / 4)

State before:
z : ℂ
⊢ cexp (-(z * I)) * (1 / 4) + cexp (-z) * (1 / 4) + cexp (z * I) * (1 / 4) + cexp z * (1 / 4) =
    cexp (z * (1 / 2) + z * I * (-1 / 2)) * cexp (z * (1 / 2) + z * I * (1 / 2)) * (1 / 4) +
          cexp (z * (1 / 2) + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * (-1 / 2)) * (1 / 4) +
        cexp (z * (1 / 2) + z * I * (1 / 2)) * cexp (z * (-1 / 2) + z * I * (1 / 2)) * (1 / 4) +
      cexp (z * (-1 / 2) + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * (1 / 2)) * (1 / 4)
Tactic:
simp only [Int.ofNat_eq_coe, Nat.cast_one, Int.cast_one, Nat.cast_ofNat, one_div,
  Int.cast_negOfNat, mul_neg, mul_one, neg_mul]
State after:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹ + z * I * (-1 / 2)) * cexp (z * 2⁻¹ + z * I * 2⁻¹) * 4⁻¹ +
          cexp (z * 2⁻¹ + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * (-1 / 2)) * 4⁻¹ +
        cexp (z * 2⁻¹ + z * I * 2⁻¹) * cexp (z * (-1 / 2) + z * I * 2⁻¹) * 4⁻¹ +
      cexp (z * (-1 / 2) + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * 2⁻¹) * 4⁻¹

State before:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹ + z * I * (-1 / 2)) * cexp (z * 2⁻¹ + z * I * 2⁻¹) * 4⁻¹ +
          cexp (z * 2⁻¹ + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * (-1 / 2)) * 4⁻¹ +
        cexp (z * 2⁻¹ + z * I * 2⁻¹) * cexp (z * (-1 / 2) + z * I * 2⁻¹) * 4⁻¹ +
      cexp (z * (-1 / 2) + z * I * (-1 / 2)) * cexp (z * (-1 / 2) + z * I * 2⁻¹) * 4⁻¹
Tactic:
simp_rw [Complex.exp_add]
State after:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹) * cexp (z * I * (-1 / 2)) * (cexp (z * 2⁻¹) * cexp (z * I * 2⁻¹)) * 4⁻¹ +
          cexp (z * 2⁻¹) * cexp (z * I * (-1 / 2)) * (cexp (z * (-1 / 2)) * cexp (z * I * (-1 / 2))) * 4⁻¹ +
        cexp (z * 2⁻¹) * cexp (z * I * 2⁻¹) * (cexp (z * (-1 / 2)) * cexp (z * I * 2⁻¹)) * 4⁻¹ +
      cexp (z * (-1 / 2)) * cexp (z * I * (-1 / 2)) * (cexp (z * (-1 / 2)) * cexp (z * I * 2⁻¹)) * 4⁻¹

State before:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹) * cexp (z * I * (-1 / 2)) * (cexp (z * 2⁻¹) * cexp (z * I * 2⁻¹)) * 4⁻¹ +
          cexp (z * 2⁻¹) * cexp (z * I * (-1 / 2)) * (cexp (z * (-1 / 2)) * cexp (z * I * (-1 / 2))) * 4⁻¹ +
        cexp (z * 2⁻¹) * cexp (z * I * 2⁻¹) * (cexp (z * (-1 / 2)) * cexp (z * I * 2⁻¹)) * 4⁻¹ +
      cexp (z * (-1 / 2)) * cexp (z * I * (-1 / 2)) * (cexp (z * (-1 / 2)) * cexp (z * I * 2⁻¹)) * 4⁻¹
Tactic:
ring_nf
State after:
z : ℂ
⊢ cexp (-(z * I)) * (1 / 4) + cexp (-z) * (1 / 4) + cexp (z * I) * (1 / 4) + cexp z * (1 / 4) =
    cexp (z * (1 / 2)) * cexp (z * I * (-1 / 2)) ^ 2 * cexp (z * (-1 / 2)) * (1 / 4) +
          cexp (z * (1 / 2)) * cexp (z * I * (1 / 2)) ^ 2 * cexp (z * (-1 / 2)) * (1 / 4) +
        cexp (z * (1 / 2)) ^ 2 * cexp (z * I * (-1 / 2)) * cexp (z * I * (1 / 2)) * (1 / 4) +
      cexp (z * I * (-1 / 2)) * cexp (z * I * (1 / 2)) * cexp (z * (-1 / 2)) ^ 2 * (1 / 4)

State before:
z : ℂ
⊢ cexp (-(z * I)) * (1 / 4) + cexp (-z) * (1 / 4) + cexp (z * I) * (1 / 4) + cexp z * (1 / 4) =
    cexp (z * (1 / 2)) * cexp (z * I * (-1 / 2)) ^ 2 * cexp (z * (-1 / 2)) * (1 / 4) +
          cexp (z * (1 / 2)) * cexp (z * I * (1 / 2)) ^ 2 * cexp (z * (-1 / 2)) * (1 / 4) +
        cexp (z * (1 / 2)) ^ 2 * cexp (z * I * (-1 / 2)) * cexp (z * I * (1 / 2)) * (1 / 4) +
      cexp (z * I * (-1 / 2)) * cexp (z * I * (1 / 2)) * cexp (z * (-1 / 2)) ^ 2 * (1 / 4)
Tactic:
simp only [Int.ofNat_eq_coe, Nat.cast_one, Int.cast_one, Nat.cast_ofNat, one_div,
  Int.cast_negOfNat, mul_neg, mul_one, neg_mul]
State after:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹) * cexp (z * I * (-1 / 2)) ^ 2 * cexp (z * (-1 / 2)) * 4⁻¹ +
          cexp (z * 2⁻¹) * cexp (z * I * 2⁻¹) ^ 2 * cexp (z * (-1 / 2)) * 4⁻¹ +
        cexp (z * 2⁻¹) ^ 2 * cexp (z * I * (-1 / 2)) * cexp (z * I * 2⁻¹) * 4⁻¹ +
      cexp (z * I * (-1 / 2)) * cexp (z * I * 2⁻¹) * cexp (z * (-1 / 2)) ^ 2 * 4⁻¹

State before:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹) * cexp (z * I * (-1 / 2)) ^ 2 * cexp (z * (-1 / 2)) * 4⁻¹ +
          cexp (z * 2⁻¹) * cexp (z * I * 2⁻¹) ^ 2 * cexp (z * (-1 / 2)) * 4⁻¹ +
        cexp (z * 2⁻¹) ^ 2 * cexp (z * I * (-1 / 2)) * cexp (z * I * 2⁻¹) * 4⁻¹ +
      cexp (z * I * (-1 / 2)) * cexp (z * I * 2⁻¹) * cexp (z * (-1 / 2)) ^ 2 * 4⁻¹
Tactic:
simp_rw [←Complex.exp_nat_mul, ←Complex.exp_add]
State after:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹ + ↑2 * (z * I * (-1 / 2)) + z * (-1 / 2)) * 4⁻¹ +
          cexp (z * 2⁻¹ + ↑2 * (z * I * 2⁻¹) + z * (-1 / 2)) * 4⁻¹ +
        cexp (↑2 * (z * 2⁻¹) + z * I * (-1 / 2) + z * I * 2⁻¹) * 4⁻¹ +
      cexp (z * I * (-1 / 2) + z * I * 2⁻¹ + ↑2 * (z * (-1 / 2))) * 4⁻¹

State before:
z : ℂ
⊢ cexp (-(z * I)) * 4⁻¹ + cexp (-z) * 4⁻¹ + cexp (z * I) * 4⁻¹ + cexp z * 4⁻¹ =
    cexp (z * 2⁻¹ + ↑2 * (z * I * (-1 / 2)) + z * (-1 / 2)) * 4⁻¹ +
          cexp (z * 2⁻¹ + ↑2 * (z * I * 2⁻¹) + z * (-1 / 2)) * 4⁻¹ +
        cexp (↑2 * (z * 2⁻¹) + z * I * (-1 / 2) + z * I * 2⁻¹) * 4⁻¹ +
      cexp (z * I * (-1 / 2) + z * I * 2⁻¹ + ↑2 * (z * (-1 / 2))) * 4⁻¹
Tactic:
ring_nf
State after:
no goals

State before:
z : ℂ
⊢ ↑4 = 4
Tactic:
rfl
State after:
no goals

State before:
z : ℂ
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
have h₁b := ExpToNatPowersOfI 3
State after:
z : ℂ
h₁b : cexp (↑π * I * ↑3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I

State before:
z : ℂ
h₁b : cexp (↑π * I * ↑3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
simp only [Nat.cast_ofNat] at h₁b
State after:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I

State before:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
have h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2) := by
  ring
State after:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I

State before:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
rw [h₁b₁] at h₁b
State after:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I

State before:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
rw [h₁b]
State after:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ I ^ 3 = -I

State before:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ I ^ 3 = -I
Tactic:
clear h₁b h₁b₁
State after:
z : ℂ
⊢ I ^ 3 = -I

State before:
z : ℂ
⊢ I ^ 3 = -I
Tactic:
have h₅ : I ^ (3 : ℕ) = I ^ (3 : ℤ) := by
  exact rfl
State after:
z : ℂ
h₅ : I ^ 3 = I ^ 3
⊢ I ^ 3 = -I

State before:
z : ℂ
h₅ : I ^ 3 = I ^ 3
⊢ I ^ 3 = -I
Tactic:
clear h₅
State after:
z : ℂ
⊢ I ^ 3 = -I

State before:
z : ℂ
⊢ I ^ 3 = -I
Tactic:
have h₆ : (3 : ℤ) = 2 + 1 := by
  exact rfl
State after:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ 3 = -I

State before:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ 3 = -I
Tactic:
rw [h₆]
State after:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ (2 + 1) = -I

State before:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ (2 + 1) = -I
Tactic:
clear h₆
State after:
z : ℂ
⊢ I ^ (2 + 1) = -I

State before:
z : ℂ
⊢ I ^ (2 + 1) = -I
Tactic:
rw [zpow_add₀ I_ne_zero]
State after:
z : ℂ
⊢ I ^ 2 * I ^ 1 = -I

State before:
z : ℂ
⊢ I ^ 2 * I ^ 1 = -I
Tactic:
have h₇ : (2 : ℤ) = 1 + 1 := by
  exact rfl
State after:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ 2 * I ^ 1 = -I

State before:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ 2 * I ^ 1 = -I
Tactic:
rw [h₇]
State after:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ (1 + 1) * I ^ 1 = -I

State before:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ (1 + 1) * I ^ 1 = -I
Tactic:
clear h₇
State after:
z : ℂ
⊢ I ^ (1 + 1) * I ^ 1 = -I

State before:
z : ℂ
⊢ I ^ (1 + 1) * I ^ 1 = -I
Tactic:
rw [zpow_add₀ I_ne_zero]
State after:
z : ℂ
⊢ I ^ 1 * I ^ 1 * I ^ 1 = -I

State before:
z : ℂ
⊢ I ^ 1 * I ^ 1 * I ^ 1 = -I
Tactic:
simp only [zpow_one, I_mul_I, neg_mul, one_mul]
State after:
no goals

State before:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
⊢ ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
Tactic:
ring
State after:
no goals

State before:
z : ℂ
⊢ I ^ 3 = I ^ 3
Tactic:
exact rfl
State after:
no goals

State before:
z : ℂ
⊢ 3 = 2 + 1
Tactic:
exact rfl
State after:
no goals

State before:
z : ℂ
⊢ 2 = 1 + 1
Tactic:
exact rfl
State after:
no goals

State before:
z : ℂ
⊢ cexp (↑π * I * 2⁻¹) = I
Tactic:
nth_rw 2 [←ExpPiMulIHalf]
State after:
z : ℂ
⊢ cexp (↑π * I * 2⁻¹) = cexp (↑(π / 2) * I)

State before:
z : ℂ
⊢ cexp (↑π * I * 2⁻¹) = cexp (↑(π / 2) * I)
Tactic:
congr 1
State after:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑(π / 2) * I

State before:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑(π / 2) * I
Tactic:
simp only [ofReal_div, ofReal_ofNat]
State after:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑π / 2 * I

State before:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑π / 2 * I
Tactic:
ring_nf
State after:
no goals

State before:
z : ℂ
⊢ (1 + I)⁻¹ = (1 - I) / 2
Tactic:
rw [Inv.inv, Complex.instInv, normSq]
State after:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 + I) =
    (1 - I) / 2

State before:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 + I) =
    (1 - I) / 2
Tactic:
simp only [MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, ofReal_inv, ofReal_add, ofReal_mul,
  map_add, map_one, conj_I, add_re, one_re, I_re, add_zero, ofReal_one, mul_one, add_im, one_im,
  I_im, zero_add]
State after:
z : ℂ
⊢ (1 + -I) * (1 + 1)⁻¹ = (1 - I) / 2

State before:
z : ℂ
⊢ (1 + -I) * (1 + 1)⁻¹ = (1 - I) / 2
Tactic:
ring_nf
State after:
no goals

State before:
z : ℂ
⊢ (1 - I)⁻¹ = (1 + I) / 2
Tactic:
rw [Inv.inv, Complex.instInv, normSq]
State after:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 - I) =
    (1 + I) / 2

State before:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 - I) =
    (1 + I) / 2
Tactic:
simp only [MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, ofReal_inv, ofReal_add, ofReal_mul,
  map_sub, map_one, conj_I, sub_neg_eq_add, sub_re, one_re, I_re, sub_zero, ofReal_one, mul_one,
  sub_im, one_im, I_im, zero_sub, ofReal_neg, mul_neg, neg_neg]
State after:
z : ℂ
⊢ (1 + I) * (1 + 1)⁻¹ = (1 + I) / 2

State before:
z : ℂ
⊢ (1 + I) * (1 + 1)⁻¹ = (1 + I) / 2
Tactic:
ring_nf
State after:
no goals