awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹

Tactic:
simp only [id]

Premises used: id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ HasDerivAt cos (-sin x) x

Tactic:
(hasStrictDerivAt_cos x).hasDerivAt

Premises used: Complex.hasStrictDerivAt_cos, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℂ n cos

Tactic:
((contDiff_id.mul contDiff_const).cexp.add (contDiff_neg.mul contDiff_const).cexp).div_const _

Premises used: ContDiff.div_const, contDiff_id, Complex.cos, ContDiff.cexp, contDiff_const, contDiff_neg, ContDiff.add, ContDiff.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ Differentiable ℂ cos

Tactic:
fun x => (hasDerivAt_cos x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Complex.hasDerivAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ DifferentiableAt ℂ cos x

Tactic:
differentiable_cos x

Premises used: Complex.differentiable_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ AnalyticAt ℂ cos x

Tactic:
contDiff_cos.contDiffAt.analyticAt

Premises used: ContDiffAt.analyticAt, Complex.contDiff_cos, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
s : Set ℂ
⊢ AnalyticWithinAt ℂ cos s x

Tactic:
contDiff_cos.contDiffWithinAt.analyticWithinAt

Premises used: ContDiff.contDiffWithinAt, Complex.contDiff_cos, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℂ
⊢ AnalyticOnNhd ℂ cos s

Tactic:
fun _ _ ↦ analyticAt_cos

Premises used: AnalyticOnNhd, Complex.analyticAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℂ
⊢ AnalyticOn ℂ cos s

Tactic:
contDiff_cos.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, ContDiffOn.analyticOn, Complex.contDiff_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ deriv cos x = -sin x

Tactic:
(hasDerivAt_cos x).deriv

Premises used: HasDerivAt.deriv, Complex.hasDerivAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ deriv cos = fun (x : ℂ) ↦ -sin x

Tactic:
funext fun _ => deriv_cos

Premises used: Complex.deriv_cos, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
f' x : ℂ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ Complex.cos (f x)) (-Complex.sin (f x) * f') x

Tactic:
(Complex.hasStrictDerivAt_cos (f x)).comp x hf

Premises used: Complex.cos, Complex.hasStrictDerivAt_cos, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
f' x : ℂ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℂ) ↦ Complex.cos (f x)) (-Complex.sin (f x) * f') x

Tactic:
(Complex.hasDerivAt_cos (f x)).comp x hf

Premises used: Complex.cos, HasDerivAt.comp, Complex.hasDerivAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ Complex.cos (f x)) (-Complex.sin (f x) * f') s x

Tactic:
(Complex.hasDerivAt_cos (f x)).comp_hasDerivWithinAt x hf

Premises used: Complex.cos, Complex.hasDerivAt_cos, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
x : ℂ
s : Set ℂ
hf : DifferentiableWithinAt ℂ f s x
hxs : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun (x : ℂ) ↦ Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.ccos.derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.ccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
x : ℂ
hc : DifferentiableAt ℂ f x
⊢ deriv (fun (x : ℂ) ↦ Complex.cos (f x)) x = -Complex.sin (f x) * deriv f x

Tactic:
hc.hasDerivAt.ccos.deriv

Premises used: HasDerivAt.ccos, DifferentiableAt.hasDerivAt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
f' x : ℂ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ Complex.sin (f x)) (Complex.cos (f x) * f') x

Tactic:
(Complex.hasStrictDerivAt_sin (f x)).comp x hf

Premises used: Complex.sin, Complex.hasStrictDerivAt_sin, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
f' x : ℂ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℂ) ↦ Complex.sin (f x)) (Complex.cos (f x) * f') x

Tactic:
(Complex.hasDerivAt_sin (f x)).comp x hf

