awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cos = -iteratedDeriv 0 sin
succ :
  ∀ (n : ℕ) (ih : iteratedDeriv (n + 1) cos = -iteratedDeriv n sin),
    iteratedDeriv (n + 1 + 1) cos = -iteratedDeriv (n + 1) sin
⊢ iteratedDeriv (n + 1) cos = -iteratedDeriv n sin

Tactic:
induction n with
  | zero => ext; simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ, deriv.neg']
    ext x
    simp

Premises used: iteratedDeriv_succ, deriv.neg'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * sin

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * sin
⊢ iteratedDeriv (2 * (n + 1)) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * sin

Tactic:
simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * sin
succ :
  ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * sin),
    iteratedDeriv (2 * (n + 1)) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * sin
⊢ iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * sin

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * cos

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos
⊢ iteratedDeriv (2 * (n + 1)) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * cos

Tactic:
simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℂ) → ℂ) (β := ℕ) (-1) 0 * cos
succ :
  ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos),
    iteratedDeriv (2 * (n + 1)) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * cos
⊢ iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n + 1) sin = HPow.hPow (α := (x : ℂ) → ℂ) (-1) n * cos

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n + 1) cos = HPow.hPow (α := (x : ℂ) → ℂ) (-1) (n + 1) * sin

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 sin)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 sin)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n_1 n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) sin)

Tactic:
simp [differentiable_iteratedDeriv_sin]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 cos)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 1 cos)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n_1 n : ℕ
⊢ Differentiable ℂ (iteratedDeriv (n + 2) cos)

Tactic:
simp [differentiable_iteratedDeriv_cos]
-- 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * sin

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * sin
⊢ iteratedDeriv (2 * (n + 1)) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * sin

Tactic:
simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sin = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * sin
succ :
  ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * sin),
    iteratedDeriv (2 * (n + 1)) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * sin
⊢ iteratedDeriv (2 * n) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * sin

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * cos

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
ih : iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos
⊢ iteratedDeriv (2 * (n + 1)) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * cos

Tactic:
simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cos = HPow.hPow (α := (x : ℝ) → ℝ) (β := ℕ) (-1) 0 * cos
succ :
  ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos),
    iteratedDeriv (2 * (n + 1)) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * cos
⊢ iteratedDeriv (2 * n) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add, pow_succ]

Premises used: pow_succ, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n + 1) sin = HPow.hPow (α := (x : ℝ) → ℝ) (-1) n * cos

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n + 1) cos = HPow.hPow (α := (x : ℝ) → ℝ) (-1) (n + 1) * sin

Tactic:
simp [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 sin)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 sin)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n_1 n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) sin)

Tactic:
simp [differentiable_iteratedDeriv_sin]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 cos)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 1 cos)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n_1 n : ℕ
⊢ Differentiable ℝ (iteratedDeriv (n + 2) cos)

Tactic:
simp [differentiable_iteratedDeriv_cos]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
x : ℝ
⊢ |iteratedDeriv 0 sin x| ≤ 1

Tactic:
simpa using Real.abs_sin_le_one x

Premises used: Real.abs_sin_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
x : ℝ
⊢ |iteratedDeriv 1 sin x| ≤ 1

Tactic:
simpa using Real.abs_cos_le_one x

Premises used: Real.abs_cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n_1 : ℕ
x : ℝ
n : ℕ
⊢ |iteratedDeriv (n + 2) sin x| ≤ 1

Tactic:
simpa using abs_iteratedDeriv_sin_le_one n x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
x : ℝ
⊢ |iteratedDeriv 0 cos x| ≤ 1

Tactic:
simpa using Real.abs_cos_le_one x

Premises used: Real.abs_cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
x : ℝ
⊢ |iteratedDeriv 1 cos x| ≤ 1

Tactic:
simpa using Real.abs_sin_le_one x

Premises used: Real.abs_sin_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n_1 : ℕ
x : ℝ
n : ℕ
⊢ |iteratedDeriv (n + 2) cos x| ≤ 1

Tactic:
simpa using abs_iteratedDeriv_cos_le_one n x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
a b : ℝ
h : a < b
x : ℝ
hx : x ∈ Icc a b
⊢ iteratedDerivWithin n sin (Icc a b) x = iteratedDeriv n sin x

Tactic:
iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc h) contDiff_sin.contDiffAt hx

