Analyticity of local inverses

theorem AnalyticAt.analyticAt_localInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} [CompleteSpace 𝕜] [CharZero 𝕜] (hf : AnalyticAt 𝕜 f x) (hf' : deriv f x ≠ 0) : AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

The local inverse of an analytic function (at a point where its derivative does not vanish) is itself analytic.

theorem analyticAt_comp_iff_of_deriv_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} [CompleteSpace 𝕜] [CharZero 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} (hf : AnalyticAt 𝕜 f x) (hf' : deriv f x ≠ 0) : AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x)