Premises used: Complex.sin, HasDerivAt.comp, Complex.hasDerivAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ Complex.sin (f x)) (Complex.cos (f x) * f') s x

Tactic:
(Complex.hasDerivAt_sin (f x)).comp_hasDerivWithinAt x hf

Premises used: Complex.sin, Complex.hasDerivAt_sin, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
x : ℂ
s : Set ℂ
hf : DifferentiableWithinAt ℂ f s x
hxs : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun (x : ℂ) ↦ Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.csin.derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.csin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℂ → ℂ
x : ℂ
hc : DifferentiableAt ℂ f x
⊢ deriv (fun (x : ℂ) ↦ Complex.sin (f x)) x = Complex.cos (f x) * deriv f x

Tactic:
hc.hasDerivAt.csin.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.csin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ Complex.cos (f x)) (-Complex.sin (f x) • f') x

Tactic:
(Complex.hasStrictDerivAt_cos (f x)).comp_hasStrictFDerivAt x hf

Premises used: Complex.cos, Complex.hasStrictDerivAt_cos, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : E) ↦ Complex.cos (f x)) (-Complex.sin (f x) • f') x

Tactic:
(Complex.hasDerivAt_cos (f x)).comp_hasFDerivAt x hf

Premises used: Complex.cos, Complex.hasDerivAt_cos, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ Complex.cos (f x)) (-Complex.sin (f x) • f') s x

Tactic:
(Complex.hasDerivAt_cos (f x)).comp_hasFDerivWithinAt x hf

Premises used: Complex.cos, HasDerivAt.comp_hasFDerivWithinAt, Complex.hasDerivAt_cos
-- 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
hf : DifferentiableWithinAt ℂ f s x
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (x : E) ↦ Complex.cos (f x)) s x

Tactic:
hf.hasFDerivWithinAt.ccos.differentiableWithinAt

Premises used: HasFDerivWithinAt.ccos, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
hc : DifferentiableAt ℂ f x
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : E) ↦ Complex.cos (f x)) x

Tactic:
hc.hasFDerivAt.ccos.differentiableAt

Premises used: HasFDerivAt.ccos, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
hc : DifferentiableOn ℂ f s
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : E) ↦ Complex.cos (f x)) s

Tactic:
fun x h => (hc x h).ccos

Premises used: DifferentiableOn, DifferentiableWithinAt.ccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
hc : Differentiable ℂ f
⊢ Differentiable ℂ (F := ℂ) fun (x : E) ↦ Complex.cos (f x)

Tactic:
fun x => (hc x).ccos

Premises used: Differentiable, DifferentiableAt.ccos
-- 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
hf : DifferentiableWithinAt ℂ f s x
hxs : UniqueDiffWithinAt ℂ s x
⊢ fderivWithin ℂ (fun (x : E) ↦ Complex.cos (f x)) s x =
    HSMul.hSMul (β := E →L[ℂ] ℂ) (-Complex.sin (f x)) (fderivWithin ℂ f s x)

Tactic:
hf.hasFDerivWithinAt.ccos.fderivWithin hxs

Premises used: HasFDerivWithinAt.ccos, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
hc : DifferentiableAt ℂ f x
⊢ fderiv ℂ (fun (x : E) ↦ Complex.cos (f x)) x = HSMul.hSMul (β := E →L[ℂ] ℂ) (-Complex.sin (f x)) (fderiv ℂ f x)

Tactic:
hc.hasFDerivAt.ccos.fderiv

Premises used: HasFDerivAt.ccos, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
n : ℕ∞ω
h : ContDiff ℂ n f
⊢ ContDiff ℂ (F := ℂ) n fun (x : E) ↦ Complex.cos (f x)

Tactic:
Complex.contDiff_cos.comp h

Premises used: Complex.cos, ContDiff.comp, Complex.contDiff_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℂ n f x
⊢ ContDiffAt ℂ (F := ℂ) n (fun (x : E) ↦ Complex.cos (f x)) x

Tactic:
Complex.contDiff_cos.contDiffAt.comp x hf

Premises used: Complex.cos, ContDiffAt.comp, Complex.contDiff_cos, ContDiff.contDiffAt
-- 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) ↦ Complex.cos (f x)) s

Tactic:
Complex.contDiff_cos.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Complex.cos, Complex.contDiff_cos
-- 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) ↦ Complex.cos (f x)) s x

Tactic:
Complex.contDiff_cos.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Complex.cos, ContDiffAt.comp_contDiffWithinAt, Complex.contDiff_cos, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
hf : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ Complex.sin (f x)) (Complex.cos (f x) • f') x

Tactic:
(Complex.hasStrictDerivAt_sin (f x)).comp_hasStrictFDerivAt x hf

Premises used: Complex.sin, Complex.hasStrictDerivAt_sin, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun (x : E) ↦ Complex.sin (f x)) (Complex.cos (f x) • f') x

Tactic:
(Complex.hasDerivAt_sin (f x)).comp_hasFDerivAt x hf

Premises used: Complex.sin, Complex.hasDerivAt_sin, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ Complex.sin (f x)) (Complex.cos (f x) • f') s x

Tactic:
(Complex.hasDerivAt_sin (f x)).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Complex.sin, Complex.hasDerivAt_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
hf : DifferentiableWithinAt ℂ f s x
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (x : E) ↦ Complex.sin (f x)) s x

