refactor(PartialHomeomorph): make (s : Opens \alpha) implicit (#10082)

It is always used in conjunction with a hypothesis `hs` about `s`.

In Lean 3, these arguments were kept explicit on purpose: given a definition `myDef {x : α} (hx : MyProp x)`,
if the proof of `hx` was nontrivial (not a variable), Lean would pretty-print it as `myDef _`.

In Lean 4, setting `pp.proofs.withType` or `pp.proofs` to true makes such terms pretty-print as `myDef (x : MyProp)`.
Hence, this workaround is no longer necessary.

Follow-up to #9894.

Author: grunweg

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, {(chartAt H x.1).subtypeRestr s ⟨x⟩}
-  chartAt x := (chartAt H x.1).subtypeRestr s ⟨x⟩
+  atlas := ⋃ x : s, {(chartAt H x.1).subtypeRestr ⟨x⟩}
+  chartAt x := (chartAt H x.1).subtypeRestr ⟨x⟩
   mem_chart_source x := ⟨trivial, mem_chart_source H x.1⟩
   chart_mem_atlas x := by
     simp only [mem_iUnion, mem_singleton_iff]
@@ -1163,7 +1163,7 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G
     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 := 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
@@ -1172,18 +1172,18 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G
 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 e := chartAt H x.val
-  have heUx_nhds : (e.subtypeRestr U ⟨x⟩).target ∈ 𝓝 (e x) := by
-    apply (e.subtypeRestr U ⟨x⟩).open_target.mem_nhds
+  have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
+    apply (e.subtypeRestr ⟨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⟩)
+  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨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 e := chartAt H (x : M)
-  have heUx_nhds : (e.subtypeRestr U ⟨x⟩).target ∈ 𝓝 (e x) := by
-    apply (e.subtypeRestr U ⟨x⟩).open_target.mem_nhds
+  have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
+    apply (e.subtypeRestr ⟨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

Mathlib/Topology/PartialHomeomorph.lean

@@ -1464,32 +1464,31 @@ open TopologicalSpace
 
 variable (e : PartialHomeomorph X Y)
 
-variable (s : Opens X) (hs : Nonempty s)
+variable {s : Opens X} (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 Y :=
   (s.partialHomeomorphSubtypeCoe hs).trans e
 #align local_homeomorph.subtype_restr PartialHomeomorph.subtypeRestr
 
-theorem subtypeRestr_def : e.subtypeRestr s hs = (s.partialHomeomorphSubtypeCoe hs).trans e :=
+theorem subtypeRestr_def : e.subtypeRestr 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 hs : PartialHomeomorph s Y) : s → Y) = Set.restrict ↑s (e : X → Y) :=
+    ((e.subtypeRestr hs : PartialHomeomorph s Y) : s → Y) = Set.restrict ↑s (e : X → Y) :=
   rfl
 #align local_homeomorph.subtype_restr_coe PartialHomeomorph.subtypeRestr_coe
 
 @[simp, mfld_simps]
-theorem subtypeRestr_source : (e.subtypeRestr s hs).source = (↑) ⁻¹' e.source := by
+theorem subtypeRestr_source : (e.subtypeRestr 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 : X) ∈ e.source) :
-    e x ∈ (e.subtypeRestr s hs).target := by
+    e x ∈ (e.subtypeRestr hs).target := by
   refine' ⟨e.map_source hxe, _⟩
   rw [s.partialHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
   exact x.prop
@@ -1498,7 +1497,7 @@ theorem map_subtype_source {x : s} (hxe : (x : X) ∈ e.source) :
 /- 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 X Y) :
-    (f.subtypeRestr s hs).symm.trans (f'.subtypeRestr s hs) ≈
+    (f.subtypeRestr hs).symm.trans (f'.subtypeRestr 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
@@ -1515,17 +1514,17 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph X Y) :
   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 X) (hU : Nonempty U) :
-    EqOn e.symm (Subtype.val ∘ (e.subtypeRestr U hU).symm) (e.subtypeRestr U hU).target := by
+theorem subtypeRestr_symm_eqOn {U : Opens X} (hU : Nonempty U) :
+    EqOn e.symm (Subtype.val ∘ (e.subtypeRestr hU).symm) (e.subtypeRestr hU).target := by
   intro y hy
   rw [eq_comm, eq_symm_apply _ _ hy.1]
   · change restrict _ e _ = _
-    rw [← subtypeRestr_coe, (e.subtypeRestr U hU).right_inv hy]
+    rw [← subtypeRestr_coe, (e.subtypeRestr hU).right_inv hy]
   · have := map_target _ hy; rwa [subtypeRestr_source] at this
 
 theorem subtypeRestr_symm_eqOn_of_le {U V : Opens X} (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
+    (hUV : U ≤ V) : EqOn (e.subtypeRestr hV).symm (Set.inclusion hUV ∘ (e.subtypeRestr hU).symm)
+      (e.subtypeRestr hU).target := by
   set i := Set.inclusion hUV
   intro y hy
   dsimp [PartialHomeomorph.subtypeRestr_def] at hy ⊢