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

Proof state:
case h.e'_3
x : ℝ
⊢ (fun n => π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) =
    Complex.re ∘ fun n => ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)

Tactic:
ext1 n

Result:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    (Complex.re ∘ fun n => ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)) n

Proof state:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re

Tactic:
suffices
  (∏ j ∈ Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℂ) =
    (∏ j ∈ Finset.range n, (1 - x ^ 2 / (j + 1) ^ 2) : ℝ) by
  rw [this, Complex.ofReal_re]

Result:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))

Proof state:
x : ℝ
n : ℕ
⊢ Finset.range n = Finset.range n

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re

Tactic:
rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]

Result:
no goals

Proof state:
case h.e'_3.h
x : ℝ
n✝ n : ℕ
x✝ : n ∈ Finset.range n✝
⊢ 1 - ↑x ^ 2 / (↑n + 1) ^ 2 = ↑(1 - x ^ 2 / (↑n + 1) ^ 2)

Tactic:
norm_cast

Result:
no goals

Proof state:
x : ℝ
n : ℕ
this : ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re

Tactic:
rw [this, Complex.ofReal_re]

Result:
no goals

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

Tactic:
convert (Complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x) using 1

Result:
case h.e'_3
x : ℝ
⊢ (fun n => π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) =
    Complex.re ∘ fun n => ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)

case h.e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re

Proof state:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ∏ i ∈ Finset.range n, ↑(1 - x ^ 2 / (↑i + 1) ^ 2)

Tactic:
refine Finset.prod_congr (by rfl) fun n _ => ?_

Result:
case h.e'_3.h
x : ℝ
n✝ n : ℕ
x✝ : n ∈ Finset.range n✝
⊢ 1 - ↑x ^ 2 / (↑n + 1) ^ 2 = ↑(1 - x ^ 2 / (↑n + 1) ^ 2)

Proof state:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))

Tactic:
rw [Complex.ofReal_prod]

Result:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ∏ i ∈ Finset.range n, ↑(1 - x ^ 2 / (↑i + 1) ^ 2)

Proof state:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    (Complex.re ∘ fun n => ↑π * ↑x * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)) n

Tactic:
rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.re_ofReal_mul]

Result:
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re