Premises used: uniqueDiffOn_Icc, iteratedDerivWithin_eq_iteratedDeriv, Real.contDiff_sin, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
a b : ℝ
h : a < b
x : ℝ
hx : x ∈ Icc a b
⊢ iteratedDerivWithin n cos (Icc a b) x = iteratedDeriv n cos x

Tactic:
iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc h) contDiff_cos.contDiffAt hx

Premises used: uniqueDiffOn_Icc, iteratedDerivWithin_eq_iteratedDeriv, Real.contDiff_cos, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
a b x : ℝ
hx : x ∈ Ioo a b
⊢ iteratedDerivWithin n sin (Ioo a b) x = iteratedDeriv n sin x

Tactic:
iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Ioo a b) contDiff_sin.contDiffAt hx

Premises used: iteratedDerivWithin_eq_iteratedDeriv, Real.contDiff_sin, uniqueDiffOn_Ioo, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : ℕ
a b x : ℝ
hx : x ∈ Ioo a b
⊢ iteratedDerivWithin n cos (Ioo a b) x = iteratedDeriv n cos x

Tactic:
iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Ioo a b) contDiff_cos.contDiffAt hx

Premises used: iteratedDerivWithin_eq_iteratedDeriv, Real.contDiff_cos, uniqueDiffOn_Ioo, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ Real.cos (f x)) (-Real.sin (f x) * f') x

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

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

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

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

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

Premises used: Real.cos, Real.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 : ℝ) ↦ Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x

Tactic:
hf.hasDerivWithinAt.cos.derivWithin hxs

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

Tactic:
hc.hasDerivAt.cos.deriv

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

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

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

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

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

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

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

Tactic:
hf.hasDerivWithinAt.sin.derivWithin hxs

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

Tactic:
hc.hasDerivAt.sin.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.sin
-- 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) ↦ Real.cos (f x)) (-Real.sin (f x) • f') x

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

Premises used: Real.cos, HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_cos
-- 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) ↦ Real.cos (f x)) (-Real.sin (f x) • f') x

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

Premises used: Real.cos, Real.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) ↦ Real.cos (f x)) (-Real.sin (f x) • f') s x

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

Premises used: Real.cos, HasDerivAt.comp_hasFDerivWithinAt, Real.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) ↦ Real.cos (f x)) s x

Tactic:
hf.hasFDerivWithinAt.cos.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.cos, 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) ↦ Real.cos (f x)) x

Tactic:
hc.hasFDerivAt.cos.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.cos
-- 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) ↦ Real.cos (f x)) s

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

Premises used: DifferentiableOn, DifferentiableWithinAt.cos
-- 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) ↦ Real.cos (f x)

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

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

Tactic:
hf.hasFDerivWithinAt.cos.fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.cos, 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) ↦ Real.cos (f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (-Real.sin (f x)) (fderiv ℝ f x)

Tactic:
hc.hasFDerivAt.cos.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.cos
-- 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) ↦ Real.cos (f x)

Tactic:
Real.contDiff_cos.comp h

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

Tactic:
Real.contDiff_cos.contDiffAt.comp x hf

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

Tactic:
Real.contDiff_cos.comp_contDiffOn hf

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

Tactic:
Real.contDiff_cos.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Real.cos, Real.contDiff_cos, ContDiffAt.comp_contDiffWithinAt, 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) ↦ Real.sin (f x)) (Real.cos (f x) • f') x

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

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_sin, Real.sin
-- 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) ↦ Real.sin (f x)) (Real.cos (f x) • f') x

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

Premises used: Real.hasDerivAt_sin, HasDerivAt.comp_hasFDerivAt, Real.sin
-- 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) ↦ Real.sin (f x)) (Real.cos (f x) • f') s x

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

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

Tactic:
hf.hasFDerivWithinAt.sin.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.sin
-- 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) ↦ Real.sin (f x)) x

Tactic:
hc.hasFDerivAt.sin.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.sin, 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) ↦ Real.sin (f x)) s

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

Premises used: DifferentiableWithinAt.sin, 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) ↦ Real.sin (f x)

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

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

Tactic:
hf.hasFDerivWithinAt.sin.fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.sin
-- 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) ↦ Real.sin (f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cos (f x)) (fderiv ℝ f x)

Tactic:
hc.hasFDerivAt.sin.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.sin, 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) ↦ Real.sin (f x)

Tactic:
Real.contDiff_sin.comp h

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

Tactic:
Real.contDiff_sin.contDiffAt.comp x hf

Premises used: Real.contDiff_sin, ContDiffAt.comp, Real.sin, ContDiff.contDiffAt