awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : ℂ)))
⊢ ∫ (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₁ : ((↑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) =
  (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
      (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
    ∫ (x : ℝ) in 0..π / 2,
      ((↑(cos x) : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
        (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
Tactic: convert!
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1
-- 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
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 : ℂ)))
h₁ :
  ((↑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) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
⊢ ∫ (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 convert_1 : IntervalIntegrable (ε := ℂ)
  (fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n - HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
  volume 0 (π / 2)
Tactic: convert!
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1
-- 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
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 : ℂ)))
h₁ :
  ((↑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) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
convert_1 :
  IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦
      (↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    volume 0 (π / 2)
⊢ ∫ (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 convert_2 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.sin (2 * z * (↑x : ℂ))) volume 0 (π / 2)
Tactic: convert!
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1
-- 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
⊢ 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 : ℂ)))
have h : ∀ x ∈ uIcc 0 (π / 2),
  Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ))
Tactic: refine integral_congr fun 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 : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
⊢ ((↑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) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
have h : Eq (α := ℂ)
  (∫ (x : ℝ) in 0..π / 2,
    (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
  (∫ (x : ℝ) in 0..π / 2,
    -(((↑(cos x) : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
        (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))))
Tactic: rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul,
      mul_zero, zero_mul, zero_mul, sub_zero, zero_sub, ←
      integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
-- 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
h :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
    (∫ (x : ℝ) in 0..π / 2,
      -(((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))))
⊢ ((↑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) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
have h₁ : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n))
  volume 0 (π / 2)
Tactic: rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul,
      mul_zero, zero_mul, zero_mul, sub_zero, zero_sub, ←
      integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
-- 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
h :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
    (∫ (x : ℝ) in 0..π / 2,
      -(((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))))
h₁ :
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n))
    volume 0 (π / 2)
⊢ ((↑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) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
have h₂ : IntervalIntegrable (ε := ℂ)
  (fun (x : ℝ) ↦ HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
  volume 0 (π / 2)
Tactic: rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul,
      mul_zero, zero_mul, zero_mul, sub_zero, zero_sub, ←
      integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
-- 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
h :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
    (∫ (x : ℝ) in 0..π / 2,
      -(((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))))
h₁ :
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n))
    volume 0 (π / 2)
h₂ :
  IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
    volume 0 (π / 2)
⊢ ((↑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) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
have h₃ : n - 1 ≠ 0
Tactic: rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul,
      mul_zero, zero_mul, zero_mul, sub_zero, zero_sub, ←
      integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
-- 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
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
    (∫ (x : ℝ) in 0..π / 2,
      -(((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))))
have h : ∀ x ∈ uIcc 0 (π / 2),
  (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)) =
    -(((↑(cos x) : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
        (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z)))
Tactic: refine integral_congr fun 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 : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)) =
    -(((↑(cos x) : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
        (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z)))
have h : ((↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2))) /
    (2 * z) =
  -((Complex.cos (↑x : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ))) /
    (2 * z)
Tactic: rw [Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq, ← mul_div_right_comm, ←
      mul_div_right_comm, ← sub_div, mul_div, ← neg_div]
-- 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 : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ ((↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2))) /
      (2 * z) =
    -((Complex.cos (↑x : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
              Complex.cos (↑x : ℂ) ^ (n - 2)) *
          -Complex.cos (2 * z * (↑x : ℂ))) /
      (2 * z)
have h : (↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
  -((Complex.cos (↑x : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
          Complex.cos (↑x : ℂ) ^ (n - 2)) *
      -Complex.cos (2 * z * (↑x : ℂ)))
Tactic: congr 1
-- 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 : ℝ
h : x ∈ uIcc 0 (π / 2)
| Complex.cos (↑x : ℂ) ^ n
have rw : Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
Tactic: rw [← Nat.sub_add_cancel hn, pow_add]
-- 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 : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
have conv_lhs : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
Tactic: conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
-- 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 : ℝ
h : x ∈ uIcc 0 (π / 2)
conv_lhs : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
have conv_lhs₁ : Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2 =
  Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
Tactic: conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
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 : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ (↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
    -((Complex.cos (↑x : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ)))
have this : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
Tactic: have : Complex.cos x ^ n = Complex.cos x ^ (n - 2) * Complex.cos x ^ 2 := by
      conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
-- 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 : ℝ
h : x ∈ uIcc 0 (π / 2)
this : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
⊢ (↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
    -((Complex.cos (↑x : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ)))
have h : (↑n : ℂ) *
      (Complex.cos (2 * z * (↑x : ℂ)) *
        (Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2)) -
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
  -((Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2 -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
          Complex.cos (↑x : ℂ) ^ (n - 2)) *
      -Complex.cos (2 * z * (↑x : ℂ)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ Ne (α := ℂ) (↑n : ℂ) 0
have contrapose! : ∀ (hn : Eq (α := ℂ) (↑n : ℂ) 0), n < 2
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : Eq (α := ℂ) (↑n : ℂ) 0
⊢ n < 2
have hn₁ : n = 0
Tactic: rw [Nat.cast_eq_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ n < 2
have rw : LT.lt (α := ℕ) 0 2
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ (1 - 4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (↑n : ℂ) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)
have nne : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: have nne : (n : ℂ) ≠ 0 := by
    contrapose! hn; rw [Nat.cast_eq_zero] at hn; rw [hn]; exact zero_lt_two