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

case h.e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re
x : ℝ
⊢ Tendsto (fun n => π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (π * x)))
convert (Complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x) using 1
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    (Complex.re ∘ fun n => ↑π * ↑x * ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)) n
case h.e'_3
x : ℝ
⊢ (fun n => π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) =
    Complex.re ∘ fun n => ↑π * ↑x * ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)
ext1 n
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    (Complex.re ∘ fun n => ↑π * ↑x * ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)) n
rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.ofReal_mul_re]
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
suffices
  (∏ j : ℕ in Finset.range n, ((1 : ℂ) - (x : ℂ) ^ 2 / ((j : ℂ) + 1) ^ 2)) =
    (∏ j : ℕ in Finset.range n, ((1 : ℝ) - x ^ 2 / ((j : ℝ) + 1) ^ 2) : ℝ) by
  rw [this, Complex.ofReal_re]
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ∏ i in Finset.range n, ↑(1 - x ^ 2 / (↑i + 1) ^ 2)
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
rw [Complex.ofReal_prod]
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)
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ∏ i in Finset.range n, ↑(1 - x ^ 2 / (↑i + 1) ^ 2)
refine' Finset.prod_congr (by rfl) fun n _ => _
no goals
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)
norm_cast
no goals
x : ℝ
n : ℕ
this : ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
rw [this, Complex.ofReal_re]
no goals
x : ℝ
n : ℕ
⊢ Finset.range n = Finset.range n
rfl
no goals
case h.e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re
rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]