refactor(PartialHomeomorph): make [Nonempty s] explicit (#9894)

winstonyin · winstonyin · commit ca91ff1e242b · 2024-01-27T11:43:26.000Z
Subsets aren't going to have `Nonempty` instances on them, typically, so one would have to manually construct a term of `[Nonempty s]` whenever `PartialHomeomorph.subtypeRestr` is used. Turning this instance argument explicit, `(hs : Nonempty s)` would help us avoid `@PartialHomeomorph.subtypeRestr _ _ _ _` constructions or `haveI : Nonempty ...`.

Its only downstream effect currently is in `ChartedSpace.lean`.
diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -1146,8 +1146,8 @@ variable (s : Opens M)
 
 /-- An open subset of a charted space is naturally a charted space. -/
 protected instance instChartedSpace : ChartedSpace H s where
-  atlas := ⋃ x : s, {@PartialHomeomorph.subtypeRestr _ _ _ _ (chartAt H x.1) s ⟨x⟩}
-  chartAt x := @PartialHomeomorph.subtypeRestr _ _ _ _ (chartAt H x.1) s ⟨x⟩
+  atlas := ⋃ x : s, {(chartAt H x.1).subtypeRestr s ⟨x⟩}
+  chartAt x := (chartAt H x.1).subtypeRestr s ⟨x⟩
   mem_chart_source x := ⟨trivial, mem_chart_source H x.1⟩
   chart_mem_atlas x := by
     simp only [mem_iUnion, mem_singleton_iff]
@@ -1159,42 +1159,35 @@ protected instance instChartedSpace : ChartedSpace H s where
 protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G where
   compatible := by
     rintro e e' ⟨_, ⟨x, hc⟩, he⟩ ⟨_, ⟨x', hc'⟩, he'⟩
-    haveI : Nonempty s := ⟨x⟩
     rw [hc.symm, mem_singleton_iff] at he
     rw [hc'.symm, mem_singleton_iff] at he'
     rw [he, he']
     refine' G.mem_of_eqOnSource _
-      (subtypeRestr_symm_trans_subtypeRestr s (chartAt H x) (chartAt H x'))
+      (subtypeRestr_symm_trans_subtypeRestr s _ (chartAt H x) (chartAt H x'))
     apply closedUnderRestriction'
     · exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _)
     · exact isOpen_inter_preimage_symm (chartAt _ _) s.2
 #align topological_space.opens.has_groupoid TopologicalSpace.Opens.instHasGroupoid
 
 theorem chartAt_subtype_val_symm_eventuallyEq (U : Opens M) {x : U} :
     (chartAt H x.val).symm =ᶠ[𝓝 (chartAt H x.val x.val)] Subtype.val ∘ (chartAt H x).symm := by
-  set i : U → M := Subtype.val
   set e := chartAt H x.val
-  haveI : Nonempty U := ⟨x⟩
-  haveI : Nonempty M := ⟨i x⟩
-  have heUx_nhds : (e.subtypeRestr U).target ∈ 𝓝 (e x) := by
-    apply (e.subtypeRestr U).open_target.mem_nhds
-    exact e.map_subtype_source (mem_chart_source _ _)
-  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn U)
+  have heUx_nhds : (e.subtypeRestr U ⟨x⟩).target ∈ 𝓝 (e x) := by
+    apply (e.subtypeRestr U ⟨x⟩).open_target.mem_nhds
+    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
+  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn U ⟨x⟩)
 
 theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
     (chartAt H (Set.inclusion hUV x)).symm
     =ᶠ[𝓝 (chartAt H (Set.inclusion hUV x) (Set.inclusion hUV x))]
     Set.inclusion hUV ∘ (chartAt H x).symm := by
-  set i := Set.inclusion hUV
   set e := chartAt H (x : M)
-  haveI : Nonempty U := ⟨x⟩
-  haveI : Nonempty V := ⟨i x⟩
-  have heUx_nhds : (e.subtypeRestr U).target ∈ 𝓝 (e x) := by
-    apply (e.subtypeRestr U).open_target.mem_nhds
-    exact e.map_subtype_source (mem_chart_source _ _)
-  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn_of_le hUV)
+  have heUx_nhds : (e.subtypeRestr U ⟨x⟩).target ∈ 𝓝 (e x) := by
+    apply (e.subtypeRestr U ⟨x⟩).open_target.mem_nhds
+    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
+  exact Filter.eventuallyEq_of_mem heUx_nhds <| e.subtypeRestr_symm_eqOn_of_le ⟨x⟩
+    ⟨Set.inclusion hUV x⟩ hUV
 #align topological_space.opens.chart_at_inclusion_symm_eventually_eq TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq
-
 end TopologicalSpace.Opens
 
 /-! ### Structomorphisms -/
diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean
@@ -1393,7 +1393,10 @@ end OpenEmbedding
 /- inclusion of an open set in a topological space -/
 namespace TopologicalSpace.Opens
 
-variable (s : Opens α) [Nonempty s]
+/- `Nonempty s` is not a type class argument because `s`, being a subset, rarely comes with a type
+class instance. Then we'd have to manually provide the instance every time we use the following
+lemmas, tediously using `haveI := ...` or `@foobar _ _ _ ...`. -/
+variable (s : Opens α) (hs : Nonempty s)
 
 /-- The inclusion of an open subset `s` of a space `α` into `α` is a partial homeomorphism from the
 subtype `s` to `α`. -/
@@ -1402,17 +1405,17 @@ noncomputable def partialHomeomorphSubtypeCoe : PartialHomeomorph s α :=
 #align topological_space.opens.local_homeomorph_subtype_coe TopologicalSpace.Opens.partialHomeomorphSubtypeCoe
 
 @[simp, mfld_simps]
-theorem partialHomeomorphSubtypeCoe_coe : (s.partialHomeomorphSubtypeCoe : s → α) = (↑) :=
+theorem partialHomeomorphSubtypeCoe_coe : (s.partialHomeomorphSubtypeCoe hs : s → α) = (↑) :=
   rfl
 #align topological_space.opens.local_homeomorph_subtype_coe_coe TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_coe
 
 @[simp, mfld_simps]
-theorem partialHomeomorphSubtypeCoe_source : s.partialHomeomorphSubtypeCoe.source = Set.univ :=
+theorem partialHomeomorphSubtypeCoe_source : (s.partialHomeomorphSubtypeCoe hs).source = Set.univ :=
   rfl
 #align topological_space.opens.local_homeomorph_subtype_coe_source TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_source
 
 @[simp, mfld_simps]
-theorem partialHomeomorphSubtypeCoe_target : s.partialHomeomorphSubtypeCoe.target = s := by
+theorem partialHomeomorphSubtypeCoe_target : (s.partialHomeomorphSubtypeCoe hs).target = s := by
   simp only [partialHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
   rfl
 #align topological_space.opens.local_homeomorph_subtype_coe_target TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_target
@@ -1459,31 +1462,32 @@ open TopologicalSpace
 
 variable (e : PartialHomeomorph α β)
 
-variable (s : Opens α) [Nonempty s]
+variable (s : Opens α) (hs : Nonempty s)
 
 /-- The restriction of a partial homeomorphism `e` to an open subset `s` of the domain type
 produces a partial homeomorphism whose domain is the subtype `s`. -/
 noncomputable def subtypeRestr : PartialHomeomorph s β :=
-  s.partialHomeomorphSubtypeCoe.trans e
+  (s.partialHomeomorphSubtypeCoe hs).trans e
 #align local_homeomorph.subtype_restr PartialHomeomorph.subtypeRestr
 
-theorem subtypeRestr_def : e.subtypeRestr s = s.partialHomeomorphSubtypeCoe.trans e :=
+theorem subtypeRestr_def : e.subtypeRestr s hs = (s.partialHomeomorphSubtypeCoe hs).trans e :=
   rfl
 #align local_homeomorph.subtype_restr_def PartialHomeomorph.subtypeRestr_def
 
 @[simp, mfld_simps]
 theorem subtypeRestr_coe :
-    ((e.subtypeRestr s : PartialHomeomorph s β) : s → β) = Set.restrict ↑s (e : α → β) :=
+    ((e.subtypeRestr s hs : PartialHomeomorph s β) : s → β) = Set.restrict ↑s (e : α → β) :=
   rfl
 #align local_homeomorph.subtype_restr_coe PartialHomeomorph.subtypeRestr_coe
 
 @[simp, mfld_simps]
-theorem subtypeRestr_source : (e.subtypeRestr s).source = (↑) ⁻¹' e.source := by
+theorem subtypeRestr_source : (e.subtypeRestr s hs).source = (↑) ⁻¹' e.source := by
   simp only [subtypeRestr_def, mfld_simps]
 #align local_homeomorph.subtype_restr_source PartialHomeomorph.subtypeRestr_source
 
 variable {s} in
-theorem map_subtype_source {x : s} (hxe : (x : α) ∈ e.source): e x ∈ (e.subtypeRestr s).target := by
+theorem map_subtype_source {x : s} (hxe : (x : α) ∈ e.source) :
+    e x ∈ (e.subtypeRestr s hs).target := by
   refine' ⟨e.map_source hxe, _⟩
   rw [s.partialHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
   exact x.prop
@@ -1492,7 +1496,7 @@ theorem map_subtype_source {x : s} (hxe : (x : α) ∈ e.source): e x ∈ (e.sub
 /- This lemma characterizes the transition functions of an open subset in terms of the transition
 functions of the original space. -/
 theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph α β) :
-    (f.subtypeRestr s).symm.trans (f'.subtypeRestr s) ≈
+    (f.subtypeRestr s hs).symm.trans (f'.subtypeRestr s hs) ≈
       (f.symm.trans f').restr (f.target ∩ f.symm ⁻¹' s) := by
   simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]
   have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.isOpen_inter_preimage_symm s.2
@@ -1505,35 +1509,35 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph α β) :
   rw [ofSet_trans', sets_identity, ← trans_of_set' _ openness₂, trans_assoc]
   refine' EqOnSource.trans' (eqOnSource_refl _) _
   -- f has been eliminated !!!
-  refine' Setoid.trans (symm_trans_self s.partialHomeomorphSubtypeCoe) _
+  refine' Setoid.trans (symm_trans_self (s.partialHomeomorphSubtypeCoe hs)) _
   simp only [mfld_simps, Setoid.refl]
 #align local_homeomorph.subtype_restr_symm_trans_subtype_restr PartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr
 
-theorem subtypeRestr_symm_eqOn (U : Opens α) [Nonempty U] :
-    EqOn e.symm (Subtype.val ∘ (e.subtypeRestr U).symm) (e.subtypeRestr U).target := by
+theorem subtypeRestr_symm_eqOn (U : Opens α) (hU : Nonempty U) :
+    EqOn e.symm (Subtype.val ∘ (e.subtypeRestr U hU).symm) (e.subtypeRestr U hU).target := by
   intro y hy
   rw [eq_comm, eq_symm_apply _ _ hy.1]
   · change restrict _ e _ = _
-    rw [← subtypeRestr_coe, (e.subtypeRestr U).right_inv hy]
+    rw [← subtypeRestr_coe, (e.subtypeRestr U hU).right_inv hy]
   · have := map_target _ hy; rwa [subtypeRestr_source] at this
 
-theorem subtypeRestr_symm_eqOn_of_le {U V : Opens α} [Nonempty U] [Nonempty V] (hUV : U ≤ V) :
-    EqOn (e.subtypeRestr V).symm (Set.inclusion hUV ∘ (e.subtypeRestr U).symm)
-      (e.subtypeRestr U).target := by
+theorem subtypeRestr_symm_eqOn_of_le {U V : Opens α} (hU : Nonempty U) (hV : Nonempty V)
+    (hUV : U ≤ V) : EqOn (e.subtypeRestr V hV).symm (Set.inclusion hUV ∘ (e.subtypeRestr U hU).symm)
+      (e.subtypeRestr U hU).target := by
   set i := Set.inclusion hUV
   intro y hy
   dsimp [PartialHomeomorph.subtypeRestr_def] at hy ⊢
-  have hyV : e.symm y ∈ V.partialHomeomorphSubtypeCoe.target := by
+  have hyV : e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target := by
     rw [Opens.partialHomeomorphSubtypeCoe_target] at hy ⊢
     exact hUV hy.2
-  refine' V.partialHomeomorphSubtypeCoe.injOn _ trivial _
+  refine' (V.partialHomeomorphSubtypeCoe hV).injOn _ trivial _
   · rw [← PartialHomeomorph.symm_target]
     apply PartialHomeomorph.map_source
     rw [PartialHomeomorph.symm_source]
     exact hyV
-  · rw [V.partialHomeomorphSubtypeCoe.right_inv hyV]
-    show _ = U.partialHomeomorphSubtypeCoe _
-    rw [U.partialHomeomorphSubtypeCoe.right_inv hy.2]
+  · rw [(V.partialHomeomorphSubtypeCoe hV).right_inv hyV]
+    show _ = U.partialHomeomorphSubtypeCoe hU _
+    rw [(U.partialHomeomorphSubtypeCoe hU).right_inv hy.2]
 #align local_homeomorph.subtype_restr_symm_eq_on_of_le PartialHomeomorph.subtypeRestr_symm_eqOn_of_le
 
 end subtypeRestr
