awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 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 this : ∫ (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)
Tactic: have := integral_cos_mul_cos_pow_aux hn hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  ∫ (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)
⊢ (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 this₁ : (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
    (↑n : ℂ) / (2 * z) *
      ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
  (↑n : ℂ) / (2 * z) *
    -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
Tactic: rw [integral_sin_mul_sin_mul_cos_pow_eq hn hz, sub_eq_neg_add, mul_add, ← sub_eq_iff_eq_add]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
⊢ (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 h : (1 - 4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) *
    ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
  -((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
          (↑n : ℂ) / (2 * z) *
            ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n)) *
      HPow.hPow (β := ℕ) (2 * z) 2 /
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
Tactic: convert! congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
h :
  (1 - 4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    -((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
            (↑n : ℂ) / (2 * z) *
              ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n)) *
        HPow.hPow (β := ℕ) (2 * z) 2 /
      HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
⊢ (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 h₁ : HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (↑n : ℂ) *
    ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2) =
  -((↑n : ℂ) / (2 * z) *
          -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
              ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))) *
      HPow.hPow (β := ℕ) (2 * z) 2 /
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
Tactic: convert! congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n + 2) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
have h : HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
  4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑(2 * n + 2) : ℂ) 2
Tactic: convert! integral_cos_mul_cos_pow (by lia : 2 ≤ 2 * n + 2) hz using 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h :
  HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑(2 * n + 2) : ℂ) 2
⊢ (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n + 2) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
have h₁ : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HSub.hSub (α := ℂ) (↑(2 * n + 2) : ℂ) 1
Tactic: convert! integral_cos_mul_cos_pow (by lia : 2 ≤ 2 * n + 2) hz using 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h :
  HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑(2 * n + 2) : ℂ) 2
h₁ : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HSub.hSub (α := ℂ) (↑(2 * n + 2) : ℂ) 1
⊢ (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n + 2) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
have h₂ : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = (↑(2 * n + 2) : ℂ)
Tactic: convert! integral_cos_mul_cos_pow (by lia : 2 ≤ 2 * n + 2) hz using 3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑(2 * n + 2) : ℂ) 2
have h : HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
  4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) 2
Tactic: simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) 2
have h : HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
  4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + HMul.hMul (α := ℂ) 2 1) 2
Tactic: nth_rw 2 [← mul_one (2 : ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + HMul.hMul (α := ℂ) 2 1) 2
have h : HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
  4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) 2 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2
Tactic: rw [← mul_add, mul_pow, ← div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HSub.hSub (α := ℂ) (↑(2 * n + 2) : ℂ) 1
have h : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 - 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = (↑(2 * n + 2) : ℂ)
have h : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ n
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) = ∫ (x : ℝ) in 0..π, sin x ^ n
Tactic: rw [mul_comm (1 / 2 : ℝ), ← div_eq_iff (one_div_ne_zero (two_ne_zero' ℝ)), ← div_mul, div_one,
    mul_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    ∫ (x : ℝ) in 0..π, sin x ^ n
have L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
Tactic: have L : IntervalIntegrable _ volume 0 (π / 2) := (continuous_sin.pow n).intervalIntegrable _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    ∫ (x : ℝ) in 0..π, sin x ^ n
have R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
Tactic: have R : IntervalIntegrable _ volume (π / 2) π := (continuous_sin.pow n).intervalIntegrable _ _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    ∫ (x : ℝ) in 0..π, sin x ^ n
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, sin x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
Tactic: rw [← integral_add_adjacent_intervals L R]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, sin x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, sin x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
have e_a₁ : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
Tactic: nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2 - 0, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
Tactic: nth_rw 3 [(by ring : π / 2 = π / 2 - 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2 - 0, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos (π / 2 - x) ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
Tactic: rw [← integral_comp_sub_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos (π / 2 - x) ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
have e_a : ∀ x ∈ uIcc 0 (π / 2), cos (π / 2 - x) ^ n = sin x ^ n
Tactic: refine integral_congr fun x _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ cos (π / 2 - x) ^ n = sin x ^ n
have e_a : sin x ^ n = sin x ^ n
Tactic: rw [cos_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π / 2 + π / 2, sin x ^ n)
Tactic: nth_rw 3 [(by ring : π = π / 2 + π / 2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π / 2 + π / 2, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0 + π / 2..π / 2 + π / 2, sin x ^ n)
Tactic: nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0 + π / 2..π / 2 + π / 2, sin x ^ n)
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n)
Tactic: rw [← integral_comp_add_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n)
have e_a : ∀ x ∈ uIcc 0 (π / 2), cos x ^ n = sin (x + π / 2) ^ n
Tactic: refine integral_congr fun x _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ cos x ^ n = sin (x + π / 2) ^ n
have e_a : cos x ^ n = cos x ^ n
Tactic: rw [sin_add_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
have inl : Complex.sin ((↑π : ℂ) * 0) =
  (((↑π : ℂ) * 0 *
        ∏ j ∈ Finset.range n,
          (1 - HPow.hPow (α := ℂ) (β := ℕ) 0 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (HMul.hMul (α := ℂ) 2 0 * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
    (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
n : ℕ
inl :
  Complex.sin ((↑π : ℂ) * 0) =
    (((↑π : ℂ) * 0 *
          ∏ j ∈ Finset.range n,
            (1 - HPow.hPow (α := ℂ) (β := ℕ) 0 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (HMul.hMul (α := ℂ) 2 0 * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
have inr : ∀ (hz : z ≠ 0),
  Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
Tactic: rcases eq_or_ne z 0 with (rfl | hz)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range 0, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ HMul.hMul (α := ℕ) 2 0) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ HMul.hMul (α := ℕ) 2 0) : ℂ)
have inr : Complex.sin ((↑π : ℂ) * z) = ((↑π : ℂ) * z * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ))) / (↑(π / 2) : ℂ)
Tactic: simp_rw [mul_zero, pow_zero, mul_one, Finset.prod_range_zero, mul_one,
      integral_one, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
⊢ 2 * z * (↑(π / 2) : ℂ) = (↑π : ℂ) * z
have push_cast : 2 * z * ((↑π : ℂ) / 2) = (↑π : ℂ) * z
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
⊢ Complex.sin ((↑π : ℂ) * z) = ((↑π : ℂ) * z * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ))) / (↑(π / 2) : ℂ)
have inr : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * (Complex.sin ((↑π : ℂ) * z) / (2 * z)) / (↑(π / 2) : ℂ)
Tactic: rw [integral_cos_mul_complex (mul_ne_zero two_ne_zero hz), Complex.ofReal_zero,
      mul_zero, Complex.sin_zero, zero_div, sub_zero,
      (by push_cast; ring : 2 * z * ↑(π / 2) = π * z)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range (n + 1),
            (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * (n + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)
have inr : (((↑π : ℂ) * z *
        ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
    (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
  ((↑π : ℂ) * z *
        ((∏ x ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1) 2)) *
          (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * (n + 1))) /
    (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)
Tactic: rw [hn, Finset.prod_range_succ]