awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ π / 2 = π / 2 - 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2 - 0, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)

Tactic:
nth_rw 3 [(by ring : π / 2 = π / 2 - 0)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos (π / 2 - x) ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in π / 2 - π / 2..π / 2 - 0, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)

Tactic:
rw [← integral_comp_sub_left]

Premises used: intervalIntegral.integral_comp_sub_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos (π / 2 - x) ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)

Tactic:
integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : ∀ x ∈ uIcc 0 (π / 2), cos (π / 2 - x) ^ n = sin x ^ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos (π / 2 - x) ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)

Tactic:
refine integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
x : ℝ
h : x ∈ uIcc 0 (π / 2)
e_a e_a₁ : sin x ^ n = sin x ^ n
⊢ cos (π / 2 - x) ^ n = sin x ^ n

Tactic:
rw [cos_pi_div_two_sub]

Premises used: Real.cos_pi_div_two_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ π = π / 2 + π / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π / 2 + π / 2, sin x ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)

Tactic:
nth_rw 3 [(by ring : π = π / 2 + π / 2)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ π / 2 = 0 + π / 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0 + π / 2..π / 2 + π / 2, sin x ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π / 2 + π / 2, sin x ^ n)

Tactic:
nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0 + π / 2..π / 2 + π / 2, sin x ^ n)

Tactic:
rw [← integral_comp_add_right]

Premises used: intervalIntegral.integral_comp_add_right
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n)

Tactic:
integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
e_a : ∀ x ∈ uIcc 0 (π / 2), cos x ^ n = sin (x + π / 2) ^ n
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n)

Tactic:
refine integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π
x : ℝ
h : x ∈ uIcc 0 (π / 2)
e_a e_a₁ : cos x ^ n = cos x ^ n
⊢ cos x ^ n = sin (x + π / 2) ^ n

Tactic:
rw [sin_add_pi_div_two]

Premises used: Real.sin_add_pi_div_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
⊢ LT.lt (α := ℝ) 0 (∫ (x : ℝ) in 0..π / 2, cos x ^ n)

Tactic:
(integral_cos_pow_eq n).symm ▸ mul_pos one_half_pos (integral_sin_pow_pos _)

Premises used: integral_sin_pow_pos, Eq.rec, mul_pos, EulerSine.integral_cos_pow_eq, one_half_pos, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
inl :
  Complex.sin ((↑π : ℂ) * 0) =
    (((↑π : ℂ) * 0 *
          ∏ j ∈ Finset.range n,
            (1 - HPow.hPow (α := ℂ) (β := ℕ) 0 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (HMul.hMul (α := ℂ) 2 0 * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
inr :
  ∀ (hz : z ≠ 0),
    Complex.sin ((↑π : ℂ) * z) =
      (((↑π : ℂ) * 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)) : ℂ)
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * 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)) : ℂ)

Tactic:
rcases eq_or_ne z 0 with (rfl | hz)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
⊢ Complex.sin ((↑π : ℂ) * 0) =
    (((↑π : ℂ) * 0 *
          ∏ j ∈ Finset.range n,
            (1 - HPow.hPow (α := ℂ) (β := ℕ) 0 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (HMul.hMul (α := ℂ) 2 0 * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
inr :
  Complex.sin ((↑π : ℂ) * z) = ((↑π : ℂ) * z * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ))) / (↑(π / 2) : ℂ)
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range 0, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ HMul.hMul (α := ℕ) 2 0) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ HMul.hMul (α := ℕ) 2 0) : ℂ)

Tactic:
simp_rw [mul_zero, pow_zero, mul_one, Finset.prod_range_zero, mul_one,
      integral_one, sub_zero]

Premises used: sub_zero, pow_zero, MulZeroClass.mul_zero, Finset.prod_range_zero, integral_one, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
push_cast : 2 * z * ((↑π : ℂ) / 2) = (↑π : ℂ) * z
⊢ 2 * z * (↑(π / 2) : ℂ) = (↑π : ℂ) * z

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ((↑π : ℂ) / 2) = (↑π : ℂ) * z

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
inr : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * (Complex.sin ((↑π : ℂ) * z) / (2 * z)) / (↑(π / 2) : ℂ)
⊢ Complex.sin ((↑π : ℂ) * z) = ((↑π : ℂ) * z * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ))) / (↑(π / 2) : ℂ)