Tactic:
hf.hasFDerivWithinAt.csin.differentiableWithinAt

Premises used: HasFDerivWithinAt.csin, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
hc : DifferentiableAt ℂ f x
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : E) ↦ Complex.sin (f x)) x

Tactic:
hc.hasFDerivAt.csin.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.csin, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
hc : DifferentiableOn ℂ f s
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : E) ↦ Complex.sin (f x)) s

Tactic:
fun x h => (hc x h).csin

Premises used: DifferentiableWithinAt.csin, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
hc : Differentiable ℂ f
⊢ Differentiable ℂ (F := ℂ) fun (x : E) ↦ Complex.sin (f x)

Tactic:
fun x => (hc x).csin

Premises used: Differentiable, DifferentiableAt.csin
-- 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
hf : DifferentiableWithinAt ℂ f s x
hxs : UniqueDiffWithinAt ℂ s x
⊢ fderivWithin ℂ (fun (x : E) ↦ Complex.sin (f x)) s x =
    HSMul.hSMul (β := E →L[ℂ] ℂ) (Complex.cos (f x)) (fderivWithin ℂ f s x)

Tactic:
hf.hasFDerivWithinAt.csin.fderivWithin hxs

Premises used: HasFDerivWithinAt.csin, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
hc : DifferentiableAt ℂ f x
⊢ fderiv ℂ (fun (x : E) ↦ Complex.sin (f x)) x = HSMul.hSMul (β := E →L[ℂ] ℂ) (Complex.cos (f x)) (fderiv ℂ f x)

Tactic:
hc.hasFDerivAt.csin.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.csin, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
n : ℕ∞ω
h : ContDiff ℂ n f
⊢ ContDiff ℂ (F := ℂ) n fun (x : E) ↦ Complex.sin (f x)

Tactic:
Complex.contDiff_sin.comp h

Premises used: Complex.sin, ContDiff.comp, Complex.contDiff_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℂ n f x
⊢ ContDiffAt ℂ (F := ℂ) n (fun (x : E) ↦ Complex.sin (f x)) x

Tactic:
Complex.contDiff_sin.contDiffAt.comp x hf

Premises used: Complex.sin, ContDiffAt.comp, Complex.contDiff_sin, ContDiff.contDiffAt
-- 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) ↦ Complex.sin (f x)) s

Tactic:
Complex.contDiff_sin.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Complex.sin, Complex.contDiff_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) ↦ Complex.sin (f x)) s x

Tactic:
Complex.contDiff_sin.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Complex.sin, ContDiffAt.comp_contDiffWithinAt, Complex.contDiff_sin, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ HasStrictDerivAt sin (cos x) x

Tactic:
(Complex.hasStrictDerivAt_sin x).real_of_complex

Premises used: Real.cos, HasStrictDerivAt.real_of_complex, Complex.ofReal, Complex.hasStrictDerivAt_sin, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ HasDerivAt sin (cos x) x

Tactic:
(hasStrictDerivAt_sin x).hasDerivAt

Premises used: Real.hasStrictDerivAt_sin, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ sin ~[𝓝 0] id

Tactic:
simpa using (hasDerivAt_sin 0).isLittleO

Premises used: HasDerivAt.isLittleO, Real.hasDerivAt_sin, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℝ n sin

Tactic:
Complex.contDiff_sin.real_of_complex

Premises used: Complex.contDiff_sin, ContDiff.real_of_complex, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ Differentiable ℝ sin

Tactic:
fun x => (hasDerivAt_sin x).differentiableAt

Premises used: Differentiable, Real.hasDerivAt_sin, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ sin x

Tactic:
differentiable_sin x

Premises used: Real.differentiable_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ AnalyticAt ℝ sin x

Tactic:
contDiff_sin.contDiffAt.analyticAt

Premises used: Real.contDiff_sin, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ sin s x

Tactic:
contDiff_sin.contDiffWithinAt.analyticWithinAt

