awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
A :
  Tendsto
    (fun (n : ℕ) ↦
      (((↑π : ℂ) * z *
            ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (Complex.sin ((↑π : ℂ) * z)))
have A₁ : Tendsto
  (fun (n : ℕ) ↦
    ((↑π : ℂ) * z *
        ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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))
Tactic: simp_rw [this, mul_div_assoc] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (Complex.sin ((↑π : ℂ) * z)))
have convert! : 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)
Tactic: convert! (tendsto_mul_iff_of_ne_zero _ one_ne_zero).mp A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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)
have suffices : 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: suffices Tendsto (fun n : ℕ =>
        (∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) /
          (∫ x in (0 : ℝ)..π / 2, cos x ^ n : ℝ)) atTop (𝓝 1) from
    this.comp (tendsto_id.const_mul_atTop' zero_lt_two)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (hypothesis)
Goal:
z : ℂ
this : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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)
have this₁ : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
Tactic: have : ContinuousOn (fun x : ℝ ↦ Complex.cos (2 * z * x)) (Icc 0 (π / 2)) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (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)
have h : Eq (α := ℕ → ℂ)
  (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) : ℂ)
Tactic: convert! tendsto_integral_cos_pow_mul_div this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
h :
  Eq (α := ℕ → ℂ)
    (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) : ℂ)
⊢ Tendsto (β := ℂ)
    (fun (n : ℕ) ↦
      (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ))
    atTop (𝓝 1)
have h₁ : 𝓝 1 = 𝓝 (Complex.cos (2 * z * (↑0 : ℂ)))
Tactic: convert! tendsto_integral_cos_pow_mul_div this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
⊢ Eq (α := ℕ → ℂ)
    (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) : ℂ)
have h : ∀ (n : ℕ),
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ) =
    (∫ (x : ℝ) in 0..π / 2, (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
n : ℕ
⊢ (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ) =
    (∫ (x : ℝ) in 0..π / 2, (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ)
have h : ∀ (x : ℝ), Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
Tactic: congr 2 with x : 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (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 : ℂ))
have h : (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ)) = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * (↑0 : ℂ)))
have h : 𝓝 1 = 𝓝 (Complex.cos (2 * z * 0))
Tactic: rw [Complex.ofReal_zero, mul_zero, Complex.cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
h : 𝓝 1 = 𝓝 (Complex.cos (2 * z * 0))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * (↑0 : ℂ)))
have h₁ : 𝓝 1 = 𝓝 (Complex.cos 0)
Tactic: rw [Complex.ofReal_zero, mul_zero, Complex.cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
z : ℂ
this_1 : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)
A :
  Tendsto
    (fun (n : ℕ) ↦
      ((↑π : ℂ) * z *
          ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑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 (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))
h : 𝓝 1 = 𝓝 (Complex.cos (2 * z * 0))
h₁ : 𝓝 1 = 𝓝 (Complex.cos 0)
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * (↑0 : ℂ)))
have h₂ : Eq (α := Filter ℂ) (𝓝 1) (𝓝 1)
Tactic: rw [Complex.ofReal_zero, mul_zero, Complex.cos_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
⊢ Tendsto
    (fun (n : ℕ) ↦
      π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2))
    atTop (𝓝 (sin (π * x)))
