refactor: extract and name the pregroupoid underlying contDiffGroupoid (

#9091)

This will be used for proving the inverse function theorem on manifolds. 



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: grunweg <grunweg@posteo.de>

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -529,46 +529,48 @@ variable {m n : ℕ∞} {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*
 
 variable (n)
 
-/-- Given a model with corners `(E, H)`, we define the groupoid of `C^n` transformations of `H` as
-the maps that are `C^n` when read in `E` through `I`. -/
+/-- Given a model with corners `(E, H)`, we define the pregroupoid of `C^n` transformations of `H`
+as the maps that are `C^n` when read in `E` through `I`. -/
+def contDiffPregroupoid : Pregroupoid H where
+  property f s := ContDiffOn 𝕜 n (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I)
+  comp {f g u v} hf hg _ _ _ := by
+    have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
+    simp only [this]
+    refine hg.comp (hf.mono fun x ⟨hx1, hx2⟩ ↦ ⟨hx1.1, hx2⟩) ?_
+    rintro x ⟨hx1, _⟩
+    simp only [mfld_simps] at hx1 ⊢
+    exact hx1.2
+  id_mem := by
+    apply ContDiffOn.congr contDiff_id.contDiffOn
+    rintro x ⟨_, hx2⟩
+    rcases mem_range.1 hx2 with ⟨y, hy⟩
+    rw [← hy]
+    simp only [mfld_simps]
+  locality {f u} _ H := by
+    apply contDiffOn_of_locally_contDiffOn
+    rintro y ⟨hy1, hy2⟩
+    rcases mem_range.1 hy2 with ⟨x, hx⟩
+    rw [← hx] at hy1 ⊢
+    simp only [mfld_simps] at hy1 ⊢
+    rcases H x hy1 with ⟨v, v_open, xv, hv⟩
+    have : I.symm ⁻¹' (u ∩ v) ∩ range I = I.symm ⁻¹' u ∩ range I ∩ I.symm ⁻¹' v := by
+      rw [preimage_inter, inter_assoc, inter_assoc]
+      congr 1
+      rw [inter_comm]
+    rw [this] at hv
+    exact ⟨I.symm ⁻¹' v, v_open.preimage I.continuous_symm, by simpa, hv⟩
+  congr {f g u} _ fg hf := by
+    apply hf.congr
+    rintro y ⟨hy1, hy2⟩
+    rcases mem_range.1 hy2 with ⟨x, hx⟩
+    rw [← hx] at hy1 ⊢
+    simp only [mfld_simps] at hy1 ⊢
+    rw [fg _ hy1]
+
+/-- Given a model with corners `(E, H)`, we define the groupoid of invertible `C^n` transformations
+  of `H` as the invertible maps that are `C^n` when read in `E` through `I`. -/
 def contDiffGroupoid : StructureGroupoid H :=
-  Pregroupoid.groupoid
-    { property := fun f s => ContDiffOn 𝕜 n (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I)
-      comp := fun {f g u v} hf hg _ _ _ => by
-        have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp
-        simp only [this]
-        refine hg.comp (hf.mono ?_) ?_
-        · rintro x ⟨hx1, hx2⟩
-          exact ⟨hx1.1, hx2⟩
-        · rintro x ⟨hx1, _⟩
-          simp only [mfld_simps] at hx1 ⊢
-          exact hx1.2
-      id_mem := by
-        apply ContDiffOn.congr contDiff_id.contDiffOn
-        rintro x ⟨_, hx2⟩
-        rcases mem_range.1 hx2 with ⟨y, hy⟩
-        rw [← hy]
-        simp only [mfld_simps]
-      locality := fun {f u} _ H => by
-        apply contDiffOn_of_locally_contDiffOn
-        rintro y ⟨hy1, hy2⟩
-        rcases mem_range.1 hy2 with ⟨x, hx⟩
-        rw [← hx] at hy1 ⊢
-        simp only [mfld_simps] at hy1 ⊢
-        rcases H x hy1 with ⟨v, v_open, xv, hv⟩
-        have : I.symm ⁻¹' (u ∩ v) ∩ range I = I.symm ⁻¹' u ∩ range I ∩ I.symm ⁻¹' v := by
-          rw [preimage_inter, inter_assoc, inter_assoc]
-          congr 1
-          rw [inter_comm]
-        rw [this] at hv
-        exact ⟨I.symm ⁻¹' v, v_open.preimage I.continuous_symm, by simpa, hv⟩
-      congr := fun {f g u} _ fg hf => by
-        apply hf.congr
-        rintro y ⟨hy1, hy2⟩
-        rcases mem_range.1 hy2 with ⟨x, hx⟩
-        rw [← hx] at hy1 ⊢
-        simp only [mfld_simps] at hy1 ⊢
-        rw [fg _ hy1] }
+  Pregroupoid.groupoid (contDiffPregroupoid n I)
 #align cont_diff_groupoid contDiffGroupoid
 
 variable {n}
@@ -590,7 +592,7 @@ theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H :
   -- we have to check that every partial homeomorphism belongs to `contDiffGroupoid 0 I`,
   -- by unfolding its definition
   change u ∈ contDiffGroupoid 0 I
-  rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
+  rw [contDiffGroupoid, mem_groupoid_of_pregroupoid, contDiffPregroupoid]
   simp only [contDiffOn_zero]
   constructor
   · refine' I.continuous.comp_continuousOn (u.continuousOn.comp I.continuousOn_symm _)
@@ -606,7 +608,7 @@ theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
     PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I := by
   rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
   suffices h : ContDiffOn 𝕜 n (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I)
-  · simp [h]
+  · simp [h, contDiffPregroupoid]
   have : ContDiffOn 𝕜 n id (univ : Set E) := contDiff_id.contDiffOn
   exact this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)
 #align of_set_mem_cont_diff_groupoid ofSet_mem_contDiffGroupoid
@@ -629,7 +631,8 @@ theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCor
   cases' he with he he_symm
   cases' he' with he' he'_symm
   simp only at he he_symm he' he'_symm
-  constructor <;> simp only [PartialEquiv.prod_source, PartialHomeomorph.prod_toPartialEquiv]
+  constructor <;> simp only [PartialEquiv.prod_source, PartialHomeomorph.prod_toPartialEquiv,
+    contDiffPregroupoid]
   · have h3 := ContDiffOn.prod_map he he'
     rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3
     rw [← (I.prod I').image_eq]
@@ -801,7 +804,7 @@ theorem mem_analyticGroupoid_of_boundaryless [CompleteSpace E] [I.Boundaryless]
   · intro he
     apply And.intro
     all_goals apply mem_groupoid_of_pregroupoid.mpr; simp only [I.image_eq, I.range_eq_univ,
-      interior_univ, subset_univ, and_true] at he ⊢
+      interior_univ, subset_univ, and_true, contDiffPregroupoid] at he ⊢
     · exact ⟨he.left.contDiffOn, he.right.contDiffOn⟩
     · exact he