Theorem: RuesN2EqualsCosh (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
⊢ Rues 2 = Complex.cosh
Tactic:
ext1 z
State after:
case h
z : ℂ
⊢ Rues 2 z = z.cosh

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

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

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

State before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑↑2) * I))) {0, 1}.val).sum / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
simp only [mem_singleton, insert_val, singleton_val, Multiset.mem_singleton, not_false_eq_true,
  Multiset.ndinsert_of_not_mem, Multiset.map_cons, CharP.cast_eq_zero, zero_div, mul_zero,
  zero_mul, Complex.exp_zero, mul_one, Multiset.map_singleton, Nat.cast_one, one_div,
  Multiset.sum_cons, Multiset.sum_singleton]
State after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (cexp z + cexp (z * cexp (2 * ↑π * (↑↑2)⁻¹ * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2

State before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (cexp z + cexp (z * cexp (2 * ↑π * (↑↑2)⁻¹ * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
have h₁ : cexp (2 * ↑π * (↑↑(2 : ℕ+))⁻¹ * I) = -1 := by
  have h₂ : 2 * (π : ℂ) * (↑↑(2 : ℕ+))⁻¹ = π := by
    field_simp
  rw [h₂]
  simp only [exp_pi_mul_I]
State after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
h₁ : cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
⊢ (cexp z + cexp (z * cexp (2 * ↑π * (↑↑2)⁻¹ * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2

State before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
h₁ : cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
⊢ (cexp z + cexp (z * cexp (2 * ↑π * (↑↑2)⁻¹ * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
simp_rw [h₁]
State after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
h₁ : cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
⊢ (cexp z + cexp (z * -1)) / ↑↑2 = (cexp z + cexp (-z)) / 2

State before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
h₁ : cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
⊢ (cexp z + cexp (z * -1)) / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
simp only [mul_neg, mul_one]
State after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
h₁ : cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
⊢ (cexp z + cexp (-z)) / ↑↑2 = (cexp z + cexp (-z)) / 2

State before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
h₁ : cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
⊢ (cexp z + cexp (-z)) / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
congr
State after:
no goals

State before:
z : ℂ
⊢ range ↑2 = {0, 1}
Tactic:
rfl
State after:
no goals

State before:
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
Tactic:
have h₂ : 2 * (π : ℂ) * (↑↑(2 : ℕ+))⁻¹ = π := by
  field_simp
State after:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1

State before:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
Tactic:
rw [h₂]
State after:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (↑π * I) = -1

State before:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (↑π * I) = -1
Tactic:
simp only [exp_pi_mul_I]
State after:
no goals

State before:
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ 2 * ↑π * (↑↑2)⁻¹ = ↑π
Tactic:
field_simp
State after:
no goals