The analytic root branch through a simple root

The analytic implicit function theorem behind the local parametrization theorem [GR84, Chapter 3, §1], in one dependent variable: for Φ₂(u, t) analytic near (u₀, t₀) with Φ₂(u₀, t₀) = 0 and ∂_t Φ₂(u₀, t₀) ≠ 0, there is an analytic τ near u₀ with τ(u₀) = t₀, Φ₂(u, τ(u)) = 0, and every zero (u, t) of Φ₂ near (u₀, t₀) has t = τ(u).

Mathlib has the inverse function theorem for C^n maps at every level n, including ω (analytic), but no separate multivariable implicit function theorem for analytic maps; the branch is therefore obtained from the local inverse Ψ of the joint map Φ(u, t) = (u, Φ₂(u, t)) (ContDiffAt.localInverse at level ω, ContDiffAt.to_localInverse for its analyticity, ContDiffAt.analyticAt), as τ(u) := (Ψ(u, 0))₂. The derivative of Φ at (u₀, t₀) is (v, s) ↦ (v, DΦ₂(v, s)), injective because DΦ₂(0, s) = s · ∂_t Φ₂(u₀, t₀), hence bijective in finite dimension (ContinuousLinearEquiv.ofBijective).

theorem Analytic.exists_analytic_root_branch {d : ℕ} {Φ₂ : (Fin d → ℂ) × ℂ → ℂ} {u₀ : Fin d → ℂ} {t₀ c : ℂ} (hΦ : AnalyticAt ℂ Φ₂ (u₀, t₀)) (h0 : Φ₂ (u₀, t₀) = 0) (hder : HasDerivAt (fun (t : ℂ) => Φ₂ (u₀, t)) c t₀) (hc : c ≠ 0) : ∃ (τ : (Fin d → ℂ) → ℂ), AnalyticAt ℂ τ u₀ ∧ τ u₀ = t₀ ∧ (∀ᶠ (u : Fin d → ℂ) in nhds u₀, Φ₂ (u, τ u) = 0) ∧ ∀ᶠ (p : (Fin d → ℂ) × ℂ) in nhds (u₀, t₀), Φ₂ p = 0 → p.2 = τ p.1

The analytic implicit function theorem in one dependent variable, from Mathlib's C^ω inverse function theorem for the joint map (u, t) ↦ (u, Φ₂(u, t)): a simple zero (u₀, t₀) of an analytic Φ₂ (∂_t Φ₂(u₀, t₀) = c ≠ 0) lies on an analytic root branch τ, and near (u₀, t₀) the zeros of Φ₂ are exactly the points of the branch.