awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
⊢ ContDiffOn ℝ (F := ℝ) n (fun (x : E) ↦ Real.sin (f x)) s

Tactic:
Real.contDiff_sin.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Real.contDiff_sin, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x : E) ↦ Real.sin (f x)) s x

Tactic:
Real.contDiff_sin.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Real.contDiff_sin, ContDiffAt.comp_contDiffWithinAt, Real.sin, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
h : ∀ (x : ℂ), logDeriv sin x = x.cot
⊢ logDeriv sin = cot

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : (deriv sin / sin) x = x.cot
h₁ : (cos / sin) x = x.cot
h₂ : cos x / sin x = x.cot
h₃ h₄ : cos x / sin x = cos x / sin x
⊢ logDeriv sin x = x.cot

Tactic:
rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]

Premises used: logDeriv, Pi.div_apply, Complex.cot, Complex.deriv_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
h : ∀ (x : ℝ), logDeriv sin x = x.cot
⊢ logDeriv sin = cot

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
h : (deriv sin / sin) x = x.cot
h₁ : (cos / sin) x = x.cot
h₂ : cos x / sin x = x.cot
h₃ h₄ : cos x / sin x = cos x / sin x
⊢ logDeriv sin x = x.cot

Tactic:
rw [logDeriv, Real.deriv_sin, Pi.div_apply, Real.cot_eq_cos_div_sin]

Premises used: logDeriv, Real.cot_eq_cos_div_sin, Pi.div_apply, Real.deriv_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
h : ∀ (x : ℂ), logDeriv cos x = (-tan) x
⊢ logDeriv cos = -tan

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
h₃ : -sin x / cos x = -tan x
h₄ : -sin x / cos x = -(sin x / cos x)
h₅ h₆ : -(sin x / cos x) = -(sin x / cos x)
⊢ logDeriv cos x = (-tan) x

Tactic:
rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]

Premises used: logDeriv, neg_div, Pi.div_apply, Complex.tan, Complex.deriv_cos', Pi.neg_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
h : ∀ (x : ℝ), logDeriv cos x = (-tan) x
⊢ logDeriv cos = -tan

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
h : (deriv cos / cos) x = (-tan) x
h₁ : HDiv.hDiv (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ -sin x) cos x = (-tan) x
h₂ : -sin x / cos x = (-tan) x
h₃ : -sin x / cos x = -tan x
h₄ : -(sin x / cos x) = -tan x
h₅ h₆ : -(sin x / cos x) = -(sin x / cos x)
⊢ logDeriv cos x = (-tan) x

Tactic:
rw [logDeriv, Real.deriv_cos', Pi.div_apply, Pi.neg_apply, neg_div, Real.tan_eq_sin_div_cos]

Premises used: logDeriv, neg_div, Pi.div_apply, Real.deriv_cos', Pi.neg_apply, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
h : ∀ (x : ℂ), logDeriv cexp x = 1 x
⊢ logDeriv cexp = 1

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : (deriv cexp / cexp) x = 1 x
h₁ : (cexp / cexp) x = 1 x
h₂ : cexp x / cexp x = 1 x
h₃ : cexp (x - x) = 1 x
h₄ : cexp 0 = 1 x
h₅ : Eq (α := ℂ) 1 (1 x)
h₆ h₇ : Eq (α := ℂ) 1 1
⊢ logDeriv cexp x = 1 x

Tactic:
rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]

Premises used: logDeriv, sub_self, Complex.exp_zero, Pi.one_apply, Pi.div_apply, Complex.exp_sub, Complex.deriv_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
h : ∀ (x : ℝ), logDeriv rexp x = 1 x
⊢ logDeriv rexp = 1

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
h : (deriv rexp / rexp) x = 1 x
h₁ : (rexp / rexp) x = 1 x
h₂ : rexp x / rexp x = 1 x
h₃ : rexp (x - x) = 1 x
h₄ : rexp 0 = 1 x
h₅ : Eq (α := ℝ) 1 (1 x)
h₆ h₇ : Eq (α := ℝ) 1 1
⊢ logDeriv rexp x = 1 x

