feat: the set of points where IsImmersionAt(OfComplement) holds is open (#30356)

Prove an API lemma which `chrisflav` requested in #28793, which was split from that PR to keep the diff smaller.

Author: grunweg

Mathlib/Geometry/Manifold/Immersion.lean

@@ -45,6 +45,8 @@ This shortens the overall argument, as the definition of submersions has the sam
 * `IsImmersionAtOfComplement.congr_F`, `IsImmersionOfComplement.congr_F`:
   being an immersion (at `x`) w.r.t. `F` is stable under
   replacing the complement `F` by an isomorphic copy
+* `IsOpen.isImmersionAtOfComplement` and `IsOpen.isImmersionAt`:
+  the set of points where `IsImmersionAt(OfComplement)` holds is open.
 
 ## Implementation notes
 
@@ -64,7 +66,6 @@ This shortens the overall argument, as the definition of submersions has the sam
 ## TODO
 * The converse to `IsImmersionAtOfComplement.congr_F` also holds: any two complements are
   isomorphic, as they are isomorphic to the cokernel of the differential `mfderiv I J f x`.
-* The set where `IsImmersionAt(OfComplement)` holds is open.
 * `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`.
 * `IsImmersion.contMDiff`: if f is an immersion, it is `C^n`.
 * `IsImmersionAt.prodMap`: the product of two immersions is an immersion.
@@ -356,6 +357,12 @@ lemma congr_F (e : F ≃L[𝕜] F') :
     IsImmersionAtOfComplement F I J n f x ↔ IsImmersionAtOfComplement F' I J n f x :=
   ⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩
 
+/- The set of points where `IsImmersionAtOfComplement` holds is open. -/
+lemma _root_.IsOpen.isImmersionAtOfComplement :
+    IsOpen {x | IsImmersionAtOfComplement F I J n f x} := by
+  simp_rw [IsImmersionAtOfComplement_def]
+  exact .liftSourceTargetPropertyAt
+
 /-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`.
 
 Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
@@ -515,6 +522,14 @@ lemma congr_iff (hfg : f =ᶠ[𝓝 x] g) :
     IsImmersionAt I J n f x ↔ IsImmersionAt I J n g x :=
   ⟨fun h ↦ h.congr_of_eventuallyEq hfg, fun h ↦ h.congr_of_eventuallyEq hfg.symm⟩
 
+/- The set of points where `IsImmersionAt` holds is open. -/
+lemma _root_.IsOpen.isImmersionAt :
+    IsOpen {x | IsImmersionAt I J n f x} := by
+  rw [isOpen_iff_forall_mem_open]
+  exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement hx.complement I J n f x },
+    fun y hy ↦ hy.isImmersionAt, .isImmersionAtOfComplement,
+    by simp [hx.isImmersionAtOfComplement_complement]⟩
+
 end IsImmersionAt
 
 variable (F I J n) in

Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean

@@ -33,6 +33,8 @@ local property of this form.
   `f` has this property at `x` if there exist charts `φ` and `ψ` such that `P f φ ψ` holds.
 * `Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq`: if `f` has property `P` at `x`
   and `g` equals `f` near `x`, then `g` also has property `P` at `x`.
+* `IsOpen.liftSourceTargetPropertyAt`: the set of points at which `LiftSourceTargetPropertyAt`
+  holds is open
 
 -/
 
@@ -194,6 +196,19 @@ lemma congr_iff_of_eventuallyEq (hP : IsLocalSourceTargetProperty P) (h' : f =
     LiftSourceTargetPropertyAt I I' n f x P ↔ LiftSourceTargetPropertyAt I I' n g x P :=
   ⟨fun hf ↦ hf.congr_of_eventuallyEq hP h', fun hg ↦ hg.congr_of_eventuallyEq hP h'.symm⟩
 
+/- The set of points where `LiftSourceTargetPropertyAt` holds is open. -/
+lemma _root_.IsOpen.liftSourceTargetPropertyAt :
+    IsOpen {x | LiftSourceTargetPropertyAt I I' n g x P} := by
+  rw [isOpen_iff_forall_mem_open]
+  intro x hx
+  -- Suppose the lifted property `P` holds at `x`:
+  -- choose slice charts `φ` near `x` and `ψ` near `f x` s.t. `P f φ ψ` holds.
+  -- Then the same charts witness that `P f φ ψ` holds at any `y ∈ φ.source`.
+  refine ⟨hx.domChart.source, fun y hy ↦ ?_, hx.domChart.open_source, hx.mem_domChart_source⟩
+  exact ⟨hx.domChart, hx.codChart, hy, hx.source_subset_preimage_source hy,
+    hx.domChart_mem_maximalAtlas, hx.codChart_mem_maximalAtlas, hx.source_subset_preimage_source,
+    hx.property⟩
+
 end LiftSourceTargetPropertyAt
 
 end Manifold