awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
f : ℂ → ℂ
x : ℂ
hc : DifferentiableAt ℂ f x
⊢ deriv (fun (x : ℂ) ↦ Complex.cosh (f x)) x = Complex.sinh (f x) * deriv f x

Tactic:
hc.hasDerivAt.ccosh.deriv

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

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

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

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

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

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

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

Tactic:
hf.hasDerivWithinAt.csinh.derivWithin hxs

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

Tactic:
hc.hasDerivAt.csinh.deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.csinh
-- 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) ↦ Complex.cosh (f x)) (Complex.sinh (f x) • f') x

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

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt, Complex.hasStrictDerivAt_cosh, Complex.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) ↦ Complex.cosh (f x)) (Complex.sinh (f x) • f') x

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

Premises used: Complex.hasDerivAt_cosh, HasDerivAt.comp_hasFDerivAt, Complex.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
s : Set E
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ Complex.cosh (f x)) (Complex.sinh (f x) • f') s x

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

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

Tactic:
hf.hasFDerivWithinAt.ccosh.differentiableWithinAt

Premises used: HasFDerivWithinAt.ccosh, 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) ↦ Complex.cosh (f x)) x

Tactic:
hc.hasFDerivAt.ccosh.differentiableAt

Premises used: HasFDerivAt.ccosh, 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) ↦ Complex.cosh (f x)) s

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

Premises used: DifferentiableWithinAt.ccosh, 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) ↦ Complex.cosh (f x)

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

Premises used: Differentiable, DifferentiableAt.ccosh
-- 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) ↦ Complex.cosh (f x)) s x =
    HSMul.hSMul (β := E →L[ℂ] ℂ) (Complex.sinh (f x)) (fderivWithin ℂ f s x)

Tactic:
hf.hasFDerivWithinAt.ccosh.fderivWithin hxs

Premises used: HasFDerivWithinAt.ccosh, 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) ↦ Complex.cosh (f x)) x = HSMul.hSMul (β := E →L[ℂ] ℂ) (Complex.sinh (f x)) (fderiv ℂ f x)

Tactic:
hc.hasFDerivAt.ccosh.fderiv

Premises used: HasFDerivAt.ccosh, 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) ↦ Complex.cosh (f x)

Tactic:
Complex.contDiff_cosh.comp h

Premises used: Complex.contDiff_cosh, ContDiff.comp, Complex.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) ↦ Complex.cosh (f x)) x

Tactic:
Complex.contDiff_cosh.contDiffAt.comp x hf

Premises used: Complex.contDiff_cosh, ContDiffAt.comp, Complex.cosh, 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) ↦ Complex.cosh (f x)) s

Tactic:
Complex.contDiff_cosh.comp_contDiffOn hf

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

Tactic:
Complex.contDiff_cosh.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Complex.contDiff_cosh, ContDiffAt.comp_contDiffWithinAt, Complex.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) ↦ Complex.sinh (f x)) (Complex.cosh (f x) • f') x

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

Premises used: Complex.sinh, Complex.hasStrictDerivAt_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) ↦ Complex.sinh (f x)) (Complex.cosh (f x) • f') x

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

Premises used: Complex.sinh, Complex.hasDerivAt_sinh, 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) ↦ Complex.sinh (f x)) (Complex.cosh (f x) • f') s x

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

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

Tactic:
hf.hasFDerivWithinAt.csinh.differentiableWithinAt

Premises used: HasFDerivWithinAt.csinh, 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) ↦ Complex.sinh (f x)) x

Tactic:
hc.hasFDerivAt.csinh.differentiableAt

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

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

Premises used: DifferentiableWithinAt.csinh, 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) ↦ Complex.sinh (f x)

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

Premises used: Differentiable, DifferentiableAt.csinh
-- 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) ↦ Complex.sinh (f x)) s x =
    HSMul.hSMul (β := E →L[ℂ] ℂ) (Complex.cosh (f x)) (fderivWithin ℂ f s x)

Tactic:
hf.hasFDerivWithinAt.csinh.fderivWithin hxs

Premises used: HasFDerivWithinAt.csinh, 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) ↦ Complex.sinh (f x)) x = HSMul.hSMul (β := E →L[ℂ] ℂ) (Complex.cosh (f x)) (fderiv ℂ f x)

Tactic:
hc.hasFDerivAt.csinh.fderiv

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

Tactic:
Complex.contDiff_sinh.comp h

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

Tactic:
Complex.contDiff_sinh.contDiffAt.comp x hf

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

Tactic:
Complex.contDiff_sinh.comp_contDiffOn hf

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

