awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
refine_2 : x ≠ 0
refine_2₁ : DifferentiableAt ℝ sinh x
refine_2₂ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x) x
⊢ LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)

Tactic:
rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]

Premises used: sub_pos, Real.deriv_sinh, deriv_id'', deriv_fun_sub, Real.one_lt_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
⊢ x ≠ 0

Tactic:
hx.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

Tactic:
differentiableAt_sinh

Premises used: Real.differentiableAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x) x

Tactic:
differentiableAt_id

Premises used: differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
⊢ x ≠ 0

Tactic:
exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]

Premises used: LT.lt.ne', Real.differentiableAt_sinh, differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ x ≤ sinh x ↔ sinh 0 - 0 ≤ sinh x - x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ sinh x ≤ x ↔ sinh x - x ≤ sinh 0 - 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ x < sinh x ↔ 0 < x

Tactic:
lt_iff_lt_of_le_iff_le sinh_le_self_iff

Premises used: lt_iff_lt_of_le_iff_le, Real.sinh_le_self_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ sinh x < x ↔ x < 0

Tactic:
lt_iff_lt_of_le_iff_le self_le_sinh_iff

Premises used: Real.self_le_sinh_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sinh = iteratedDeriv 0 cosh

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

Tactic:
rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

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

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

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

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

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

Tactic:
rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]

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

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

Premises used: iteratedDeriv_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sinh = sinh

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
ih : iteratedDeriv (2 * n) sinh = sinh
⊢ iteratedDeriv (2 * (n + 1)) sinh = sinh

Tactic:
simp_all [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) sinh = sinh
succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) sinh = sinh), iteratedDeriv (2 * (n + 1)) sinh = sinh
⊢ iteratedDeriv (2 * n) sinh = sinh

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

Premises used: mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cosh = cosh

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
ih : iteratedDeriv (2 * n) cosh = cosh
⊢ iteratedDeriv (2 * (n + 1)) cosh = cosh

Tactic:
simp_all [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
zero : iteratedDeriv (HMul.hMul (α := ℕ) 2 0) cosh = cosh
succ : ∀ (n : ℕ) (ih : iteratedDeriv (2 * n) cosh = cosh), iteratedDeriv (2 * (n + 1)) cosh = cosh
⊢ iteratedDeriv (2 * n) cosh = cosh

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

Premises used: mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n + 1) sinh = cosh

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
⊢ iteratedDeriv (2 * n + 1) cosh = sinh

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 sinh)

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

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

Tactic:
simp [differentiable_iteratedDeriv_sinh]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
⊢ Differentiable ℂ (iteratedDeriv 0 cosh)

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

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

Tactic:
simp [differentiable_iteratedDeriv_cosh]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
zero : ∀ (x : ℝ), iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh x = iteratedDeriv 0 sinh x
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh = iteratedDeriv 0 sinh

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) cosh x = iteratedDeriv 0 sinh x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 sinh)

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

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

Tactic:
simp [differentiable_iteratedDeriv_sinh]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
⊢ Differentiable ℝ (iteratedDeriv 0 cosh)

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

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

Tactic:
simp [differentiable_iteratedDeriv_cosh]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : ℕ
a b : ℝ
h : a < b
x : ℝ
hx : x ∈ Icc a b
⊢ iteratedDerivWithin n sinh (Icc a b) x = iteratedDeriv n sinh x

Tactic:
iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc h) contDiff_sinh.contDiffAt hx

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

Tactic:
iteratedDerivWithin_eq_iteratedDeriv (uniqueDiffOn_Icc h) contDiff_cosh.contDiffAt hx

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

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

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

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

