feat: an explicit criterion for membership in the maximal atlas of a C^n manifold (leanprover-community#40632)

Add an explicit characterisation, that an `OpenPartialHomeomorph` phi lies in the maximal atlas of a C^n manifold if both phi and phi.symm are C^n on their source.

This can be useful to prove that certain explicit maps are in the maximal atlas, so prove some maps are immersions. Motivating examples are leanprover-community#29077 (for the inclusion of a closed interval [a, b] into the real numbers) and for a manual proof that diffeomorphisms are immersions.

Along the way, rename `contMDiff_model` and its inverse cousin `contMDiffOn_model_symm` to match the naming convention, and golf their proofs.

Author: grunweg

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -45,19 +45,20 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 
 section Atlas
 
-theorem contMDiff_model : ContMDiff I 𝓘(𝕜, E) n I := by
+variable (I) in
+theorem ModelWithCorners.contMDiff : ContMDiff I 𝓘(𝕜, E) n I := by
   intro x
   refine contMDiffAt_iff.mpr ⟨I.continuousAt, ?_⟩
-  simp only [mfld_simps]
-  refine contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_
-  · exact Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun x₂ => I.right_inv
-  simp_rw [Function.comp_apply, I.left_inv, Function.id_def]
+  simpa using contDiffWithinAt_id.congr (fun y hy ↦ by simp [hy]) (by simp)
+@[deprecated (since := "2026-06-16")] alias contMDiff_model := ModelWithCorners.contMDiff
 
-theorem contMDiffOn_model_symm : ContMDiffOn 𝓘(𝕜, E) I n I.symm (range I) := by
-  rw [contMDiffOn_iff]
-  refine ⟨I.continuousOn_symm, fun x y => ?_⟩
-  simp only [mfld_simps]
-  exact contDiffOn_id.congr fun x' => I.right_inv
+variable (I) in
+theorem ModelWithCorners.contMDiffOn_symm : ContMDiffOn 𝓘(𝕜, E) I n I.symm (range I) := by
+  intro x hx
+  apply contMDiffWithinAt_iff.mpr ⟨by fun_prop, ?_⟩
+  simpa using contDiffWithinAt_id.congr (fun y hy ↦ by simp [hy]) (by simp [hx])
+@[deprecated (since := "2026-06-16")]
+alias contMDiffOn_model_symm := ModelWithCorners.contMDiffOn_symm
 
 /-- An atlas member is `C^n` for any `n`. -/
 theorem contMDiffOn_of_mem_maximalAtlas (h : e ∈ maximalAtlas I n M) :
@@ -89,7 +90,7 @@ theorem contMDiffOn_chart_symm [IsManifold I n M] :
 
 theorem contMDiffAt_extend {x : M} (he : e ∈ maximalAtlas I n M) (hx : x ∈ e.source) :
     ContMDiffAt I 𝓘(𝕜, E) n (e.extend I) x :=
-  (contMDiff_model _).comp x <| contMDiffAt_of_mem_maximalAtlas he hx
+  (I.contMDiff _).comp x <| contMDiffAt_of_mem_maximalAtlas he hx
 
 theorem contMDiffOn_extend (he : e ∈ maximalAtlas I n M) :
     ContMDiffOn I 𝓘(𝕜, E) n (e.extend I) e.source :=
@@ -112,7 +113,7 @@ theorem contMDiffOn_extChartAt [IsManifold I n M] :
 theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) :
     ContMDiffOn 𝓘(𝕜, E) I n (e.extend I).symm (I '' e.target) := by
   refine (contMDiffOn_symm_of_mem_maximalAtlas he).comp
-    (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_
+    (I.contMDiffOn_symm.mono <| image_subset_range _ _) ?_
   simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm,
     preimage_preimage, I.left_inv, preimage_id']; rfl
 
@@ -155,6 +156,24 @@ theorem contMDiffOn_of_mem_contDiffGroupoid {e' : OpenPartialHomeomorph H H}
     (h : e' ∈ contDiffGroupoid n I) : ContMDiffOn I I n e' e'.source :=
   (contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_groupoid contDiffWithinAtProp_id h
 
+lemma OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn (φ : OpenPartialHomeomorph H H)
+    (hφ : ContMDiffOn I I n φ φ.source) (hφ' : ContMDiffOn I I n φ.symm φ.target) :
+    φ ∈ maximalAtlas I n H := by
+  simp only [mfld_simps, IsManifold.mem_maximalAtlas_iff, StructureGroupoid.maximalAtlas, forall_eq,
+    contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid,
+    ← contMDiffOn_iff_contDiffOn]
+  refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
+  all_goals apply I.contMDiff.comp_contMDiffOn
+  · exact hφ'.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
+  · exact hφ.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
+  · exact hφ.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
+  · exact hφ'.comp (I.contMDiffOn_symm.mono (by simp)) (by simp)
+
+lemma IsManifold.mem_maximalAtlas_iff_contMDiffOn (φ : OpenPartialHomeomorph H H) :
+    φ ∈ maximalAtlas I n H ↔ ContMDiffOn I I n φ φ.source ∧ ContMDiffOn I I n φ.symm φ.target :=
+  ⟨fun h ↦ ⟨contMDiffOn_of_mem_maximalAtlas h, contMDiffOn_symm_of_mem_maximalAtlas h⟩,
+   fun ⟨hφ, hφ'⟩ ↦ φ.mem_maximalAtlas_of_contMDiffOn hφ hφ'⟩
+
 end Atlas
 
 /-! ### (local) structomorphisms are `C^n` -/

Mathlib/Geometry/Manifold/PartitionOfUnity.lean

@@ -736,7 +736,7 @@ lemma IsOpen.exists_contMDiff_support_eq_aux {s : Set H} (hs : IsOpen s) :
   refine ⟨f ∘ I, ?_, ?_, ?_⟩
   · rw [support_comp_eq_preimage, f_supp, ← preimage_comp]
     simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]
-  · exact f_diff.comp_contMDiff contMDiff_model
+  · exact f_diff.comp_contMDiff I.contMDiff
   · exact Subset.trans (range_comp_subset_range _ _) f_range
 
 @[deprecated (since := "2025-12-17")]