Tactic:
Complex.contDiff_sinh.contDiffAt.comp_contDiffWithinAt x hf

Premises used: Complex.sinh, ContDiffAt.comp_contDiffWithinAt, Complex.contDiff_sinh, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ HasStrictDerivAt sinh (cosh x) x

Tactic:
(Complex.hasStrictDerivAt_sinh x).real_of_complex

Premises used: HasStrictDerivAt.real_of_complex, Complex.hasStrictDerivAt_sinh, Real.sinh, Complex.ofReal, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ HasDerivAt sinh (cosh x) x

Tactic:
(Complex.hasDerivAt_sinh x).real_of_complex

Premises used: Real.sinh, Complex.hasDerivAt_sinh, Complex.ofReal, HasDerivAt.real_of_complex, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ sinh ~[𝓝 0] id

Tactic:
simpa using (hasDerivAt_sinh 0).isLittleO

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

Tactic:
Complex.contDiff_sinh.real_of_complex

Premises used: Real.sinh, Complex.contDiff_sinh, ContDiff.real_of_complex
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ Differentiable ℝ sinh

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

Premises used: Differentiable, HasDerivAt.differentiableAt, Real.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ DifferentiableAt ℝ sinh x

Tactic:
differentiable_sinh x

Premises used: Real.differentiable_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ AnalyticAt ℝ sinh x

Tactic:
contDiff_sinh.contDiffAt.analyticAt

Premises used: Real.contDiff_sinh, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ sinh s x

Tactic:
contDiff_sinh.contDiffWithinAt.analyticWithinAt

Premises used: ContDiff.contDiffWithinAt, Real.contDiff_sinh, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℝ
⊢ AnalyticOnNhd ℝ sinh s

Tactic:
fun _ _ ↦ analyticAt_sinh

Premises used: Real.analyticAt_sinh, AnalyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℝ
⊢ AnalyticOn ℝ sinh s

Tactic:
contDiff_sinh.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, ContDiffOn.analyticOn, Real.contDiff_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ deriv sinh = cosh

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

Premises used: HasDerivAt.deriv, funext, Real.hasDerivAt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ HasStrictDerivAt cosh (sinh x) x

Tactic:
(Complex.hasStrictDerivAt_cosh x).real_of_complex

Premises used: HasStrictDerivAt.real_of_complex, Real.sinh, Complex.ofReal, Complex.hasStrictDerivAt_cosh, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ HasDerivAt cosh (sinh x) x

Tactic:
(Complex.hasDerivAt_cosh x).real_of_complex

Premises used: Real.sinh, Complex.ofReal, Complex.hasDerivAt_cosh, HasDerivAt.real_of_complex, Real.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℝ n cosh

Tactic:
Complex.contDiff_cosh.real_of_complex

Premises used: Complex.contDiff_cosh, Real.cosh, ContDiff.real_of_complex
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ Differentiable ℝ cosh

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

Premises used: Differentiable, HasDerivAt.differentiableAt, Real.hasDerivAt_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ DifferentiableAt ℝ cosh x

Tactic:
differentiable_cosh x

Premises used: Real.differentiable_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ AnalyticAt ℝ cosh x

Tactic:
contDiff_cosh.contDiffAt.analyticAt

Premises used: Real.contDiff_cosh, ContDiffAt.analyticAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ cosh s x

Tactic:
contDiff_cosh.contDiffWithinAt.analyticWithinAt

Premises used: ContDiff.contDiffWithinAt, Real.contDiff_cosh, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℝ
⊢ AnalyticOnNhd ℝ cosh s

Tactic:
fun _ _ ↦ analyticAt_cosh

Premises used: AnalyticOnNhd, Real.analyticAt_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
s : Set ℝ
⊢ AnalyticOn ℝ cosh s

Tactic:
contDiff_cosh.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, ContDiffOn.analyticOn, Real.contDiff_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ deriv cosh = sinh

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

Premises used: HasDerivAt.deriv, funext, Real.hasDerivAt_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
rw : ∀ (x : ℝ), 0 < cosh x
⊢ ∀ (x : ℝ), 0 < deriv sinh x

Tactic:
rw [Real.deriv_sinh]

Premises used: Real.deriv_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ ∀ (x : ℝ), 0 < cosh x

Tactic:
cosh_pos

Premises used: Real.cosh_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ ∀ (x : ℝ), 0 < cosh x

Tactic:
exact cosh_pos

Premises used: Real.cosh_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ Function.Injective sinh

Tactic:
sinh_strictMono.injective