Premises used: Real.contDiff_sin, ContDiff.contDiffWithinAt, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℝ
⊢ AnalyticOnNhd ℝ sin s

Tactic:
fun _ _ ↦ analyticAt_sin

Premises used: AnalyticOnNhd, Real.analyticAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℝ
⊢ AnalyticOn ℝ sin s

Tactic:
contDiff_sin.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, Real.contDiff_sin, ContDiffOn.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ deriv sin = cos

Tactic:
funext fun x => (hasDerivAt_sin x).deriv

Premises used: Real.hasDerivAt_sin, HasDerivAt.deriv, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ HasStrictDerivAt cos (-sin x) x

Tactic:
(Complex.hasStrictDerivAt_cos x).real_of_complex

Premises used: Real.cos, HasStrictDerivAt.real_of_complex, Complex.ofReal, Complex.hasStrictDerivAt_cos, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ HasDerivAt cos (-sin x) x

Tactic:
(Complex.hasDerivAt_cos x).real_of_complex

Premises used: Real.cos, Complex.hasDerivAt_cos, Complex.ofReal, HasDerivAt.real_of_complex, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℝ n cos

Tactic:
Complex.contDiff_cos.real_of_complex

Premises used: Real.cos, Complex.contDiff_cos, ContDiff.real_of_complex
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ Differentiable ℝ cos

Tactic:
fun x => (hasDerivAt_cos x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Real.hasDerivAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ DifferentiableAt ℝ cos x

Tactic:
differentiable_cos x

Premises used: Real.differentiable_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ AnalyticAt ℝ cos x

Tactic:
contDiff_cos.contDiffAt.analyticAt

Premises used: Real.contDiff_cos, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ cos s x

Tactic:
contDiff_cos.contDiffWithinAt.analyticWithinAt

Premises used: Real.contDiff_cos, ContDiff.contDiffWithinAt, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℝ
⊢ AnalyticOnNhd ℝ cos s

Tactic:
fun _ _ ↦ analyticAt_cos

Premises used: Real.analyticAt_cos, AnalyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℝ
⊢ AnalyticOn ℝ cos s

Tactic:
contDiff_cos.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, Real.contDiff_cos, ContDiffOn.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℝ
⊢ deriv cos x = -sin x

Tactic:
(hasDerivAt_cos x).deriv

Premises used: HasDerivAt.deriv, Real.hasDerivAt_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ deriv cos = fun (x : ℝ) ↦ -sin x

Tactic:
funext fun _ => deriv_cos

Premises used: funext, Real.deriv_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sin = iteratedDeriv 0 cos

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos
succ : deriv (iteratedDeriv (n + 1) sin) = iteratedDeriv (n + 1) cos
succ₁ : deriv (iteratedDeriv n cos) = iteratedDeriv (n + 1) cos
succ₂ succ₃ : deriv (iteratedDeriv n cos) = deriv (iteratedDeriv n cos)
⊢ iteratedDeriv (n + 1 + 1) sin = iteratedDeriv (n + 1) cos

Tactic:
rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

Premises used: iteratedDeriv_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sin = iteratedDeriv 0 cos
succ :
  ∀ (n : ℕ) (ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos),
    iteratedDeriv (n + 1 + 1) sin = iteratedDeriv (n + 1) cos
⊢ iteratedDeriv (n + 1) sin = iteratedDeriv n cos

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

Premises used: iteratedDeriv_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
zero : ∀ (x : ℂ), iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos x = (-iteratedDeriv 0 sin) x
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos = -iteratedDeriv 0 sin

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos x = (-iteratedDeriv 0 sin) x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
succ : (fun (x : ℂ) ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)
⊢ iteratedDeriv (n + 1 + 1) cos = -iteratedDeriv (n + 1) sin

Tactic:
rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']

Premises used: iteratedDeriv_succ, deriv.neg'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
succ : ∀ (x : ℂ), -deriv (iteratedDeriv n sin) x = (-deriv (iteratedDeriv n sin)) x
⊢ (fun (x : ℂ) ↦ -deriv (iteratedDeriv n sin) x) = -deriv (iteratedDeriv n sin)

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin
x : ℂ
⊢ -deriv (iteratedDeriv n sin) x = (-deriv (iteratedDeriv n sin)) x

Tactic:
simp