awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ 0 ∈ closure (interior (Icc 0 (π / 2)))

Tactic:
have zero_mem : (0 : ℝ) ∈ closure (interior (Icc 0 (π / 2))) := by
    rw [interior_Icc, closure_Ioo pi_div_two_pos.ne, left_mem_Icc]
    exact pi_div_two_pos.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
c_zero_pos : 0 < cos 0
zero_mem : 0 ∈ closure (interior (Icc 0 (π / 2)))
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := ℂ)
        (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict volume (Icc 0 (π / 2)))
            fun (x : ℝ) ↦ cos x ^ n)⁻¹
        (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict volume (Icc 0 (π / 2)))
          fun (x : ℝ) ↦ cos x ^ n • f x))
    atTop (𝓝 (f 0))

Tactic:
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn isCompact_Icc
      continuousOn_cos c_lt c_nonneg c_zero_pos zero_mem hf

Premises used: Real.continuousOn_cos, CompactIccSpace.isCompact_Icc, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
c_zero_pos : 0 < cos 0
zero_mem : 0 ∈ closure (interior (Icc 0 (π / 2)))
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (α := ℝ) (β := ℂ)
        (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict volume (Icc 0 (π / 2)))
            fun (x : ℝ) ↦ cos x ^ n)⁻¹
        (@MeasureTheory.integral _ _ _ _ measurableSpace (MeasureTheory.Measure.restrict volume (Icc 0 (π / 2)))
          fun (x : ℝ) ↦ cos x ^ n • f x))
    atTop (𝓝 (f 0))

Tactic:
exact
    tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn isCompact_Icc
      continuousOn_cos c_lt c_nonneg c_zero_pos zero_mem hf

Premises used: Real.continuousOn_cos, CompactIccSpace.isCompact_Icc, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
⊢ 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)))

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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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)))
rw rw₁ : 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z))
⊢ 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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)))
⊢ 𝓝 (Complex.sin ((↑π : ℂ) * z)) = 𝓝 (Complex.sin ((↑π : ℂ) * z) * 1)

Tactic:
have : 𝓝 (Complex.sin (π * z)) = 𝓝 (Complex.sin (π * z) * 1) := by rw [mul_one]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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)) *
        ((∫ (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

Premises used: mul_div_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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)))

Tactic:
(tendsto_mul_iff_of_ne_zero _ one_ne_zero).mp A

Premises used: Filter.tendsto_mul_iff_of_ne_zero, Iff.mp, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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))
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)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (↑π : ℂ) * z *
        ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (Complex.sin ((↑π : ℂ) * z)))

Tactic:
convert! (tendsto_mul_iff_of_ne_zero _ one_ne_zero).mp A

Premises used: Filter.tendsto_mul_iff_of_ne_zero, Iff.mp, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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))
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)
⊢ 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:
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)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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))
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) (Icc 0 (π / 2))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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))
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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, (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ))
    atTop (𝓝 (Complex.cos (2 * z * (↑0 : ℂ))))

Tactic:
tendsto_integral_cos_pow_mul_div this

Premises used: EulerSine.tendsto_integral_cos_pow_mul_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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) : ℂ)
h₁ : 𝓝 1 = 𝓝 (Complex.cos (2 * z * (↑0 : ℂ)))
⊢ 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

Premises used: EulerSine.tendsto_integral_cos_pow_mul_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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 :
  ∀ (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) : ℂ)
⊢ 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:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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 : ℕ
h : ∀ (x : ℝ), Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
⊢ (∫ (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:
congr 2 with x : 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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 : ℝ
h h₁ : (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ)) = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
⊢ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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)
h₂ h₃ : Eq (α := Filter ℂ) (𝓝 1) (𝓝 1)
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * (↑0 : ℂ)))

Tactic:
rw [Complex.ofReal_zero, mul_zero, Complex.cos_zero]

Premises used: MulZeroClass.mul_zero, Complex.ofReal_zero, Complex.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
x : ℝ
⊢ Tendsto (α := ℕ)
    (Complex.re ∘ fun (n : ℕ) ↦
      (↑π : ℂ) * (↑x : ℂ) *
        ∏ j ∈ Finset.range n,
          (1 - HPow.hPow (β := ℕ) (↑x : ℂ) 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re)

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

Premises used: Complex.continuous_re, Complex.tendsto_euler_sin_prod, Complex.ofReal, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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))
h₁ : 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re
⊢ Tendsto
    (fun (n : ℕ) ↦
      π * x * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) (↑j : ℝ) 1) 2))
    atTop (𝓝 (sin (π * x)))

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

Premises used: Complex.continuous_re, Complex.tendsto_euler_sin_prod, Complex.ofReal, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
x : ℝ
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
⊢ 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:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
x : ℝ
n : ℕ
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))
⊢ π * 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:
rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.re_ofReal_mul]

Premises used: Function.comp_apply, Complex.ofReal_mul, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
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
rw₁ 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)
⊢ π * 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 [this, Complex.ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
x : ℝ
n : ℕ
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)) : ℂ)
⊢ π * 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:
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]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
x : ℝ
n : ℕ
⊢ ∏ 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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
x : ℝ
h : 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑(π * x) : ℂ)).re
h₁ : 𝓝 (sin (π * x)) = 𝓝 (↑(sin (π * x)) : ℂ).re
h₂ h₃ : 𝓝 (sin (π * x)) = 𝓝 (sin (π * x))
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin ((↑π : ℂ) * (↑x : ℂ))).re

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

Premises used: Complex.ofReal_re, Complex.ofReal_sin, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x ∈ Icc (-(π / 2)) (π / 2)

Tactic:
Subtype.coe_prop _

Premises used: Subtype.coe_prop, Real.arcsin, Set.Mem
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
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)
⊢ range arcsin = Icc (-(π / 2)) (π / 2)

Tactic:
rw [arcsin, range_comp Subtype.val]

Premises used: Set.range_comp, Real.arcsin, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
⊢ 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:
simp [Icc]

Premises used: Set.Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ arcsin x ≤ π / 2

Tactic:
(arcsin_mem_Icc x).2

Premises used: Real.arcsin_mem_Icc, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Goal:
x : ℝ
⊢ -(π / 2) ≤ arcsin x

Tactic:
(arcsin_mem_Icc x).1

Premises used: Real.arcsin_mem_Icc, And.left