awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x = -1 ∨ x = 1
neg : 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)
neg₁ : 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)
⊢ 0 = 1 / √(1 - HPow.hPow (β := ℕ) x 2)

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
⊢ 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
⊢ 0 = 1 / √(1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
⊢ DifferentiableOn ℝ arcsin {-1, 1}ᶜ

Tactic:
fun _x hx =>
  (differentiableAt_arcsin.2
      ⟨fun h => hx (Or.inl h), fun h => hx (Or.inr h)⟩).differentiableWithinAt

Premises used: Iff.mpr, Real.differentiableAt_arcsin, DifferentiableAt.differentiableWithinAt, And.intro, DifferentiableOn, Or.inl, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
n : ℕ∞ω
⊢ ContDiffOn ℝ n arcsin {-1, 1}ᶜ

Tactic:
fun _x hx =>
  (contDiffAt_arcsin (mt Or.inl hx) (mt Or.inr hx)).contDiffWithinAt

Premises used: ContDiffOn, mt, Or.inl, Real.contDiffAt_arcsin, Or.inr, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
n : ℕ∞ω
⊢ ContDiffAt ℝ n arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Tactic:
⟨fun h => or_iff_not_imp_left.2 fun hn => differentiableAt_arcsin.1 <| h.differentiableAt hn,
    fun h => h.elim (fun hn => hn.symm ▸ (contDiff_zero.2 continuous_arcsin).contDiffAt) fun hx =>
      contDiffAt_arcsin hx.1 hx.2⟩

Premises used: Iff.mpr, Real.differentiableAt_arcsin, Real.continuous_arcsin, contDiff_zero, ContDiffAt.differentiableAt, Eq.rec, And.right, And.left, Classical.or_iff_not_imp_left, Iff.intro, Iff.mp, Or.elim, Eq.symm, Real.contDiffAt_arcsin, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasStrictDerivAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) x

Tactic:
(hasStrictDerivAt_arcsin h₁ h₂).const_sub (π / 2)

Premises used: Real.pi, HDiv.hDiv, Real.hasStrictDerivAt_arcsin, OfNat.ofNat, HasStrictDerivAt.const_sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasDerivAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) x

Tactic:
(hasDerivAt_arcsin h₁ h₂).const_sub (π / 2)

Premises used: HasDerivAt.const_sub, Real.pi, Real.hasDerivAt_arcsin, HDiv.hDiv, OfNat.ofNat, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
n : ℕ∞ω
⊢ ContDiffAt ℝ n arccos x

Tactic:
contDiffAt_const.sub (contDiffAt_arcsin h₁ h₂)

Premises used: contDiffAt_const, ContDiffAt.sub, Real.contDiffAt_arcsin, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) (Ici x) x

Tactic:
(hasDerivWithinAt_arcsin_Ici h).const_sub _

Premises used: Real.hasDerivWithinAt_arcsin_Ici, HasDerivWithinAt.const_sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) (Iic x) x

Tactic:
(hasDerivWithinAt_arcsin_Iic h).const_sub _

Premises used: HasDerivWithinAt.const_sub, Real.arccos, Real.hasDerivWithinAt_arcsin_Iic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ DifferentiableWithinAt ℝ arccos (Ici x) x ↔ x ≠ -1

Tactic:
(differentiableWithinAt_const_sub_iff _).trans differentiableWithinAt_arcsin_Ici

Premises used: Real.differentiableWithinAt_arcsin_Ici, Iff.trans, differentiableWithinAt_const_sub_iff, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ DifferentiableWithinAt ℝ arccos (Iic x) x ↔ x ≠ 1

Tactic:
(differentiableWithinAt_const_sub_iff _).trans differentiableWithinAt_arcsin_Iic

Premises used: Real.differentiableWithinAt_arcsin_Iic, Iff.trans, differentiableWithinAt_const_sub_iff, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ arccos x ↔ x ≠ -1 ∧ x ≠ 1

Tactic:
(differentiableAt_const _).sub_iff_right.trans differentiableAt_arcsin

Premises used: Real.differentiableAt_arcsin, DifferentiableAt.sub_iff_right, differentiableAt_const, Iff.trans, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
⊢ -deriv arcsin x = -(1 / √(1 - HPow.hPow (β := ℕ) x 2))

