internlm/Lean-Github huggingface dataset:
Theorem: RuesN2EqualsCosh
Proof 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]
Proof 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
Theorem: RuesN2EqualsCosh
Proof 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₁]
Proof 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
Theorem: RuesN2EqualsCosh
Proof 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]
Proof 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
Theorem: RuesN2EqualsCosh
Proof 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
Proof state after:
no goals
Theorem: RuesN2EqualsCosh
Proof state before:
z : ℂ
⊢ range ↑2 = {0, 1}
Tactic:
rfl
Proof state after:
no goals
Theorem: RuesN2EqualsCosh
Proof state before:
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
Tactic:
have h₂ : 2 * (π : ℂ) * (↑↑(2 : ℕ+))⁻¹ = π := by
  field_simp
Proof state after:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
Theorem: RuesN2EqualsCosh
Proof state before:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (2 * ↑π * (↑↑2)⁻¹ * I) = -1
Tactic:
rw [h₂]
Proof state after:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (↑π * I) = -1
Theorem: RuesN2EqualsCosh
Proof state before:
z : ℂ
h₀ : range ↑2 = {0, 1}
h₂ : 2 * ↑π * (↑↑2)⁻¹ = ↑π
⊢ cexp (↑π * I) = -1
Tactic:
simp only [exp_pi_mul_I]
Proof state after:
no goals
Theorem: RuesN2EqualsCosh
Proof state before:
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ 2 * ↑π * (↑↑2)⁻¹ = ↑π
Tactic:
field_simp
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ Rues 4 z = (z / (1 + I)).cosh * (z / (1 - I)).cosh
Tactic:
rw [RuesNEqualsExpSum, Complex.cosh, Complex.cosh]
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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₀
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₁]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₁
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₂]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₂
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₃]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₃
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₄]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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₄
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof 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)
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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]
Proof 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⁻¹
Theorem: RuesN4EqualsCoshCosh
Proof 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
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ ↑4 = 4
Tactic:
rfl
Proof state after:
no goals