∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {f' x : 𝕜},
  HasStrictDerivAt f f' x →
    ∀ (hf' : f' ≠ 0), HasStrictFDerivAt f (↑((ContinuousLinearEquiv.unitsEquivAut 𝕜) (Units.mk0 f' hf'))) x