-- 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))
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))
⊢ 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 * cos 0 - 0 * 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]