awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)

Tactic:
have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (↑y : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑y : ℂ))
    (Complex.cos (↑x : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑x : ℂ) +
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)))
    x

Tactic:
((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal

Premises used: HasDerivAt.comp_ofReal, Complex.ofReal, Complex.hasDerivAt_sin, HasDerivAt.fun_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
h :
  Eq (α := ℝ → ℂ) (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1)) fun (y : ℝ) ↦
    Complex.sin (↑y : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑y : ℂ)
h₁ :
  (↑(cos x) : ℂ) ^ n - HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2) =
    Complex.cos (↑x : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑x : ℂ) +
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ))
⊢ 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

Tactic:
convert! ((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal using 1

Premises used: HasDerivAt.comp_ofReal, Complex.ofReal, Complex.hasDerivAt_sin, HasDerivAt.fun_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ Eq (α := ℝ → ℂ) (fun (y : ℝ) ↦ (↑(sin y) : ℂ) * (↑(cos y) : ℂ) ^ (n - 1)) fun (y : ℝ) ↦
    Complex.sin (↑y : ℂ) * ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos) (↑y : ℂ)

Tactic:
simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]

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

Tactic:
simp only [Complex.ofReal_cos, Complex.ofReal_sin]

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

Tactic:
rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]

Premises used: sub_eq_add_neg, Function.comp_apply, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
h : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1)
h₁ :
  HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))
⊢ Complex.cos (↑x : ℂ) ^ n -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1) -
      Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))

Tactic:
congr 1
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
h : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ (n - 1 + 1)
h₁ h₂ : Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) ^ n
⊢ Complex.cos (↑x : ℂ) ^ n = Complex.cos (↑x : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1)

Tactic:
rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]

Premises used: Nat.sub_add_cancel, pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
rw : HSub.hSub (α := ℂ) (↑n : ℂ) (↑1 : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
rw₁ rw₂ : HSub.hSub (α := ℂ) (↑n : ℂ) 1 = HSub.hSub (α := ℂ) (↑n : ℂ) 1
⊢ (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1

Tactic:
rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]

Premises used: Nat.cast_sub, one_le_two, LE.le.trans, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
⊢ (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1

Tactic:
have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by
          rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
c :
  HasDerivAt ((fun (x : ℂ) ↦ x ^ (n - 1)) ∘ Complex.cos)
    ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * -Complex.sin (↑x : ℂ)) (↑x : ℂ)
this : (↑(n - 1) : ℂ) = HSub.hSub (α := ℂ) (↑n : ℂ) 1
h :
  HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.sin (↑x : ℂ) *
      (HSub.hSub (α := ℂ) (↑n : ℂ) 1 * Complex.cos (↑x : ℂ) ^ (n - HAdd.hAdd (α := ℕ) 1 1) * Complex.sin (↑x : ℂ))
⊢ HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (Complex.sin (↑x : ℂ)) 2 * Complex.cos (↑x : ℂ) ^ (n - 2) =
    Complex.sin (↑x : ℂ) * ((↑(n - 1) : ℂ) * Complex.cos (↑x : ℂ) ^ (n - 1 - 1) * Complex.sin (↑x : ℂ))

Tactic:
rw [Nat.sub_sub, this]

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

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∀ 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

Tactic:
have der1 :
    ∀ x : ℝ,
      x ∈ uIcc 0 (π / 2) →
        HasDerivAt (fun y : ℝ => sin y * (cos y : ℂ) ^ (n - 1))
          ((cos x : ℂ) ^ n - (n - 1) * (sin x : ℂ) ^ 2 * (cos x : ℂ) ^ (n - 2)) x := by
    intro x _
    have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
    convert! ((Complex.hasDerivAt_sin x).fun_mul c).comp_ofReal using 1
    · simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]
    · simp only [Complex.ofReal_cos, Complex.ofReal_sin]
      rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
      congr 1
      · rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]
      · have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by
          rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
        rw [Nat.sub_sub, this]
        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
⊢ ∫ (x : ℝ) in 0..π / 2, (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ)) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 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:
integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _

Premises used: intervalIntegral.integral_mul_deriv_eq_deriv_mul, EulerSine.antideriv_sin_comp_const_mul
-- 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
h :
  Eq (α := ℂ) (∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1))
    (∫ (x : ℝ) in 0..π / 2, (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ)))
h₁ :
  ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        ((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))
convert_1 :
  IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦
      (↑(cos x) : ℂ) ^ n -
        HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2))
    volume 0 (π / 2)
convert_2 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.sin (2 * z * (↑x : ℂ))) volume 0 (π / 2)
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)

Tactic:
convert!
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1

Premises used: intervalIntegral.integral_mul_deriv_eq_deriv_mul, EulerSine.antideriv_sin_comp_const_mul
-- 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
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1))
    (∫ (x : ℝ) in 0..π / 2, (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ)))

Tactic:
integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- 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
h :
  ∀ x ∈ uIcc 0 (π / 2),
    Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
      (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ))
⊢ Eq (α := ℂ) (∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1))
    (∫ (x : ℝ) in 0..π / 2, (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ)))

Tactic:
refine integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- 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.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * Complex.sin (2 * z * (↑x : ℂ))

Tactic:
ring_nf
-- 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
h :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑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)))
    (∫ (x : ℝ) in 0..π / 2,
      -(((↑(cos x) : ℂ) ^ n -
            HSub.hSub (α := ℂ) (↑n : ℂ) 1 * HPow.hPow (β := ℕ) (↑(sin x) : ℂ) 2 * (↑(cos x) : ℂ) ^ (n - 2)) *
          (-Complex.cos (2 * z * (↑x : ℂ)) / (2 * z))))
h₁ :
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n))
    volume 0 (π / 2)
h₂ :
  IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2)))
    volume 0 (π / 2)
h₃ : n - 1 ≠ 0
⊢ ((↑n : ℂ) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) -
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ (n - 2) =
    (↑(sin (π / 2)) : ℂ) * (↑(cos (π / 2)) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(sin 0) : ℂ) * (↑(cos 0) : ℂ) ^ (n - 1) * (-Complex.cos (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 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 [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul,
      mul_zero, zero_mul, zero_mul, sub_zero, zero_sub, ←
      integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]

Premises used: sub_zero, MulZeroClass.zero_mul, Real.sin_zero, Real.cos_pi_div_two, MulZeroClass.mul_zero, Complex.ofReal_zero, intervalIntegral.integral_sub, zero_pow, intervalIntegral.integral_neg, zero_sub, intervalIntegral.integral_const_mul
-- 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 : ℝ) ↦ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n)

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 : ℝ) ↦ (↑n : ℂ) / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n))
    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 : ℝ) ↦
    HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(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 : ℝ) ↦
      HSub.hSub (α := ℂ) (↑n : ℂ) 1 / (2 * z) * (Complex.cos (2 * z * (↑x : ℂ)) * (↑(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
⊢ n - 1 ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt hn

Premises used: Nat.sub_ne_zero_of_lt
-- 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
⊢ n - 1 ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt hn

Premises used: Nat.sub_ne_zero_of_lt
-- 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
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑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)))
    (∫ (x : ℝ) in 0..π / 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:
integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr
-- 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
h :
  ∀ x ∈ uIcc 0 (π / 2),
    (↑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)))
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑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)))
    (∫ (x : ℝ) in 0..π / 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:
refine integral_congr fun x _ => ?_

Premises used: intervalIntegral.integral_congr