-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem sin_pi_mul_eq (z : ℂ) (n : ℕ) :
    Complex.sin (π * z) =
      ((π * z * ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)) *
          ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)) /
        (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n) : ℝ)

Proof state:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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 - z ^ 2 / (↑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)

Result:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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 - z ^ 2 / (↑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)))

Proof state:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  ↑π * 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))
⊢ (1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B

Tactic:
convert integral_cos_mul_cos_pow_even n hz

Result:
case h.e'_2.h.e'_5.h.e'_6.h.e'_6.h.e'_5
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  ↑π * 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))
⊢ ↑n.succ = ↑n + 1

Proof state:
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑(π / 2) = ↑π * z

Tactic:
push_cast

Result:
z : ℂ
hz : z ≠ 0
⊢ 2 * z * (↑π / 2) = ↑π * z

Proof state:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)

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
  nth_rw 2 [Nat.succ_eq_add_one]
  rw [Nat.cast_add_one]
  ring

Result:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  ↑π * 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))
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)

Proof state:
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑π = ↑π * z * 2

Tactic:
ring

Result:
no goals

Proof state:
case inr.zero
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = ↑π * z * (Complex.sin (↑π * z) / (2 * z)) / ↑(π / 2)

Tactic:
field_simp [Complex.ofReal_ne_zero.mpr pi_pos.ne']

Result:
case inr.zero
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) * (2 * z * ↑π) = ↑π * z * Complex.sin (↑π * z) * 2

Proof state:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C

Tactic:
dsimp only [C]

Result:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)

Proof state:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  ↑π * 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))
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)

Tactic:
rw [this]

Result:
case inr.succ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑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) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  ↑π * 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))
⊢ ↑π * z * A * B / ↑C =
    ↑π * z * A *
        ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)