Premises used: iteratedDerivWithin_eq_iteratedDeriv, Real.contDiff_cosh, uniqueDiffOn_Ioo, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ Real.cosh (f x)) (Real.sinh (f x) * f') x

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

Premises used: Real.hasStrictDerivAt_cosh, HasStrictDerivAt.comp, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.cosh (f x)) (Real.sinh (f x) * f') x

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

Premises used: HasDerivAt.comp, Real.hasDerivAt_cosh, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ Real.cosh (f x)) (Real.sinh (f x) * f') s x

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

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

Tactic:
hf.hasDerivWithinAt.cosh.derivWithin hxs

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

Tactic:
hc.hasDerivAt.cosh.deriv

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

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

Premises used: Real.hasStrictDerivAt_sinh, Real.sinh, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℝ) ↦ Real.sinh (f x)) (Real.cosh (f x) * f') x

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

Premises used: HasDerivAt.comp, Real.sinh, Real.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ Real.sinh (f x)) (Real.cosh (f x) * f') s x

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

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

Tactic:
hf.hasDerivWithinAt.sinh.derivWithin hxs

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

Tactic:
hc.hasDerivAt.sinh.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) (Real.sinh (f x) • f') x

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

Premises used: Real.hasStrictDerivAt_cosh, HasStrictDerivAt.comp_hasStrictFDerivAt, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) (Real.sinh (f x) • f') x

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

Premises used: Real.hasDerivAt_cosh, Real.cosh, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) (Real.sinh (f x) • f') s x

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

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Real.hasDerivAt_cosh, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) s x

Tactic:
hf.hasFDerivWithinAt.cosh.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) x

Tactic:
hc.hasFDerivAt.cosh.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) s

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

Premises used: DifferentiableWithinAt.cosh, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hc : Differentiable ℝ f
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ Real.cosh (f x)

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

Premises used: Differentiable, DifferentiableAt.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) s x =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sinh (f x)) (fderivWithin ℝ f s x)

Tactic:
hf.hasFDerivWithinAt.cosh.fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.sinh (f x)) (fderiv ℝ f x)

Tactic:
hc.hasFDerivAt.cosh.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)

Tactic:
Real.contDiff_cosh.comp h

Premises used: ContDiff.comp, Real.contDiff_cosh, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) x

Tactic:
Real.contDiff_cosh.contDiffAt.comp x hf

Premises used: Real.contDiff_cosh, Real.cosh, ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) s

Tactic:
Real.contDiff_cosh.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Real.contDiff_cosh, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.cosh (f x)) s x

Tactic:
Real.contDiff_cosh.contDiffAt.comp_contDiffWithinAt x hf

Premises used: ContDiffAt.comp_contDiffWithinAt, Real.contDiff_cosh, Real.cosh, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) (Real.cosh (f x) • f') x

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

Premises used: Real.hasStrictDerivAt_sinh, Real.sinh, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) (Real.cosh (f x) • f') x

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

Premises used: Real.sinh, HasDerivAt.comp_hasFDerivAt, Real.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) (Real.cosh (f x) • f') s x

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

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Real.sinh, Real.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) s x

Tactic:
hf.hasFDerivWithinAt.sinh.differentiableWithinAt

Premises used: HasFDerivWithinAt.sinh, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) x

Tactic:
hc.hasFDerivAt.sinh.differentiableAt

Premises used: HasFDerivAt.sinh, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) s

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

Premises used: DifferentiableOn, DifferentiableWithinAt.sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hc : Differentiable ℝ f
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ Real.sinh (f x)

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

Premises used: Differentiable, DifferentiableAt.sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) s x =
    HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cosh (f x)) (fderivWithin ℝ f s x)

Tactic:
hf.hasFDerivWithinAt.sinh.fderivWithin hxs

Premises used: HasFDerivWithinAt.sinh, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (Real.cosh (f x)) (fderiv ℝ f x)

Tactic:
hc.hasFDerivAt.sinh.fderiv

Premises used: HasFDerivAt.sinh, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)

Tactic:
Real.contDiff_sinh.comp h

Premises used: Real.sinh, ContDiff.comp, Real.contDiff_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) x

Tactic:
Real.contDiff_sinh.contDiffAt.comp x hf

Premises used: Real.sinh, Real.contDiff_sinh, ContDiffAt.comp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) s

Tactic:
Real.contDiff_sinh.comp_contDiffOn hf

Premises used: ContDiff.comp_contDiffOn, Real.sinh, Real.contDiff_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
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.sinh (f x)) s x

Tactic:
Real.contDiff_sinh.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Real.sinh, ContDiffAt.comp_contDiffWithinAt, Real.contDiff_sinh, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
h : ∀ (x : ℂ), logDeriv cosh x = tanh x
⊢ logDeriv cosh = tanh

Tactic:
ext