Premises used: StrictMono.injective, Real.sinh_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x y : ℝ
⊢ sinh x = sinh y ↔ x = y

Tactic:
sinh_injective.eq_iff

Premises used: Function.Injective.eq_iff, Real.sinh_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x y : ℝ
⊢ sinh x ≤ sinh y ↔ x ≤ y

Tactic:
sinh_strictMono.le_iff_le

Premises used: Real.sinh_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x y : ℝ
⊢ sinh x < sinh y ↔ x < y

Tactic:
sinh_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Real.sinh_strictMono
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
rw : sinh x = 0 ↔ sinh x = sinh 0
rw₁ rw₂ : sinh x = 0 ↔ sinh x = 0
⊢ sinh x = 0 ↔ x = 0

Tactic:
rw [← @sinh_inj x, sinh_zero]

Premises used: Real.sinh_zero, Real.sinh_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ sinh x ≠ 0 ↔ x ≠ 0

Tactic:
sinh_eq_zero.not

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

Tactic:
simpa only [sinh_zero] using @sinh_lt_sinh 0 x

Premises used: Real.sinh_zero, Real.sinh_lt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0

Tactic:
simpa only [sinh_zero] using @sinh_le_sinh x 0

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

Tactic:
simpa only [sinh_zero] using @sinh_lt_sinh x 0

Premises used: Real.sinh_zero, Real.sinh_lt_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ 0 ≤ sinh x ↔ 0 ≤ x

Tactic:
simpa only [sinh_zero] using @sinh_le_sinh 0 x

Premises used: Real.sinh_zero, Real.sinh_le_sinh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
inl : x ≤ 0 → |sinh x| = sinh |x|
inr : 0 ≤ x → |sinh x| = sinh |x|
⊢ |sinh x| = sinh |x|

Tactic:
cases le_total x 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
h : x ≤ 0
⊢ |sinh x| = sinh |x|

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, *]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
h : 0 ≤ x
⊢ |sinh x| = sinh |x|

Tactic:
simp [abs_of_nonneg, abs_of_nonpos, *]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (interior (Ici 0)) x
⊢ 0 < x

Tactic:
rw [interior_Ici, mem_Ioi] at hx

Premises used: interior_Ici, Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
hx : 0 < x
rwa : 0 < sinh x
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < x
⊢ 0 < deriv cosh x

Tactic:
rwa [deriv_cosh, sinh_pos_iff]

Premises used: Real.sinh_pos_iff, Real.deriv_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x y : ℝ
⊢ cosh x ≤ cosh y ↔ |x| ≤ |y|

Tactic:
cosh_abs x ▸ cosh_abs y ▸ cosh_strictMonoOn.le_iff_le (abs_nonneg x) (abs_nonneg y)

Premises used: Real.cosh_abs, Eq.rec, Real.cosh_strictMonoOn, StrictMonoOn.le_iff_le, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x y : ℝ
⊢ cosh x < cosh y ↔ |x| < |y|

Tactic:
lt_iff_lt_of_le_iff_le cosh_le_cosh

Premises used: Real.cosh_le_cosh, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ |0| ≤ |x|

Tactic:
simp only [_root_.abs_zero, _root_.abs_nonneg]

Premises used: abs_zero, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ |0| < |x| ↔ x ≠ 0

Tactic:
simp only [_root_.abs_zero, abs_pos]

Premises used: abs_pos, abs_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
simp : -sinh x + x = x - sinh x
⊢ sinh (-x) - -x = -(sinh x - x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
x : ℝ
⊢ -sinh x + x = x - sinh x

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
refine : StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
⊢ StrictMono (β := ℝ) fun (x : ℝ) ↦ sinh x - x

Tactic:
refine strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) ?_

Premises used: strictMono_of_odd_strictMonoOn_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)

Tactic:
strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_

Premises used: convex_Ici, strictMonoOn_of_deriv_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)
refine_2 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (interior (Ici 0)) x),
    LT.lt (α := ℝ) 0 (deriv (fun (x : ℝ) ↦ sinh x - x) x)
⊢ StrictMonoOn (β := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)

Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_

Premises used: convex_Ici, strictMonoOn_of_deriv_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)

Tactic:
(continuous_sinh.sub continuous_id).continuousOn

Premises used: Continuous.continuousOn, Real.continuous_sinh, continuous_id, Continuous.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Goal:
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ sinh x - x) (Ici 0)

Tactic:
exact (continuous_sinh.sub continuous_id).continuousOn

Premises used: Continuous.continuousOn, Real.continuous_sinh, continuous_id, Continuous.sub