awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
h :
  ((↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2))) /
      (2 * z) =
    -((Complex.cos (↑x : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
              Complex.cos (↑x : ℂ) ^ (n - 2)) *
          -Complex.cos (2 * z * (↑x : ℂ))) /
      (2 * z)
⊢ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)) =
    -(((↑(cos x) : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
        (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z)))

Tactic:
rw [Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq, ← mul_div_right_comm, ←
      mul_div_right_comm, ← sub_div, mul_div, ← neg_div]

Premises used: mul_div, neg_div, sub_div, mul_div_right_comm, Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
h :
  (↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
    -((Complex.cos (↑x : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ)))
⊢ ((↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2))) /
      (2 * z) =
    -((Complex.cos (↑x : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
              Complex.cos (↑x : ℂ) ^ (n - 2)) *
          -Complex.cos (2 * z * (↑x : ℂ))) /
      (2 * z)

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h : x ∈ uIcc 0 (π / 2)
rw : Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
| Complex.cos (↑x : ℂ) ^ n

Tactic:
rw [← Nat.sub_add_cancel hn, pow_add]

Premises used: pow_add, Nat.sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h : x ∈ uIcc 0 (π / 2)
conv_lhs : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
conv_lhs₁ :
  Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2 =
    Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2

Tactic:
conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]

Premises used: pow_add, Nat.sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2

Tactic:
have : Complex.cos x ^ n = Complex.cos x ^ (n - 2) * Complex.cos x ^ 2 := by
      conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
this : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
h :
  (↑n : ℂ) *
        (Complex.cos (2 * z * (↑x : ℂ)) *
          (Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2)) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
    -((Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2 -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ)))
⊢ (↑n : ℂ) * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
    -((Complex.cos (↑x : ℂ) ^ n -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ)))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
x : ℝ
h : x ∈ uIcc 0 (π / 2)
this : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2
⊢ (↑n : ℂ) *
        (Complex.cos (2 * z * (↑x : ℂ)) *
          (Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2)) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (Complex.cos (2 * z * (↑x : ℂ)) * Complex.cos (↑x : ℂ) ^ (n - 2)) =
    -((Complex.cos (↑x : ℂ) ^ (n - 2) * HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2 -
          HSub.hSub (α := ℂ) (↑n : ℂ) 1 * (1 - HPow.hPow (β := ℕ) (Complex.cos (↑x : ℂ)) 2) *
            Complex.cos (↑x : ℂ) ^ (n - 2)) *
        -Complex.cos (2 * z * (↑x : ℂ)))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n - HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
⊢ IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦
      (↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    volume 0 (π / 2)

Tactic:
apply Continuous.intervalIntegrable <| by fun_prop

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ Complex.sin (2 * z * (↑x : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1))
      ((↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
      x
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.sin (2 * z * (↑x : ℂ))) volume 0 (π / 2)

Tactic:
apply Continuous.intervalIntegrable <| by fun_prop

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
contrapose! : ∀ (hn : Eq (α := ℂ) (↑n : ℂ) 0), n < 2
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
contrapose! hn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : Eq (α := ℂ) (↑n : ℂ) 0
⊢ n = 0

Tactic:
rw [Nat.cast_eq_zero] at hn

Premises used: Nat.cast_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
rw : LT.lt (α := ℕ) 0 2
⊢ n < 2

Tactic:
rw [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ LT.lt (α := ℕ) 0 2

Tactic:
zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ LT.lt (α := ℕ) 0 2

Tactic:
exact zero_lt_two

Premises used: zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
have nne : (n : ℂ) ≠ 0 := by
    contrapose! hn; rw [Nat.cast_eq_zero] at hn; rw [hn]; exact zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)

Tactic:
have := integral_cos_mul_cos_pow_aux hn hz
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)
⊢ (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))

Tactic:
rw [integral_sin_mul_sin_mul_cos_pow_eq hn hz, sub_eq_neg_add, mul_add, ← sub_eq_iff_eq_add]
    at this

Premises used: sub_eq_neg_add, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, sub_eq_iff_eq_add, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
⊢ Eq (α := ℂ)
    ((fun (u : ℂ) ↦ -u * HPow.hPow (β := ℕ) (2 * z) 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
      ((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
        (↑n : ℂ) / (2 * z) *
          ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n)))
    ((fun (u : ℂ) ↦ -u * HPow.hPow (β := ℕ) (2 * z) 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)
      ((↑n : ℂ) / (2 * z) *
        -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
            ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))))