Tactic:
rw [integral_cos_mul_complex (mul_ne_zero two_ne_zero hz), Complex.ofReal_zero,
      mul_zero, Complex.sin_zero, zero_div, sub_zero,
      (by push_cast; ring : 2 * z * ↑(π / 2) = π * z)]

Premises used: sub_zero, zero_div, MulZeroClass.mul_zero, two_ne_zero, Complex.ofReal_zero, Complex.sin_zero, mul_ne_zero, integral_cos_mul_complex
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
⊢ Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * (Complex.sin ((↑π : ℂ) * z) / (2 * z)) / (↑(π / 2) : ℂ)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * 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)) : ℂ)
inr :
  (((↑π : ℂ) * 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)) : ℂ) =
    ((↑π : ℂ) * z *
          ((∏ x ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1) 2)) *
            (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 + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)
⊢ Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * z *
          ∏ j ∈ Finset.range (n + 1),
            (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 + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)

Tactic:
rw [hn, Finset.prod_range_succ]

Premises used: Finset.prod_range_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin ((↑π : ℂ) * z) =
    (((↑π : ℂ) * 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)) : ℂ)
inr :
  let A : ℂ :=
    ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2);
  ∀
    (hn :
      Complex.sin ((↑π : ℂ) * z) =
        ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
          (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)),
    ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
      ((↑π : ℂ) * 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 + 1))) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)
⊢ (((↑π : ℂ) * 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)) : ℂ) =
    ((↑π : ℂ) * z *
          ((∏ x ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1) 2)) *
            (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 + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)

Tactic:
set A := ∏ j ∈ Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)

Premises used: Finset.range
-- 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)
hn :
  Complex.sin ((↑π : ℂ) * z) =
    ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
inr :
  let B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n);
  ∀ (hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)),
    (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
      ((↑π : ℂ) * 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 + 1))) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)
⊢ ((↑π : ℂ) * z * A * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (2 * n)) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
    ((↑π : ℂ) * 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 + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)

Tactic:
set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)

Premises used: HMul.hMul, 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)
hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ)
inr :
  let C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n);
  ∀ (hn : Complex.sin ((↑π : ℂ) * z) = (↑π : ℂ) * z * A * B / (↑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 + 1))) /
        (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)
⊢ (↑π : ℂ) * z * A * B / (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)) : ℂ) =
    ((↑π : ℂ) * 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 + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)

Tactic:
set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)

Premises used: HMul.hMul, 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 : ℂ)
rw : 2 * (n + 1) = 2 * n + 2
rw₁ : 2 * n + HMul.hMul (α := ℕ) 2 1 = 2 * n + 2
rw₂ rw₃ : 2 * n + 2 = 2 * n + 2
⊢ 2 * n.succ = 2 * n + 2

Tactic:
rw [Nat.succ_eq_add_one, mul_add, mul_one]

Premises used: Nat.succ_eq_add_one, mul_add, mul_one
-- 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 : ℂ)
⊢ 2 * n.succ = 2 * n + 2

Tactic:
have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
-- 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
rw :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C

Tactic:
rw [integral_cos_pow_eq]

Premises used: EulerSine.integral_cos_pow_eq
-- 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
dsimp :
  1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C

Tactic:
dsimp only [C]
-- 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
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C

Tactic:
have : (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n.succ)) = (2 * (n : ℝ) + 1) / (2 * n + 2) * C := by
      rw [integral_cos_pow_eq]
      dsimp only [C]
      rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ',
        zero_mul, zero_mul, zero_mul, sub_zero, zero_div,
        zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_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 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * C
inr :
  (↑π : ℂ) * 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 + 1))) /
      (↑((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 + 1))) /
      (↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * (n + 1))) : ℂ)

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 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * 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) =
    (↑π : ℂ) * 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))

Tactic:
grind
-- 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 :
  ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) =
    (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) * 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) =
    (↑π : ℂ) * 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))

Tactic:
have :
      (π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
          ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
        π * z * A *
          (((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
            ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) := by
      grind