-- 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.zero
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) * (2 * z * ↑π) = ↑π * z * Complex.sin (↑π * z) * 2

Tactic:
ring

Result:
no goals

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 + 1))) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * (n + 1)))

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
⊢ ↑π * 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))) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)

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

Tactic:
field_simp

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

Proof state:
case h.e'_2.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))
this✝ :
  (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
this : ↑C ≠ 0
⊢ 2 * ↑n = ↑(2 * n)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2
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))
this✝¹ :
  (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
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 1) + 1

Tactic:
push_cast

Result:
case h.e'_2
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))
this✝¹ :
  (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
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 1 + 1

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

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
this : ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * 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))

Tactic:
nth_rw 2 [Nat.succ_eq_add_one]

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
this : ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * 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 + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ))