∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : StrongDual ℝ E},
  HasStrictFDerivAt f f' a → HasStrictFDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a