Tactic:
rw [logDeriv, Real.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]

Premises used: logDeriv, sub_self, Pi.one_apply, Real.deriv_exp, Pi.div_apply, Real.exp_zero, Real.exp_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
⊢ HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)

Tactic:
have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
⊢ HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)

Tactic:
have b : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_sin (x * (2 * z))) a
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
⊢ HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑x : ℂ) / (2 * z))
    (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z)) x

Tactic:
have c := b.comp_ofReal.div_const (2 * z)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑x : ℂ) / (2 * z))
    (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z)) x
⊢ HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * 2 * z) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ)))
    x

Tactic:
field_simp at c
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * 2 * z) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ)))
    x
⊢ HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ 2 * z * y) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ)))
    x

Tactic:
simp only [mul_rotate _ 2 z] at c

Premises used: OfNat.ofNat, mul_rotate
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ 2 * z * y) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ)))
    x
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x

Tactic:
c

Premises used: Complex.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * (2 * z)) (Complex.cos ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (x : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ 2 * z * y) (↑x : ℂ) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ)))
    x
⊢ HasDerivAt (fun (y : ℝ) ↦ Complex.sin (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.cos (2 * z * (↑x : ℂ))) x

Tactic:
exact c
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
⊢ HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)

Tactic:
have b : HasDerivAt (Complex.cos ∘ fun y : ℂ => (y * (2 * z))) _ x :=
    HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_cos (x * (2 * z))) a
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
⊢ HasDerivAt (fun (i : ℝ) ↦ -((Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑i : ℂ) / (2 * z)))
    (-(-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z))) x

Tactic:
have c := (b.comp_ofReal.div_const (2 * z)).fun_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (i : ℝ) ↦ -((Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (↑i : ℂ) / (2 * z)))
    (-(-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z) / (2 * z))) x
⊢ HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * (2 * z)) / (2 * z)))
    (-(-(Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) / (2 * z))) x

Tactic:
simp at c ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c :
  HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * (2 * z)) / (2 * z)))
    (-(-(Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) / (2 * z))) x
