awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (i : ℝ) ↦ -((Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑i : ℂ) / (2 * z)))
    (-(-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z))) x
⊢ HasDerivAt (fun (y : ℝ) ↦ -Complex.cos (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.sin (2 * z * (↑x : ℂ))) x
have c₁ : HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * (2 * z)) / (2 * z)))
  (-(-(Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) / (2 * z))) x
Tactic: simp at c ⊢
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * (2 * z)) / (2 * z)))
    (-(-(Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) / (2 * z))) x
⊢ HasDerivAt (fun (y : ℝ) ↦ -Complex.cos (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.sin (2 * z * (↑x : ℂ))) x
have field_simp : ∀ (c : HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * 2 * z) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x),
  HasDerivAt (fun (y : ℝ) ↦ -(Complex.cos (2 * z * (↑y : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x
Tactic: field_simp at c ⊢
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
have b : HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ)) (-(↑(sin x) : ℂ)) x
Tactic: have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
      simpa using (hasDerivAt_cos x).ofReal_comp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ)) (-(↑(sin x) : ℂ)) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
have h : -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) = (↑n : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * -(↑(sin x) : ℂ)
Tactic: convert! HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)
have der1 : ∀ x ∈ uIcc 0 (π / 2),
  HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
Tactic: have der1 :
    ∀ x : ℝ,
      x ∈ uIcc 0 (π / 2) →
        HasDerivAt (fun y : ℝ => (cos y : ℂ) ^ n) (-n * sin x * (cos x : ℂ) ^ (n - 1)) x := by
    intro x _
    have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
      simpa using (hasDerivAt_cos x).ofReal_comp
    convert! HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
    ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)
have h : Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
  (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
Tactic: convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)
have h₁ : (↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
  (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
      (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
    ∫ (x : ℝ) in 0..π / 2,
      -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))
Tactic: convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
h₁ :
  (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)
have convert_1 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) volume 0 (π / 2)
Tactic: convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
h₁ :
  (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))
convert_1 :
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) volume 0 (π / 2)
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)
have convert_2 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) volume 0 (π / 2)
Tactic: convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
have h : ∀ (x : ℝ), Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
x : ℝ
⊢ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
have h : (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ)) = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))
have h : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..π / 2,
    (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)))
  (∫ (x : ℝ) in 0..π / 2,
    -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))))
Tactic: rw [Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div, mul_zero, sub_zero,
      cos_pi_div_two, Complex.ofReal_zero, zero_pow (by positivity : n ≠ 0), zero_mul, zero_sub,
      ← integral_neg, ← integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)))
    (∫ (x : ℝ) in 0..π / 2,
      -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))))
have h : ∀ x ∈ uIcc 0 (π / 2),
  (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) =
    -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z)))
Tactic: refine integral_congr fun x _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
    ((↑(cos x) : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    x
have c : HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
  ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
Tactic: have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
    ((↑(cos x) : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    x
have h : Eq (α := ℝ → ℂ) (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1)) fun (y : ℝ) ↦
  Complex.sin (↑y : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑y : ℂ)
Tactic: convert! ((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
h :
  Eq (α := ℝ → ℂ) (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1)) fun (y : ℝ) ↦
    Complex.sin (↑y : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑y : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
    ((↑(cos x) : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    x
have h₁ : (↑(cos x) : ℂ) ^ n - HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2) =
  Complex.cos (↑x : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑x : ℂ) +
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ))
Tactic: convert! ((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ (↑(cos x) : ℂ) ^ n - HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2) =
    Complex.cos (↑x : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑x : ℂ) +
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ))
have h : Complex.cos (↑x : ℂ) ^ n -
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
  Complex.cos (↑x : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑x : ℂ) +
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ))
Tactic: simp only [Complex.ofReal_cos, Complex.ofReal_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ Complex.cos (↑x : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.cos (↑x : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑x : ℂ) +
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ))
have h : Complex.cos (↑x : ℂ) ^ n -
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
  Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1) -
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
Tactic: rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ Complex.cos (↑x : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1) -
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
have h : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
h : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1)
⊢ Complex.cos (↑x : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1) -
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
have h₁ : HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
  Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1)
have h : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 1 + 1)
Tactic: rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
h : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 1 + 1)
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1)
have h₁ : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ n
Tactic: rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
have rw : HSub.hSub (α := ℂ) (↑n : ℂ) (↑1 : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
Tactic: rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
rw : HSub.hSub (α := ℂ) (↑n : ℂ) (↑1 : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
⊢ (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
have rw₁ : HSub.hSub (α := ℂ) (↑n : ℂ) 1 = HSub.hSub (α := ℂ) (↑n : ℂ) 1
Tactic: rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
have this : (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
Tactic: have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by
          rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
this : (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
⊢ HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
have h : HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
  Complex.sin (↑x : ℂ) *
    (HSub.hSub (α := ℂ) (↑n : ℂ) 1 * Complex.cos (↑x : ℂ) ^ (n - HAdd.hAdd (α := ℕ) 1 1) * Complex.sin (↑x : ℂ))
Tactic: rw [Nat.sub_sub, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)
have der1 : ∀ x ∈ uIcc 0 (π / 2),
  HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
    ((↑(cos x) : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    x
Tactic: have der1 :
    ∀ x : ℝ,
      x ∈ uIcc 0 (π / 2) →
        HasDerivAt (fun y : ℝ => sin y * (cos y : ℂ) ^ (n - 1))
          ((cos x : ℂ) ^ n - (n - 1) * (sin x : ℂ) ^ 2 * (cos x : ℂ) ^ (n - 2)) x := by
    intro x _
    have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
    convert! ((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal using 1
    · simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]
    · simp only [Complex.ofReal_cos, Complex.ofReal_sin]
      rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
      congr 1
      · rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]
      · have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by
          rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
        rw [Nat.sub_sub, this]
        ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)
have h : Eq (α := ℂ) (∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1))
  (∫ (x : ℝ) in 0..π / 2, (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ)))
Tactic: convert!
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1