case h.e'_7.h.e'_3
x✝ y x : ℝ
⊢ sqrt (1 + x ^ 2) = cosh (↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph sinhHomeomorph)) x)
x✝ y x : ℝ
⊢ HasStrictDerivAt arsinh (sqrt (1 + x ^ 2))⁻¹ x
convert sinhHomeomorph.toLocalHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne'
  (hasStrictDerivAt_sinh _) using 2
no goals
case h.e'_7.h.e'_3
x✝ y x : ℝ
⊢ sqrt (1 + x ^ 2) = cosh (↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph sinhHomeomorph)) x)
exact (cosh_arsinh _).symm