x✝ y z x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
x✝ y z x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv cosh x
rw [interior_Ici, mem_Ioi] at hx
no goals
x✝ y z x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
rwa [deriv_cosh, sinh_pos_iff]