A continuous, already constructed solution of a smooth identity is smooth when the derivative in its value variable is invertible. The local inverse theorem proves regularity; no new solution is postulated.

theorem EulerSmoothImplicitLift.contDiffAt_of_identity {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Y : P → E) (G : E → F) (H : P → F) (x : P) (n : WithTop ℕ∞) (hn : n ≠ 0) (hY : ContinuousAt Y x) (hG : ContDiffAt ℝ n G (Y x)) (hH : ContDiffAt ℝ n H x) (L : E ≃L[ℝ] F) (hL : HasFDerivAt G (↑L) (Y x)) (heq : ∀ (y : P), G (Y y) = H y) : ContDiffAt ℝ n Y x