x y z : ℝ
⊢ StrictMonoOn (fun x => sinh x - x) (Ici 0)
x y z : ℝ
⊢ StrictMono fun x => sinh x - x
refine' strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) _
case refine'_1
x y z : ℝ
⊢ ContinuousOn (fun x => sinh x - x) (Ici 0)

case refine'_2
x✝ y z x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x => sinh x - x) x
x y z : ℝ
⊢ StrictMonoOn (fun x => sinh x - x) (Ici 0)
refine' (convex_Ici _).strictMonoOn_of_deriv_pos _ fun x hx => _
x✝ y z x : ℝ
⊢ -sinh x + x = x - sinh x
x✝ y z x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)
simp
no goals
x✝ y z x : ℝ
⊢ -sinh x + x = x - sinh x
abel
no goals
case refine'_1
x y z : ℝ
⊢ ContinuousOn (fun x => sinh x - x) (Ici 0)
exact (continuous_sinh.sub continuous_id).continuousOn
case refine'_2
x✝ y z x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x => sinh x - x) x
case refine'_2
x✝ y z x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x => sinh x - x) x
rw [interior_Ici, mem_Ioi] at hx
case refine'_2
x✝ y z x : ℝ
hx : 0 < x
⊢ x ≠ 0

case refine'_2.hf
x✝ y z x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => sinh x) x

case refine'_2.hg
x✝ y z x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => x) x
case refine'_2
x✝ y z x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x => sinh x - x) x
rw [deriv_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
no goals
case refine'_2
x✝ y z x : ℝ
hx : 0 < x
⊢ x ≠ 0

case refine'_2.hf
x✝ y z x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => sinh x) x

case refine'_2.hg
x✝ y z x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => x) x
exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]