awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
have this : DifferentiableWithinAt ℝ (F := ℝ) (fun (i : ℝ) ↦ -(arcsin ∘ Neg.neg) i) (Ici (-x)) (-x)
Tactic: have := (h.comp (-x) differentiableWithinAt_id.fun_neg (mapsTo_image _ _)).fun_neg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
⊢ deriv arcsin = fun (x : ℝ) ↦ 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have h : ∀ (x : ℝ), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: funext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have pos : ∀ (h : x ≠ -1 ∧ x ≠ 1), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases h : x ≠ -1 ∧ x ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
pos : ∀ (h : x ≠ -1 ∧ x ≠ 1), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : ∀ (h : ¬(x ≠ -1 ∧ x ≠ 1)), deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: by_cases h : x ≠ -1 ∧ x ≠ 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : 0 = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
Tactic: rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (hypothesis)
Goal:
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have h₁ : x = -1 ∨ x = 1
Tactic: simp only [not_and_or, Ne, Classical.not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have neg : 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
h : x = -1 ∨ x = 1
neg : 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)
⊢ 0 = 1 / √(1 - HPow.hPow (β := ℕ) x 2)
have neg₁ : 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
n : ℕ∞ω
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
have refine_1 : ∀ (h : ContDiffAt ℝ n arccos x), ContDiffAt ℝ n arcsin x
Tactic: refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv (goal)
Goal:
x : ℝ
n : ℕ∞ω
refine_1 : ∀ (h : ContDiffAt ℝ n arccos x), ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
have refine_2 : ∀ (h : ContDiffAt ℝ n arcsin x), ContDiffAt ℝ n arccos x
Tactic: refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic (goal)
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
⊢ MeromorphicNFAt tan x
have refine : cos x ≠ 0 ∨ sin x ≠ 0
Tactic: refine MeromorphicNFOn.div analyticAt_sin analyticAt_cos.meromorphicNFAt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic (goal)
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
⊢ MeromorphicNFAt tanh x
have refine : cosh x ≠ 0 ∨ sinh x ≠ 0
Tactic: refine MeromorphicNFOn.div analyticAt_sinh analyticAt_cosh.meromorphicNFAt ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) (cos z)
have rw : HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
Tactic: rw [Complex.cos, Complex.exp_eq_exp_ℂ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (hypothesis)
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
have this : HasSum (fun (i : ℕ) ↦ ((z * I) ^ i / (↑i ! : ℂ) + (-z * I) ^ i / (↑i ! : ℂ)) / 2)
  ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
Tactic: have := ((expSeries_div_hasSum_exp (z * Complex.I)).add
    (expSeries_div_hasSum_exp (-z * Complex.I))).div_const 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (hypothesis)
Goal:
z : ℂ
this :
  HasSum (fun (i : ℕ) ↦ ((z * I) ^ i / (↑i ! : ℂ) + (-z * I) ^ i / (↑i ! : ℂ)) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
have this₁ : HasSum (β := ℕ × Fin 2)
  ((fun (i : ℕ) ↦ ((z * I) ^ i / (↑i ! : ℂ) + (-z * I) ^ i / (↑i ! : ℂ)) / 2) ∘
    (⇑(Equiv.symm (Nat.divModEquiv 2)) : (a : ℕ × Fin 2) → ℕ))
  ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
Tactic: replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (hypothesis)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (x.1 * 2 + (↑x.2 : ℕ)) / (↑(x.1 * 2 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (x.1 * 2 + (↑x.2 : ℕ)) / (↑(x.1 * 2 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
have this₁ : HasSum
  (fun (x : ℕ × Fin 2) ↦
    ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
        (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
      2)
  ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
Tactic: simp_rw [← mul_comm 2 _] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
have refine : ∀ (k : ℕ),
  HasSum
    (fun (c : Fin 2) ↦
      ((z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ)) /
        2)
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ))
Tactic: refine this.prod_fiberwise fun k => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ HasSum
    (fun (c : Fin 2) ↦
      ((z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * (k, c).1 + (↑(k, c).2 : ℕ)) / (↑(2 * (k, c).1 + (↑(k, c).2 : ℕ))! : ℂ)) /
        2)
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ))
have dsimp : HasSum
  (fun (c : Fin 2) ↦
    ((z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) +
        (-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) /
      2)
  ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ))
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ HasSum
    (fun (c : Fin 2) ↦
      ((z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) /
        2)
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ))
have h : (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
  ∑ b : Fin 2,
    ((z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) +
        (-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) /
      2
Tactic: convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ∑ b : Fin 2,
      ((z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) /
        2
have h : (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
  ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
        (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
      2 +
    ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
        (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
      2
Tactic: rw [Fin.sum_univ_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h : (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
  ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
    ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
        (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
      2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
h :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h₁ : (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
  ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
h :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
h₁ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h₂ : (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
  ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
h :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
h₁ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₂ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h₃ : (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
  ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
    ((z * I) ^ (2 * k) * (z * I) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k) * (-z * I) / (↑(2 * k + 1)! : ℂ)) / 2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
h :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
h₁ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₂ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₃ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k) * (z * I) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k) * (-z * I) / (↑(2 * k + 1)! : ℂ)) / 2
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h₄ : HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ) =
  (HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ) + HPow.hPow (β := ℕ) (-z * I) 2 ^ k / (↑(2 * k)! : ℂ)) / 2 +
    (HPow.hPow (β := ℕ) (z * I) 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) +
        HPow.hPow (β := ℕ) (-z * I) 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ)) /
      2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) /
        2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
h :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
h₁ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ) + (-z * I) ^ (2 * k + 0) / (↑(2 * k + 0)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₂ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ)) / 2
h₃ :
  (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) + (-z * I) ^ (2 * k) / (↑(2 * k)! : ℂ)) / 2 +
      ((z * I) ^ (2 * k) * (z * I) / (↑(2 * k + 1)! : ℂ) + (-z * I) ^ (2 * k) * (-z * I) / (↑(2 * k + 1)! : ℂ)) / 2
h₄ :
  HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ) =
    (HPow.hPow (β := ℕ) (z * I) 2 ^ k / (↑(2 * k)! : ℂ) + HPow.hPow (β := ℕ) (-z * I) 2 ^ k / (↑(2 * k)! : ℂ)) / 2 +
      (HPow.hPow (β := ℕ) (z * I) 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) +
          HPow.hPow (β := ℕ) (-z * I) 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ)) /
        2