have h : Eq (α := ℕ → ℝ)
  (fun (n : ℕ) ↦
    π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2))
  (Complex.re ∘ fun (n : ℕ) ↦
    (↑π : ℂ) * (↑x : ℂ) *
      ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
Tactic: convert! (Complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
h :
  Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2))
    (Complex.re ∘ fun (n : ℕ) ↦
      (↑π : ℂ) * (↑x : ℂ) *
        ∏ j ∈ Finset.range n,
          (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
⊢ Tendsto
    (fun (n : ℕ) ↦
      π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2))
    atTop (𝓝 (sin (π * x)))
have h₁ : 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re
Tactic: convert! (Complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2))
    (Complex.re ∘ fun (n : ℕ) ↦
      (↑π : ℂ) * (↑x : ℂ) *
        ∏ j ∈ Finset.range n,
          (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
have h : ∀ (n : ℕ),
  π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
    (Complex.re ∘ fun (n : ℕ) ↦
        (↑π : ℂ) * (↑x : ℂ) *
          ∏ j ∈ Finset.range n,
            (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
      n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
    (Complex.re ∘ fun (n : ℕ) ↦
        (↑π : ℂ) * (↑x : ℂ) *
          ∏ j ∈ Finset.range n,
            (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
      n
have h : π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
  π * x *
    Complex.re
      (∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
Tactic: rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
n : ℕ
this :
  ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2) =
    (↑(∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2)) : ℂ)
⊢ π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
    π * x *
      Complex.re
        (∏ j ∈ Finset.range n,
          (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
have rw : π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
  π * x *
    (↑(∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2)) :
        ℂ).re
Tactic: rw [this, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
n : ℕ
this :
  ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2) =
    (↑(∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2)) : ℂ)
rw :
  π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
    π * x *
      (↑(∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2)) :
          ℂ).re
⊢ π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
    π * x *
      Complex.re
        (∏ j ∈ Finset.range n,
          (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
have rw₁ : π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
  π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2)
Tactic: rw [this, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2) =
    π * x *
      Complex.re
        (∏ j ∈ Finset.range n,
          (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
have h : ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2) =
  (↑(∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2)) : ℂ)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re
have h : 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑(π * x) : ℂ)).re
Tactic: rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
h : 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑(π * x) : ℂ)).re
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re
have h₁ : 𝓝 (sin (π * x)) = 𝓝 (↑(sin (π * x)) : ℂ).re
Tactic: rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd (goal)
Goal:
x : ℝ
h : 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑(π * x) : ℂ)).re
h₁ : 𝓝 (sin (π * x)) = 𝓝 (↑(sin (π * x)) : ℂ).re
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re
have h₂ : 𝓝 (sin (π * x)) = 𝓝 (sin (π * x))
Tactic: rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
⊢ range arcsin = Icc (-(π / 2)) (π / 2)
have rw : image (α := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
    (range
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))) =
  Icc (-(π / 2)) (π / 2)
Tactic: rw [arcsin, range_comp Subtype.val]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x
have rw : Eq (α := ℝ)
  (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
    (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
    (IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
    (↑(projIcc (-1) 1 sorry x) : ℝ))
  (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
    (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
    (IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
    x)
Tactic: rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw :
  Eq (α := ℝ)
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      (↑(projIcc (-1) 1 ⋯ x) : ℝ))
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      x)
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x
have rw₁ : Eq (α := ℝ)
  (↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
        (↑(projIcc (-1) 1 sorry x) : ℝ)) :
    ℝ)
  (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
    (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
    (IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
    x)
Tactic: rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (goal)
Goal:
x : ℝ
rw :
  Eq (α := ℝ)
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      (↑(projIcc (-1) 1 ⋯ x) : ℝ))
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      x)
rw₁ :
  Eq (α := ℝ)
    (↑(IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type))
          (↑(projIcc (-1) 1 ⋯ x) : ℝ)) :
      ℝ)
    (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
      (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
      (IccExtend arcsin._proof_2
        (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
      x)
⊢ arcsin (↑(projIcc (-1) 1 ⋯ x) : ℝ) = arcsin x
have rw₂ : Eq (α := ℝ)
  (↑((sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)) (projIcc (-1) 1 sorry x)) : ℝ)
  (Function.comp (β := { x : ℝ // x ∈ Icc (-(π / 2)) (π / 2) })
    (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc (-(π / 2)) (π / 2)))
    (IccExtend arcsin._proof_2 (⇑sinOrderIso.symm : (a : (↑(Icc (-1) 1) : Type)) → (↑(Icc (-(π / 2)) (π / 2)) : Type)))
    x)
Tactic: rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
        Function.comp_apply]