-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem _root_.Complex.tendsto_euler_sin_prod (z : ℂ) :
    Tendsto (fun n : ℕ => π * z * ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2))
      atTop (𝓝 <| Complex.sin (π * z))

Proof state:
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)

Tactic:
convert tendsto_integral_cos_pow_mul_div this using 1

Result:
case h.e'_3
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)) =
    fun n => (∫ (x : ℝ) in 0 ..π / 2, ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)

case h.e'_5
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * ↑0))

Proof state:
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))

Tactic:
convert (tendsto_mul_iff_of_ne_zero _ one_ne_zero).mp A

Result:
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
        ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))
    atTop (𝓝 1)

Proof state:
z : ℂ
⊢ Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))

Tactic:
have A :
  Tendsto
    (fun n : ℕ =>
      ((π * 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) : ℝ))
    atTop (𝓝 <| _) :=
  Tendsto.congr (fun n => sin_pi_mul_eq z n) tendsto_const_nhds

Result:
z : ℂ
A :
  Tendsto
    (fun n =>
      ((↑π * 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)))
    atTop (𝓝 (Complex.sin (↑π * z)))
⊢ Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))

Proof state:
case h.e'_3.h.e_a.e_f.h
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
n : ℕ
x : ℝ
⊢ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)

Tactic:
rw [mul_comm]

Result:
no goals

Proof state:
z : ℂ
A :
  Tendsto
    (fun n =>
      ((↑π * 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)))
    atTop (𝓝 (Complex.sin (↑π * z)))
⊢ Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))

Tactic:
have : 𝓝 (Complex.sin (π * z)) = 𝓝 (Complex.sin (π * z) * 1) := by rw [mul_one]

Result:
z : ℂ
A :
  Tendsto
    (fun n =>
      ((↑π * 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)))
    atTop (𝓝 (Complex.sin (↑π * z)))
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
⊢ Tendsto (fun n => ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))

Proof state:
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)

Tactic:
have : ContinuousOn (fun x : ℝ => Complex.cos (2 * z * x)) (Icc 0 (π / 2)) :=
  (Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).continuousOn

Result:
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun n =>
      (↑π * 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)