Tactic:
simp only [deriv_arcsin]

Premises used: Real.deriv_arcsin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
⊢ DifferentiableOn ℝ arccos {-1, 1}ᶜ

Tactic:
differentiableOn_arcsin.const_sub _

Premises used: Real.differentiableOn_arcsin, DifferentiableOn.const_sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
n : ℕ∞ω
⊢ ContDiffOn ℝ n arccos {-1, 1}ᶜ

Tactic:
contDiffOn_const.sub contDiffOn_arcsin

Premises used: ContDiffOn.sub, Real.contDiffOn_arcsin, Real.arccos, contDiffOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
n : ℕ∞ω
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Tactic:
Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff

Premises used: Real.contDiffAt_arcsin_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
n : ℕ∞ω
refine_1 : ∀ (h : ContDiffAt ℝ n arccos x), ContDiffAt ℝ n arcsin x
refine_2 : ∀ (h : ContDiffAt ℝ n arcsin x), ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Tactic:
refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff

Premises used: Real.contDiffAt_arcsin_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x

Tactic:
simpa [arccos] using (contDiffAt_const (c := π / 2)).sub h

Premises used: contDiffAt_const, ContDiffAt.sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Goal:
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x

Tactic:
simpa [arccos] using (contDiffAt_const (c := π / 2)).sub h

Premises used: contDiffAt_const, ContDiffAt.sub, Real.arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
_ : Membership.mem (γ := Set ℂ) Set.univ x → MeromorphicNFAt tan x
⊢ Membership.mem (γ := Set ℂ) Set.univ x → MeromorphicNFAt tan x

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
⊢ MeromorphicNFAt tan x

Tactic:
MeromorphicNFOn.div analyticAt_sin analyticAt_cos.meromorphicNFAt ?_

Premises used: Complex.analyticAt_sin, AnalyticAt.meromorphicNFAt, Complex.tan, Complex.analyticAt_cos, MeromorphicNFOn.div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
refine : cos x ≠ 0 ∨ sin x ≠ 0
⊢ MeromorphicNFAt tan x

Tactic:
refine MeromorphicNFOn.div analyticAt_sin analyticAt_cos.meromorphicNFAt ?_

Premises used: Complex.analyticAt_sin, AnalyticAt.meromorphicNFAt, Complex.analyticAt_cos, MeromorphicNFOn.div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
⊢ cos x ≠ 0 ∨ sin x ≠ 0

Tactic:
grind [sin_sq_add_cos_sq]

Premises used: Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
z : ℂ
⊢ MeromorphicAt tan z

Tactic:
(meromorphicNFOn_tan (Set.mem_univ z)).meromorphicAt

Premises used: Complex.meromorphicNFOn_tan, MeromorphicNFAt.meromorphicAt, Set.mem_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
⊢ Meromorphic tan

Tactic:
meromorphicAt_tan

Premises used: Meromorphic, Complex.meromorphicAt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
_ : Membership.mem (γ := Set ℂ) Set.univ x → MeromorphicNFAt tanh x
⊢ Membership.mem (γ := Set ℂ) Set.univ x → MeromorphicNFAt tanh x

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
⊢ MeromorphicNFAt tanh x

Tactic:
MeromorphicNFOn.div analyticAt_sinh analyticAt_cosh.meromorphicNFAt ?_

Premises used: Complex.tanh, Complex.analyticAt_cosh, AnalyticAt.meromorphicNFAt, Complex.analyticAt_sinh, MeromorphicNFOn.div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
refine : cosh x ≠ 0 ∨ sinh x ≠ 0
⊢ MeromorphicNFAt tanh x

Tactic:
refine MeromorphicNFOn.div analyticAt_sinh analyticAt_cosh.meromorphicNFAt ?_

Premises used: Complex.analyticAt_cosh, AnalyticAt.meromorphicNFAt, Complex.analyticAt_sinh, MeromorphicNFOn.div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
x : ℂ
h : Membership.mem (γ := Set ℂ) Set.univ x
⊢ cosh x ≠ 0 ∨ sinh x ≠ 0

Tactic:
grind [cosh_sq_sub_sinh_sq]

Premises used: Complex.cosh_sq_sub_sinh_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
z : ℂ
⊢ MeromorphicAt tanh z

Tactic:
(meromorphicNFOn_tanh (Set.mem_univ z)).meromorphicAt

Premises used: MeromorphicNFAt.meromorphicAt, Set.mem_univ, Complex.meromorphicNFOn_tanh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic
Goal:
⊢ Meromorphic tanh

Tactic:
meromorphicAt_tanh

Premises used: Meromorphic, Complex.meromorphicAt_tanh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
rw :
  HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) (cos z)

Tactic:
rw [Complex.cos, Complex.exp_eq_exp_ℂ]

Premises used: Complex.exp_eq_exp_ℂ, Complex.cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 (β := ℕ × 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 (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

Premises used: mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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)

Tactic:
this.prod_fiberwise fun k => ?_

Premises used: HasSum.prod_fiberwise
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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)
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)! : ℂ))
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)

Tactic:
refine this.prod_fiberwise fun k => ?_

Premises used: HasSum.prod_fiberwise
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ
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)! : ℂ))
⊢ 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:
dsimp only
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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)
    (∑ b : Fin 2,
      ((z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) /
        2)

Tactic:
hasSum_fintype (_ : Fin 2 → ℂ)

Premises used: hasSum_fintype, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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)! : ℂ) =
    ∑ b : Fin 2,
      ((z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) /
        2
⊢ 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:
convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1

Premises used: hasSum_fintype, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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)! : ℂ) =
    ∑ b : Fin 2,
      ((z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) +
          (-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) /
        2

Tactic:
rw [Fin.sum_univ_two]

Premises used: Fin.sum_univ_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
rw :
  HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I) (sin z)

Tactic:
rw [Complex.sin, Complex.exp_eq_exp_ℂ]

Premises used: Complex.exp_eq_exp_ℂ, Complex.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 (β := ℕ × 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 (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

Premises used: mul_comm, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ))! : ℂ)) *
          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)

Tactic:
this.prod_fiberwise fun k => ?_

Premises used: HasSum.prod_fiberwise
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
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 : ℕ))! : ℂ)) *
            I /
          2)
      ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)

Tactic:
refine this.prod_fiberwise fun k => ?_

Premises used: HasSum.prod_fiberwise
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
dsimp :
  HasSum
    (fun (c : Fin 2) ↦
      ((-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)
⊢ 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 : ℕ))! : ℂ)) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)

Tactic:
dsimp only
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ HasSum (α := ℂ)
    (fun (c : Fin 2) ↦
      ((-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) *
          I /
        2)
    (∑ b : Fin 2,
      ((-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) *
          I /
        2)

Tactic:
hasSum_fintype (_ : Fin 2 → ℂ)

Premises used: hasSum_fintype, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
h :
  (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ∑ b : Fin 2,
      ((-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) *
          I /
        2
⊢ HasSum
    (fun (c : Fin 2) ↦
      ((-z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑c : ℕ)) / (↑(2 * k + (↑c : ℕ))! : ℂ)) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I)

Tactic:
convert! hasSum_fintype (_ : Fin 2 → ℂ) using 1

Premises used: hasSum_fintype, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
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 : ℕ))! : ℂ)) *
          I /
        2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
h :
  (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ((-z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑0 : ℕ)) / (↑(2 * k + (↑0 : ℕ))! : ℂ)) *
          I /
        2 +
      ((-z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑1 : ℕ)) / (↑(2 * k + (↑1 : ℕ))! : ℂ)) *
          I /
        2
⊢ (z * I) ^ (2 * k + 1) / (↑(2 * k + 1)! : ℂ) / I =
    ∑ b : Fin 2,
      ((-z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ) -
            (z * I) ^ (2 * k + (↑b : ℕ)) / (↑(2 * k + (↑b : ℕ))! : ℂ)) *
          I /
        2

Tactic:
rw [Fin.sum_univ_two]

Premises used: Fin.sum_univ_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Goal:
z : ℂ
⊢ HasSum (fun (n : ℕ) ↦ (z * I) ^ (2 * n) / (↑(2 * n)! : ℂ)) (cos z)

Tactic:
Complex.hasSum_cos' z

Premises used: Complex.hasSum_cos'