feat: drop HasGroupoid assumption in several LiftPropAt lemmas (#40475)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -36,7 +36,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
   {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] {n : ℕ∞ω}
-  [IsManifold I n M]
   -- declare a topological space `M'`.
   {M' : Type*} [TopologicalSpace M']
   -- declare functions, sets, points and smoothness indices
@@ -80,10 +79,12 @@ theorem contMDiffAt_symm_of_mem_maximalAtlas {x : H} (h : e ∈ maximalAtlas I n
     (hx : x ∈ e.target) : ContMDiffAt I I n e.symm x :=
   (contMDiffOn_symm_of_mem_maximalAtlas h).contMDiffAt <| e.open_target.mem_nhds hx
 
-theorem contMDiffOn_chart : ContMDiffOn I I n (chartAt H x) (chartAt H x).source :=
+theorem contMDiffOn_chart [IsManifold I n M] :
+    ContMDiffOn I I n (chartAt H x) (chartAt H x).source :=
   contMDiffOn_of_mem_maximalAtlas <| chart_mem_maximalAtlas x
 
-theorem contMDiffOn_chart_symm : ContMDiffOn I I n (chartAt H x).symm (chartAt H x).target :=
+theorem contMDiffOn_chart_symm [IsManifold I n M] :
+    ContMDiffOn I I n (chartAt H x).symm (chartAt H x).target :=
   contMDiffOn_symm_of_mem_maximalAtlas <| chart_mem_maximalAtlas x
 
 theorem contMDiffAt_extend {x : M} (he : e ∈ maximalAtlas I n M) (hx : x ∈ e.source) :
@@ -94,18 +95,18 @@ theorem contMDiffOn_extend (he : e ∈ maximalAtlas I n M) :
     ContMDiffOn I 𝓘(𝕜, E) n (e.extend I) e.source :=
   fun _x' hx' ↦ (contMDiffAt_extend he hx').contMDiffWithinAt
 
-theorem contMDiffAt_extChartAt' {x' : M} (h : x' ∈ (chartAt H x).source) :
+theorem contMDiffAt_extChartAt' [IsManifold I n M] {x' : M} (h : x' ∈ (chartAt H x).source) :
     ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x) x' :=
   contMDiffAt_extend (chart_mem_maximalAtlas x) h
 
-omit [IsManifold I n M] in
 theorem contMDiffAt_extChartAt : ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x) x := by
   rw [contMDiffAt_iff_source]
   apply contMDiffWithinAt_id.congr_of_eventuallyEq_of_mem _ (by simp)
   filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
   exact PartialEquiv.right_inv (extChartAt I x) hy
 
-theorem contMDiffOn_extChartAt : ContMDiffOn I 𝓘(𝕜, E) n (extChartAt I x) (chartAt H x).source :=
+theorem contMDiffOn_extChartAt [IsManifold I n M] :
+    ContMDiffOn I 𝓘(𝕜, E) n (extChartAt I x) (chartAt H x).source :=
   contMDiffOn_extend (chart_mem_maximalAtlas x)
 
 theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) :
@@ -115,25 +116,23 @@ theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) :
   simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm,
     preimage_preimage, I.left_inv, preimage_id']; rfl
 
-theorem contMDiffOn_extChartAt_symm (x : M) :
+theorem contMDiffOn_extChartAt_symm [IsManifold I n M] (x : M) :
     ContMDiffOn 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target := by
   convert! contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)
   · rw [extChartAt_target, I.image_eq]
   · infer_instance
-  · infer_instance
 
-theorem contMDiffWithinAt_extChartAt_symm_target
+theorem contMDiffWithinAt_extChartAt_symm_target [IsManifold I n M]
     (x : M) {y : E} (hy : y ∈ (extChartAt I x).target) :
     ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target y :=
   contMDiffOn_extChartAt_symm x y hy
 
-theorem contMDiffWithinAt_extChartAt_symm_range
+theorem contMDiffWithinAt_extChartAt_symm_range [IsManifold I n M]
     (x : M) {y : E} (hy : y ∈ (extChartAt I x).target) :
     ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (range I) y :=
   (contMDiffWithinAt_extChartAt_symm_target x hy).mono_of_mem_nhdsWithin
     (extChartAt_target_mem_nhdsWithin_of_mem hy)
 
-omit [IsManifold I n M] in
 theorem contMDiffWithinAt_extChartAt_symm_target_self (x : M) :
     ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target
       (extChartAt I x x) := by
@@ -146,7 +145,6 @@ theorem contMDiffWithinAt_extChartAt_symm_target_self (x : M) :
     convert! PartialEquiv.right_inv (extChartAt I x) hy
     simp
 
-omit [IsManifold I n M] in
 theorem contMDiffWithinAt_extChartAt_symm_range_self (x : M) :
     ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (range I) (extChartAt I x x) :=
   (contMDiffWithinAt_extChartAt_symm_target_self x).mono_of_mem_nhdsWithin