field_simp :
  ∀ (c : HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * 2 * z) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x),
    HasDerivAt (fun (y : ℝ) ↦ -(Complex.cos (2 * z * (↑y : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x
⊢ HasDerivAt (fun (y : ℝ) ↦ -Complex.cos (2 * z * (↑y : ℂ)) / (2 * z)) (Complex.sin (2 * z * (↑x : ℂ))) x

Tactic:
field_simp at c ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c : HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos ((↑i : ℂ) * 2 * z) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x
⊢ HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos (2 * z * (↑i : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x

Tactic:
simp only [mul_rotate _ 2 z] at c

Premises used: OfNat.ofNat, mul_rotate
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c : HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos (2 * z * (↑i : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x
⊢ HasDerivAt (fun (y : ℝ) ↦ -(Complex.cos (2 * z * (↑y : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x

Tactic:
c
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun (y : ℂ) ↦ y * (2 * z)) (2 * z) (↑x : ℂ)
b : HasDerivAt (Complex.cos ∘ fun (y : ℂ) ↦ y * (2 * z)) (-Complex.sin ((↑x : ℂ) * (2 * z)) * (2 * z)) (↑x : ℂ)
c : HasDerivAt (fun (i : ℝ) ↦ -(Complex.cos (2 * z * (↑i : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x
⊢ HasDerivAt (fun (y : ℝ) ↦ -(Complex.cos (2 * z * (↑y : ℂ)) / (2 * z))) (Complex.sin (2 * z * (↑x : ℂ))) x

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

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

Tactic:
simpa using (hasDerivAt_cos x).ofReal_comp

Premises used: Real.hasDerivAt_cos, HasDerivAt.ofReal_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ)) (-(↑(sin x) : ℂ)) x

Tactic:
have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
      simpa using (hasDerivAt_cos x).ofReal_comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ)) (-(↑(sin x) : ℂ)) x
⊢ HasDerivAt ((fun (x : ℂ) ↦ x ^ n) ∘ fun (y : ℝ) ↦ (↑(cos y) : ℂ))
    ((↑n : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * -(↑(sin x) : ℂ)) x

Tactic:
HasDerivAt.comp x (hasDerivAt_pow _ _) b

Premises used: HasDerivAt.comp, hasDerivAt_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h_1 : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ)) (-(↑(sin x) : ℂ)) x
h : -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) = (↑n : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * -(↑(sin x) : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x

Tactic:
convert! HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1

Premises used: HasDerivAt.comp, hasDerivAt_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
h : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ)) (-(↑(sin x) : ℂ)) x
⊢ -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) = (↑n : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * -(↑(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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x

Tactic:
have der1 :
    ∀ x : ℝ,
      x ∈ uIcc 0 (π / 2) →
        HasDerivAt (fun y : ℝ => (cos y : ℂ) ^ n) (-n * sin x * (cos x : ℂ) ^ (n - 1)) x := by
    intro x _
    have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
      simpa using (hasDerivAt_cos x).ofReal_comp
    convert! HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
    ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0..π / 2, (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ)) =
    (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))

Tactic:
integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _

Premises used: intervalIntegral.integral_mul_deriv_eq_deriv_mul, EulerSine.antideriv_cos_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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h :
  Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
h₁ :
  (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))
convert_1 :
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) volume 0 (π / 2)
convert_2 : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ))) volume 0 (π / 2)
⊢ ∫ (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:
convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2

Premises used: intervalIntegral.integral_mul_deriv_eq_deriv_mul, EulerSine.antideriv_cos_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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h : ∀ (x : ℝ), Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n = (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))
⊢ Eq (α := ℝ → ℂ) (fun (x : ℝ) ↦ Complex.cos (2 * z * (↑x : ℂ)) * (↑(cos x) : ℂ) ^ n) fun (x : ℝ) ↦
    (↑(cos x) : ℂ) ^ n * Complex.cos (2 * z * (↑x : ℂ))

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

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ n ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
Goal:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun (y : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h :
  Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)))
    (∫ (x : ℝ) in 0..π / 2,
      -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))))
⊢ (↑n : ℂ) / (2 * z) *
      ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) =
    (↑(cos (π / 2)) : ℂ) ^ n * (Complex.sin (2 * z * (↑(π / 2) : ℂ)) / (2 * z)) -
        (↑(cos 0) : ℂ) ^ n * (Complex.sin (2 * z * (↑0 : ℂ)) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))

Tactic:
rw [Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div, mul_zero, sub_zero,
      cos_pi_div_two, Complex.ofReal_zero, zero_pow (by positivity : n ≠ 0), zero_mul, zero_sub,
      ← integral_neg, ← integral_const_mul]

Premises used: sub_zero, MulZeroClass.zero_mul, zero_div, Real.cos_pi_div_two, MulZeroClass.mul_zero, Complex.ofReal_zero, Complex.sin_zero, 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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)))
    (∫ (x : ℝ) in 0..π / 2,
      -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
h :
  ∀ x ∈ uIcc 0 (π / 2),
    (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) =
      -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z)))
⊢ Eq (α := ℂ)
    (∫ (x : ℝ) in 0..π / 2,
      (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)))
    (∫ (x : ℝ) in 0..π / 2,
      -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z))))

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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
x : ℝ
h : x ∈ uIcc 0 (π / 2)
⊢ (↑n : ℂ) / (2 * z) * (Complex.sin (2 * z * (↑x : ℂ)) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) =
    -(-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1) * (Complex.sin (2 * z * (↑x : ℂ)) / (2 * z)))

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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)

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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) 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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ Complex.cos (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 : ℝ) ↦ (↑(cos y) : ℂ) ^ n) (-(↑n : ℂ) * (↑(sin x) : ℂ) * (↑(cos x) : ℂ) ^ (n - 1)) x
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ Complex.cos (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
x : ℝ
_ :
  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 ∈ 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:
_