Tactic:
congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, congr_arg, HPow.hPow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
h :
  (1 - 4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    -((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
            (↑n : ℂ) / (2 * z) *
              ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n)) *
        HPow.hPow (β := ℕ) (2 * z) 2 /
      HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
h₁ :
  HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (↑n : ℂ) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2) =
    -((↑n : ℂ) / (2 * z) *
            -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
                ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))) *
        HPow.hPow (β := ℕ) (2 * z) 2 /
      HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2
⊢ (1 - 4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (↑n : ℂ) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)

Tactic:
convert! congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this using 1

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, congr_arg, HPow.hPow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
⊢ (1 - 4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n =
    -((∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
            (↑n : ℂ) / (2 * z) *
              ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n)) *
        HPow.hPow (β := ℕ) (2 * z) 2 /
      HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : Ne (α := ℂ) (↑n : ℂ) 0
this :
  (∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      (↑n : ℂ) / (2 * z) *
        ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) =
    (↑n : ℂ) / (2 * z) *
      -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))
⊢ HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (↑n : ℂ) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2) =
    -((↑n : ℂ) / (2 * z) *
            -(HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
                ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2))) *
        HPow.hPow (β := ℕ) (2 * z) 2 /
      HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ 2 ≤ 2 * n + 2

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h :
  HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑(2 * n + 2) : ℂ) 2
h₁ : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HSub.hSub (α := ℂ) (↑(2 * n + 2) : ℂ) 1
h₂ : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = (↑(2 * n + 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 + 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:
convert! integral_cos_mul_cos_pow (by lia : 2 ≤ 2 * n + 2) hz using 3

Premises used: EulerSine.integral_cos_mul_cos_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h :
  HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) 2
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) (↑(2 * n + 2) : ℂ) 2

Tactic:
simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_two]

Premises used: Nat.cast_add, Nat.cast_mul, Nat.cast_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h :
  HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + HMul.hMul (α := ℂ) 2 1) 2
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2) 2

Tactic:
nth_rw 2 [← mul_one (2 : ℂ)]

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h :
  HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) 2 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HMul.hMul (α := ℂ) 2 (↑n : ℂ) + HMul.hMul (α := ℂ) 2 1) 2

Tactic:
rw [← mul_add, mul_pow, ← div_div]

Premises used: mul_add, div_div, mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 =
    4 * HPow.hPow (β := ℕ) z 2 / HPow.hPow (α := ℂ) (β := ℕ) 2 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 - 1
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HSub.hSub (α := ℂ) (↑(2 * n + 2) : ℂ) 1

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1 = HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 - 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
h : HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = (↑(2 * n + 2) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2 = HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    ∫ (x : ℝ) in 0..π, sin x ^ n
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
rw [mul_comm (1 / 2 : ℝ), ← div_eq_iff (one_div_ne_zero (two_ne_zero' ℝ)), ← div_mul, div_one,
    mul_two]

Premises used: Real, HDiv.hDiv, div_mul, two_ne_zero', div_eq_iff, mul_comm, OfNat.ofNat, div_one, mul_two, one_div_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
⊢ IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)

Tactic:
have L : IntervalIntegrable _ volume 0 (π / 2) := (continuous_sin.pow n).intervalIntegrable _ _
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
n : ℕ
L : IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume 0 (π / 2)
⊢ IntervalIntegrable (ε := ℝ) (fun (b : ℝ) ↦ sin b ^ n) volume (π / 2) π

Tactic:
have R : IntervalIntegrable _ volume (π / 2) π := (continuous_sin.pow n).intervalIntegrable _ _
-- 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) π
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, sin x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
rw [← integral_add_adjacent_intervals L R]

Premises used: intervalIntegral.integral_add_adjacent_intervals
-- 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 ^ n)
e_a₁ : Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 0..π / 2, sin x ^ n) (∫ (x : ℝ) in π / 2..π, sin x ^ n)

Tactic:
congr 1
-- 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) π
⊢ 0 = π / 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 π / 2 - π / 2..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..π / 2, cos x ^ n) (∫ (x : ℝ) in 0..π / 2, sin x ^ n)

Tactic:
nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]