awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
inr :
  (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    (↑π : ℂ) * z * A *
        ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ)) /
      (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    ((↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ)) /
      (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
rw :
  (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    (↑π : ℂ) * z * A * ((HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B) /
      ((↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) : ℂ) / (↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) : ℂ) * (↑C : ℂ))
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    (↑π : ℂ) * z * A *
        ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ)) /
      (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)

Tactic:
rw [this, Complex.ofReal_mul, Complex.ofReal_div]

Premises used: Complex.ofReal_div, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
⊢ (↑C : ℂ) ≠ 0

Tactic:
have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this_3 :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
this : (↑C : ℂ) ≠ 0
⊢ HAdd.hAdd (α := ℂ) (↑(2 * n) : ℂ) 1 ≠ 0

Tactic:
(Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)

Premises used: HMul.hMul, Nat.cast_add_one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this_3 :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
this : (↑C : ℂ) ≠ 0
h : HMul.hMul (α := ℂ) 2 (↑n : ℂ) = (↑(2 * n) : ℂ)
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 ≠ 0

Tactic:
convert! (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)

Premises used: HMul.hMul, Nat.cast_add_one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this_3 :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
this : (↑C : ℂ) ≠ 0
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) = (↑(2 * n) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this_3 :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
this : (↑C : ℂ) ≠ 0
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 ≠ 0

Tactic:
have : 2 * (n : ℂ) + 1 ≠ 0 := by
        convert! (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
        simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this_3 :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
this_4 : (↑C : ℂ) ≠ 0
this : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 ≠ 0
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
have : (n : ℂ) + 1 ≠ 0 := Nat.cast_add_one_ne_zero n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this_2 :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
this_3 :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
this_4 : (↑C : ℂ) ≠ 0
this_5 : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 ≠ 0
this : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    (↑π : ℂ) * z * A * ((HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B) /
      ((↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) : ℂ) / (↑(HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) : ℂ) * (↑C : ℂ))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
inr :
  (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B
⊢ (↑π : ℂ) * z * A * B / (↑C : ℂ) =
    (↑π : ℂ) * z * A *
        ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ)) /
      (↑((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C) : ℂ)

Tactic:
suffices
      (((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
          ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
        (2 * n + 1) / (2 * n + 2) * B by
      rw [this, Complex.ofReal_mul, Complex.ofReal_div]
      have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
      have : 2 * (n : ℂ) + 1 ≠ 0 := by
        convert! (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
        simp
      have : (n : ℂ) + 1 ≠ 0 := Nat.cast_add_one_ne_zero n
      simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
⊢ (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n + 2) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)

Tactic:
integral_cos_mul_cos_pow_even n hz

Premises used: EulerSine.integral_cos_mul_cos_pow_even
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
h : (↑n.succ : ℂ) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
⊢ (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1) / (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) * B

Tactic:
convert! integral_cos_mul_cos_pow_even n hz

Premises used: EulerSine.integral_cos_mul_cos_pow_even
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑C : ℂ)
aux' : 2 * n.succ = 2 * n + 2
this_1 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
this :
  (↑π : ℂ) * z * (A * (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ) =
    (↑π : ℂ) * z * A *
      ((1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n.succ : ℂ) 2) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n.succ))
h h₁ : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
⊢ (↑n.succ : ℂ) = HAdd.hAdd (α := ℂ) (↑n : ℂ) 1

Tactic:
rw [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
simp_rw :
  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))
⊢ Tendsto (fun (n : ℕ) ↦ (∫ (x : ℝ) in 0..π / 2, (↑(cos x) : ℂ) ^ n * f x) / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ n) : ℂ))
    atTop (𝓝 (f 0))

Tactic:
simp_rw [div_eq_inv_mul (α := ℂ), ← Complex.ofReal_inv, integral_of_le pi_div_two_pos.le,
    ← MeasureTheory.integral_Icc_eq_integral_Ioc, ← Complex.ofReal_pow, ← Complex.real_smul]

Premises used: Complex.real_smul, Real.pi_div_two_pos, LT.lt.le, intervalIntegral.integral_of_le, div_eq_inv_mul, Complex.ofReal_pow, Complex.ofReal_inv, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
⊢ ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0

Tactic:
have c_lt : ∀ y : ℝ, y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0 := fun y hy hy' =>
    cos_lt_cos_of_nonneg_of_le_pi_div_two (le_refl 0) hy.2 (lt_of_le_of_ne hy.1 hy'.symm)
-- 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
⊢ ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x

Tactic:
have c_nonneg : ∀ x : ℝ, x ∈ Icc 0 (π / 2) → 0 ≤ cos x := fun x hx =>
    cos_nonneg_of_mem_Icc ((Icc_subset_Icc_left (neg_nonpos_of_nonneg pi_div_two_pos.le)) hx)
-- 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
rw : LT.lt (α := ℝ) 0 1
⊢ 0 < cos 0

Tactic:
rw [cos_zero]

Premises used: Real.cos_zero
-- 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
⊢ LT.lt (α := ℝ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- 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
⊢ LT.lt (α := ℝ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- 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
⊢ 0 < cos 0

Tactic:
have c_zero_pos : 0 < cos 0 := by rw [cos_zero]; exact zero_lt_one
-- 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
rw : 0 ≤ π / 2
⊢ 0 ∈ closure (interior (Icc 0 (π / 2)))

Tactic:
rw [interior_Icc, closure_Ioo pi_div_two_pos.ne, left_mem_Icc]

Premises used: Real.pi_div_two_pos, interior_Icc, Set.left_mem_Icc, LT.lt.ne, closure_Ioo
-- 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 ≤ π / 2

Tactic:
pi_div_two_pos.le

Premises used: Real.pi_div_two_pos, LT.lt.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
⊢ 0 ≤ π / 2

Tactic:
exact pi_div_two_pos.le

Premises used: Real.pi_div_two_pos, LT.lt.le