An actual continuous inverse has the inverse Jacobian as its derivative. This is the easy half of the inverse function theorem; no differentiability of the inverse is an independent assumption.

theorem EulerContinuousInverseDerivative.hasFDerivAt_inverse {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (X : F → E) (Y : E → F) (x : E) (J : F →L[ℝ] E) (I : E →L[ℝ] F) (hY : ContinuousAt Y x) (hX : HasFDerivAt X J (Y x)) (hXY : ∀ᶠ (y : E) in nhds x, X (Y y) = y) (hI : Function.LeftInverse ⇑I ⇑J) : HasFDerivAt Y I x