@@ -163,7 +161,7 @@ end Atlas
 
 section IsLocalStructomorph
 
-variable [ChartedSpace H M'] [IsM' : IsManifold I n M']
+variable [IsManifold I n M] [ChartedSpace H M'] [IsM' : IsManifold I n M']
 
 theorem isLocalStructomorphOn_contDiffGroupoid_iff_aux {f : OpenPartialHomeomorph M M'}
     (hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt f f.source) :
@@ -308,8 +306,7 @@ end IsLocalStructomorph
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
   {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
-  {n : ℕ∞ω}
-  [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M}
+  {n : ℕ∞ω} {f : M → N} {s : Set M}
   {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G}
 
 /-- This is a smooth analogue of `OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff`. -/

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -371,8 +371,6 @@ theorem contMDiffAt_iff_target_of_mem_source
   rw [ContMDiffAt, contMDiffWithinAt_iff_target_of_mem_source hy, continuousWithinAt_univ,
     ContMDiffAt]
 
-variable [IsManifold I n M] [IsManifold I' n M']
-
 theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtlas I n M)
     (he' : e' ∈ maximalAtlas I' n M') (hx : x ∈ e.source) (hy : f x ∈ e'.source) :
     ContMDiffWithinAt I I' n f s x ↔
@@ -396,7 +394,8 @@ theorem contMDiffWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I n M)
 
 /-- One can reformulate being `C^n` within a set at a point as continuity within this set at this
 point, and being `C^n` in any chart containing that point. -/
-theorem contMDiffWithinAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
+theorem contMDiffWithinAt_iff_of_mem_source [IsManifold I n M] [IsManifold I' n M']
+    {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
     (hy : f x' ∈ (chartAt H' y).source) :
     ContMDiffWithinAt I I' n f s x' ↔
       ContinuousWithinAt f s x' ∧
@@ -405,7 +404,8 @@ theorem contMDiffWithinAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (char
   contMDiffWithinAt_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x)
     (chart_mem_maximalAtlas y) hx hy
 
-theorem contMDiffWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
+theorem contMDiffWithinAt_iff_of_mem_source' [IsManifold I n M] [IsManifold I' n M']
+    {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
     (hy : f x' ∈ (chartAt H' y).source) :
     ContMDiffWithinAt I I' n f s x' ↔
       ContinuousWithinAt f s x' ∧
@@ -423,7 +423,8 @@ theorem contMDiffWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (cha
     ← map_extChartAt_nhdsWithin' hx, inter_comm, nhdsWithin_inter_of_mem]
   exact hc (extChartAt_source_mem_nhds' hy)
 
-theorem contMDiffAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
+theorem contMDiffAt_iff_of_mem_source [IsManifold I n M] [IsManifold I' n M']
+    {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
     (hy : f x' ∈ (chartAt H' y).source) :
     ContMDiffAt I I' n f x' ↔
       ContinuousAt f x' ∧
@@ -452,7 +453,8 @@ into a single chart, the fact that `f` is `C^n` on that set can be expressed by
 these charts.
 Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
 that this set lies in `(extChartAt I x).target`. -/
-theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source)
+theorem contMDiffOn_iff_of_subset_source [IsManifold I n M] [IsManifold I' n M']
+    {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source)
     (h2s : MapsTo f s (chartAt H' y).source) :
     ContMDiffOn I I' n f s ↔
       ContinuousOn f s ∧
@@ -465,7 +467,8 @@ into a single chart, the fact that `f` is `C^n` on that set can be expressed by
 these charts.
 Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
 that this set lies in `(extChartAt I x).target`. -/
-theorem contMDiffOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source)
+theorem contMDiffOn_iff_of_subset_source' [IsManifold I n M] [IsManifold I' n M']
+    {x : M} {y : M'} (hs : s ⊆ (extChartAt I x).source)
     (h2s : MapsTo f s (extChartAt I' y).source) :
     ContMDiffOn I I' n f s ↔
         ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) := by
@@ -475,7 +478,7 @@ theorem contMDiffOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChart
 
 /-- One can reformulate being `C^n` on a set as continuity on this set, and being `C^n` in any
 extended chart. -/
-theorem contMDiffOn_iff :
+theorem contMDiffOn_iff [IsManifold I n M] [IsManifold I' n M'] :
     ContMDiffOn I I' n f s ↔
       ContinuousOn f s ∧
         ∀ (x : M) (y : M'),
@@ -518,7 +521,7 @@ theorem contMDiffOn_zero_iff :
 
 /-- One can reformulate being `C^n` on a set as continuity on this set, and being `C^n` in any
 extended chart in the target. -/
-theorem contMDiffOn_iff_target :
+theorem contMDiffOn_iff_target [IsManifold I n M] [IsManifold I' n M'] :
     ContMDiffOn I I' n f s ↔
       ContinuousOn f s ∧
         ∀ y : M',
@@ -536,7 +539,7 @@ theorem contMDiffOn_iff_target :
 
 
 /-- One can reformulate being `C^n` as continuity and being `C^n` in any extended chart. -/
-theorem contMDiff_iff :
+theorem contMDiff_iff [IsManifold I n M] [IsManifold I' n M'] :
     ContMDiff I I' n f ↔
       Continuous f ∧
         ∀ (x : M) (y : M'),
@@ -547,7 +550,7 @@ theorem contMDiff_iff :
 
 /-- One can reformulate being `C^n` as continuity and being `C^n` in any extended chart in the
 target. -/
-theorem contMDiff_iff_target :
+theorem contMDiff_iff_target [IsManifold I n M] [IsManifold I' n M'] :
     ContMDiff I I' n f ↔
       Continuous f ∧ ∀ y : M',
         ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) (f ⁻¹' (extChartAt I' y).source) := by

Mathlib/Geometry/Manifold/HasGroupoid.lean

@@ -105,6 +105,16 @@ theorem mem_maximalAtlas_iff {e : OpenPartialHomeomorph M H} :
     e ∈ G.maximalAtlas M ↔ ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G :=
   Iff.rfl
 
+theorem StructureGroupoid.compatible_of_mem_maximalAtlas_right
+    {e' : OpenPartialHomeomorph M H} {x : M}
+    (he' : e' ∈ G.maximalAtlas M) : (chartAt H x).symm ≫ₕ e' ∈ G :=
+  (he' _ (ChartedSpace.chart_mem_atlas x)).2
+
+theorem StructureGroupoid.compatible_of_mem_maximalAtlas_left
+    {e' : OpenPartialHomeomorph M H} {x : M}
+    (he' : e' ∈ G.maximalAtlas M) : e'.symm ≫ₕ chartAt H x ∈ G :=
+  (he' _ (ChartedSpace.chart_mem_atlas x)).1
+
 /-- Changing coordinates between two elements of the maximal atlas gives rise to an element
 of the structure groupoid. -/
 theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : OpenPartialHomeomorph M H}

Mathlib/Geometry/Manifold/Immersion.lean

@@ -74,10 +74,6 @@ This shortens the overall argument, as the definition of submersions has the sam
   `IsImmersion(At)OfComplement.small` and `IsImmersion(At)OfComplement.smallEquiv`.
 
 ## TODO
-* Remove the `IsManifold I n M` and `IsManifold J n N` hypotheses from `IsImmersionAt.contMDiffAt`
-  and all its variants; these are superfluous. By hypothesis, `h.domChart` and `h.codChart` are in
-  the maximal atlas for `M` resp. `N`; this implies that smoothness of `f` can be tested w.r.t.
-  these charts (without any `IsManifold` hypotheses).
 * 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`.
 * If `f` is an immersion at `x`, its differential splits, hence is injective.
@@ -408,8 +404,6 @@ theorem continuousOn (h : IsImmersionAtOfComplement F I J n f x) :
 theorem continuousAt (h : IsImmersionAtOfComplement F I J n f x) : ContinuousAt f x :=
   h.continuousOn.continuousAt (h.domChart.open_source.mem_nhds (mem_domChart_source h))
 
-variable [IsManifold I n M] [IsManifold J n N]
-
 /-- Prefer using `IsImmersionAtOfComplement.contMDiffAt` instead -/
 theorem contMDiffOn (h : IsImmersionAtOfComplement F I J n f x) :
     CMDiff[h.domChart.source] n f := by
@@ -601,8 +595,6 @@ theorem continuousOn (h : IsImmersionAt I J n f x) : ContinuousOn f h.domChart.s
 theorem continuousAt (h : IsImmersionAt I J n f x) : ContinuousAt f x :=
   h.isImmersionAtOfComplement_complement.continuousAt
 
-variable [IsManifold I n M] [IsManifold J n N]
-
 /-- Prefer using `IsImmersionAt.contMDiffAt` instead -/
 theorem contMDiffOn (h : IsImmersionAt I J n f x) : CMDiff[h.domChart.source] n f :=
   h.isImmersionAtOfComplement_complement.contMDiffOn
@@ -707,7 +699,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) :
 @[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
 
 /-- A `C^n` immersion is `C^n`. -/
-theorem contMDiff [IsManifold I n M] [IsManifold J n N]
+theorem contMDiff
     (h : IsImmersionOfComplement F I J n f) : CMDiff n f :=
   fun x ↦ (h x).contMDiffAt
 
@@ -774,7 +766,7 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) :
 @[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
 
 /-- A `C^n` immersion is `C^n`. -/
-theorem contMDiff [IsManifold I n M] [IsManifold J n N]
+theorem contMDiff
     (h : IsImmersion I J n f) : CMDiff n f :=
   h.isImmersionOfComplement_complement.contMDiff