awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) : ℂ)
⊢ (((↑π : ℂ) * 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))) : ℂ)
have inr : let A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2);
∀
  (hn :
    Complex.sin ((↑π : ℂ) * z) =
      ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)),
  ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
    ((↑π : ℂ) * z * (A * (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: set A := ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
hn :
  Complex.sin ((↑π : ℂ) * z) =
    ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
⊢ ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
    ((↑π : ℂ) * z * (A * (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))) : ℂ)
have inr : let B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n);
∀ (hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)),
  (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
    ((↑π : ℂ) * z * (A * (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: set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
⊢ (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
    ((↑π : ℂ) * z * (A * (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))) : ℂ)
have inr : let C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n);
∀ (hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)),
  (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (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: set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
rw : 2 * (n + 1) = 2 * n + 2
⊢ 2 * n.succ = 2 * n + 2
have rw₁ : 2 * n + HMul.hMul (α := ℕ) 2 1 = 2 * n + 2
Tactic: rw [Nat.succ_eq_add_one, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (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))) : ℂ)
have aux' : 2 * n.succ = 2 * n + 2
Tactic: have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
have rw : 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
Tactic: rw [integral_cos_pow_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
have rw : 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
    (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Tactic: rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
rw :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
have rw₁ : 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 2) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
    (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Tactic: rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
rw :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₁ :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
have rw₂ : 1 / 2 *
    ((sin 0 ^ (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
    (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Tactic: rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
rw :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₁ :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₂ :
  1 / 2 *
      ((sin 0 ^ (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 *
          ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
have rw₃ : 1 / 2 *
    ((HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
    (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Tactic: rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
rw :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₁ :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₂ :
  1 / 2 *
      ((sin 0 ^ (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 *
          ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₃ :
  1 / 2 *
      ((HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 *
          ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
have rw₄ : 1 / 2 *
    ((HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos 0 - HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos π) /
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
    (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Tactic: rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
rw :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₁ :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 2) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₂ :
  1 / 2 *
      ((sin 0 ^ (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 *
          ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₃ :
  1 / 2 *
      ((HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos 0 - sin π ^ (2 * n + 1) * cos π) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 *
          ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
rw₄ :
  1 / 2 *
      ((HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos 0 - HPow.hPow (α := ℝ) 0 (2 * n + 1) * cos π) /
          HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 *
          ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
      (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
have rw₅ : 1 / 2 *
    ((0 * HPow.hPow (α := ℝ) 0 (2 * n) * cos 0 - 0 * HPow.hPow (α := ℝ) 0 (2 * n) * cos π) /
        HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 +
      HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n)) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) *
    (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Tactic: rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (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))) : ℂ)
have this : ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
  (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
Tactic: have : (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n.succ)) = (2 * (n : ℝ) + 1) / (2 * n + 2) * C := by
      rw [integral_cos_pow_eq]
      dsimp only [C]
      rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (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))) : ℂ)
have inr : (↑π : ℂ) * z * A * B / (↑C : ℂ) =
  ((↑π : ℂ) * z * (A * (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))) /
    (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (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.succ)) /
      (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)
have this₁ : (↑π : ℂ) * z * (A * (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.succ) =
  (↑π : ℂ) * z * A *
    ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
Tactic: have :
      (π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
          ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
        π * z * A *
          (((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
            ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) := by
      grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this :
  (↑π : ℂ) * z * (A * (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.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (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.succ)) /
      (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)
have inr : (↑π : ℂ) * z * A * B / (↑C : ℂ) =
  (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ)) /
    (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)
Tactic: rw [this]