feat: uniqueness API for implicit function of IsContDiffImplicitAt (#31988)

Author: winstonyin

Mathlib/Analysis/Calculus/Implicit.lean

@@ -161,6 +161,9 @@ complementary subspaces of `E`, then `implicitFunction` is the unique (germ of a
 def implicitFunction : F → G → E :=
   Function.curry <| φ.toOpenPartialHomeomorph.symm
 
+lemma implicitFunction_apply {x : F} {y : G} :
+    φ.implicitFunction x y = φ.toOpenPartialHomeomorph.symm (x, y) := rfl
+
 @[simp]
 theorem toOpenPartialHomeomorph_coe : ⇑φ.toOpenPartialHomeomorph = φ.prodFun :=
   rfl
@@ -272,6 +275,11 @@ theorem map_implicitFunction_nhdsWithin_preimage (φ : ImplicitFunctionData 𝕜
       φ.toOpenPartialHomeomorph.leftInvOn hxs]
   · exact φ.toOpenPartialHomeomorph.mapsTo φ.pt_mem_toOpenPartialHomeomorph_source
 
+theorem eventuallyEq_implicitFunction {ψ : F → G → E}
+    (h : ∀ᶠ x in 𝓝 φ.pt, ψ (φ.leftFun x) (φ.rightFun x) = x) :
+    Function.uncurry ψ =ᶠ[𝓝 (φ.prodFun φ.pt)] Function.uncurry φ.implicitFunction :=
+  HasStrictFDerivAt.localInverse_unique _ h
+
 end ImplicitFunctionData
 
 namespace HasStrictFDerivAt

Mathlib/Analysis/Calculus/ImplicitContDiff.lean

@@ -98,12 +98,16 @@ def implicitFunctionData (h : IsContDiffImplicitAt n f f' a) :
       exact ⟨(0, y), by simp, x - (0, y), by simp [map_sub, ← hy], by abel⟩
 
 @[simp]
-lemma implicitFunctionData_leftFun_pt (h : IsContDiffImplicitAt n f f' a) :
-    h.implicitFunctionData.leftFun h.implicitFunctionData.pt = a.1 := rfl
+lemma implicitFunctionData_pt (h : IsContDiffImplicitAt n f f' a) :
+    h.implicitFunctionData.pt = a := rfl
 
 @[simp]
-lemma implicitFunctionData_rightFun_pt (h : IsContDiffImplicitAt n f f' a) :
-    h.implicitFunctionData.rightFun h.implicitFunctionData.pt = f a := rfl
+lemma implicitFunctionData_leftFun_apply {h : IsContDiffImplicitAt n f f' a} {xy : E × F} :
+    h.implicitFunctionData.leftFun xy = xy.1 := rfl
+
+@[simp]
+lemma implicitFunctionData_rightFun_apply {h : IsContDiffImplicitAt n f f' a} {xy : E × F} :
+    h.implicitFunctionData.rightFun xy = f xy := rfl
 
 /-- The implicit function provided by the general theorem, from which we construct the more useful
 form `IsContDiffImplicitAt.implicitFunction`. -/
@@ -126,6 +130,10 @@ lemma implicitFunction_def (h : IsContDiffImplicitAt n f f' a) :
     h.implicitFunction = fun x ↦ (h.implicitFunctionData.implicitFunction.uncurry (x, f a)).2 :=
   rfl
 
+@[simp]
+lemma implicitFunction_apply (h : IsContDiffImplicitAt n f f' a) (x : E) :
+    h.implicitFunction x = (h.implicitFunctionData.implicitFunction x (f a)).2 := rfl
+
 /-- `implicitFunction` is indeed the (local) implicit function defined by `f`. -/
 lemma apply_implicitFunction (h : IsContDiffImplicitAt n f f' a) :
     ∀ᶠ x in 𝓝 a.1, f (x, h.implicitFunction x) = f a := by
@@ -142,6 +150,11 @@ lemma apply_implicitFunction (h : IsContDiffImplicitAt n f f' a) :
   · rw [h1]
   · rfl
 
+theorem eventually_implicitFunction_apply_eq (h : IsContDiffImplicitAt n f f' a) :
+    ∀ᶠ xy in 𝓝 a, f xy = f a → h.implicitFunction xy.1 = xy.2 := by
+  refine h.implicitFunctionData.implicitFunction_apply_image.mono fun xy h₁ h₂ ↦ ?_
+  simp_all
+
 /-- If the implicit equation `f` is $C^n$ at `(x, y)`, then its implicit function `φ` around `x` is
 also $C^n$ at `x`. -/
 theorem contDiffAt_implicitFunction (h : IsContDiffImplicitAt n f f' a) :