⊢ (z * I) ^ (2 * k) / (↑(2 * k)! : ℂ) =
    ((z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) /
        2 +
      ((z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) /
        2
have h₅ : HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) =
  (HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ) +
        HPow.hPow (β := ℕ) (-z) 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k / (↑(2 * k)! : ℂ)) /
      2 +
    (HPow.hPow (β := ℕ) z 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (z * I) / (↑(2 * k + 1)! : ℂ) +
        HPow.hPow (β := ℕ) (-z) 2 ^ k * HPow.hPow (β := ℕ) I 2 ^ k * (-z * I) / (↑(2 * k + 1)! : ℂ)) /
      2
Tactic: simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, ← two_mul,
    neg_mul, mul_neg, neg_div, add_neg_cancel, zero_div, add_zero,
    mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I) (sin z)
have rw : HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
  ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
Tactic: rw [Complex.sin, Complex.exp_eq_exp_ℂ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (hypothesis)
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
have this : HasSum (fun (i : ℕ) ↦ ((-z * I) ^ i / (↑i ! : ℂ) - (z * I) ^ i / (↑i ! : ℂ)) * I / 2)
  ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
Tactic: have := (((expSeries_div_hasSum_exp (-z * Complex.I)).sub
    (expSeries_div_hasSum_exp (z * Complex.I))).mul_right Complex.I).div_const 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (hypothesis)
Goal:
z : ℂ
this :
  HasSum (fun (i : ℕ) ↦ ((-z * I) ^ i / (↑i ! : ℂ) - (z * I) ^ i / (↑i ! : ℂ)) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
have this₁ : HasSum (β := ℕ × Fin 2)
  ((fun (i : ℕ) ↦ ((-z * I) ^ i / (↑i ! : ℂ) - (z * I) ^ i / (↑i ! : ℂ)) * I / 2) ∘
    (⇑(Equiv.symm (Nat.divModEquiv 2)) : (a : ℕ × Fin 2) → ℕ))
  ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
Tactic: replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (hypothesis)
Goal:
z : ℂ
this :
  HasSum
    (fun (x : ℕ × Fin 2) ↦
      ((-z * I) ^ (x.1 * 2 + (↑x.2 : ℕ)) / (↑(x.1 * 2 + (↑x.2 : ℕ))! : ℂ) -
            (z * I) ^ (x.1 * 2 + (↑x.2 : ℕ)) / (↑(x.1 * 2 + (↑x.2 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
have this₁ : HasSum
  (fun (x : ℕ × Fin 2) ↦
    ((-z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ) -
          (z * I) ^ (2 * x.1 + (↑x.2 : ℕ)) / (↑(2 * x.1 + (↑x.2 : ℕ))! : ℂ)) *
        I /
      2)
  ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
Tactic: simp_rw [← mul_comm 2 _] at this
Cleared hypotheses: this