∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E},
  HasStrictFDerivAt f f' x → f x ≠ 0 → HasStrictFDerivAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') x