refactor(PartialHomeomorph): Remove explicit variable (x : M). (#10083)

Instead, supply it as needed.

This replaces an explicit argument (x : M) by an implicit `{x : M}` in the following lemmas:
- extChartAt_source_mem_nhds'
- extChartAt_source_mem_nhdsWithin'
- continuousAt_extChartAt'
- extChartAt_image_nhd_mem_nhds_of_boundaryless
- extChartAt_target_mem_nhdsWithin'
- nhdsWithin_extChartAt_target_eq'
- continuousAt_extChartAt_symm'
- continuousAt_extChartAt_symm''
- map_extChartAt_nhdsWithin_eq_image'
- map_extChartAt_nhdsWithin'
- map_extChartAt_symm_nhdsWithin'
- map_extChartAt_symm_nhdsWithin_range'
- extChartAt_preimage_mem_nhdsWithin'
- extChartAt_preimage_mem_nhdsWithin
- extChartAt_preimage_mem_nhds'
- extChartAt_preimage_mem_nhds



Co-authored-by: grunweg <grunweg@posteo.de>

Author: grunweg

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -438,9 +438,9 @@ theorem contMDiffWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (cha
   rw [and_congr_right_iff]
   set e := extChartAt I x; set e' := extChartAt I' (f x)
   refine' fun hc => contDiffWithinAt_congr_nhds _
-  rw [← e.image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image' I x hx, ←
-    map_extChartAt_nhdsWithin' I x hx, inter_comm, nhdsWithin_inter_of_mem]
-  exact hc (extChartAt_source_mem_nhds' _ _ hy)
+  rw [← e.image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image' I hx, ←
+    map_extChartAt_nhdsWithin' I hx, inter_comm, nhdsWithin_inter_of_mem]
+  exact hc (extChartAt_source_mem_nhds' _ hy)
 #align cont_mdiff_within_at_iff_of_mem_source' contMDiffWithinAt_iff_of_mem_source'
 
 theorem contMDiffAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
@@ -465,7 +465,7 @@ theorem contMDiffWithinAt_iff_target_of_mem_source {x : M} {y : M'}
   simp_rw [StructureGroupoid.liftPropWithinAt_self_target]
   simp_rw [((chartAt H' y).continuousAt hy).comp_continuousWithinAt hf]
   rw [← extChartAt_source I'] at hy
-  simp_rw [(continuousAt_extChartAt' I' _ hy).comp_continuousWithinAt hf]
+  simp_rw [(continuousAt_extChartAt' I' hy).comp_continuousWithinAt hf]
   rfl
 #align cont_mdiff_within_at_iff_target_of_mem_source contMDiffWithinAt_iff_target_of_mem_source
 

Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

@@ -137,8 +137,8 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N →
       rw [(extChartAt I (g x₂)).left_inv hx, (extChartAt I' (f x₂ (g x₂))).left_inv h2x]
     refine' Filter.EventuallyEq.fderivWithin_eq_nhds _
     refine' eventually_of_mem (inter_mem _ _) this
-    · exact extChartAt_preimage_mem_nhds' _ _ hx₂ (extChartAt_source_mem_nhds I (g x₂))
-    refine' extChartAt_preimage_mem_nhds' _ _ hx₂ _
+    · exact extChartAt_preimage_mem_nhds' _ hx₂ (extChartAt_source_mem_nhds I (g x₂))
+    refine' extChartAt_preimage_mem_nhds' _ hx₂ _
     exact h2x₂.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds _ _)
   /- The conclusion is equal to the following, when unfolding coord_change of
       `tangentBundleCore` -/

Mathlib/Geometry/Manifold/IntegralCurve.lean

@@ -345,7 +345,7 @@ theorem exists_isIntegralCurveAt_of_contMDiffAt
     mem_of_mem_of_subset hf3' (extChartAt I x₀).target_subset_preimage_source
   have hft2 := mem_extChartAt_source I xₜ
   -- express the derivative of the integral curve in the local chart
-  refine ⟨(continuousAt_extChartAt_symm'' _ _ hf3').comp h.continuousAt,
+  refine ⟨(continuousAt_extChartAt_symm'' _ hf3').comp h.continuousAt,
     HasDerivWithinAt.hasFDerivWithinAt ?_⟩
   simp only [mfld_simps, hasDerivWithinAt_univ]
   show HasDerivAt ((extChartAt I xₜ ∘ (extChartAt I x₀).symm) ∘ f) (v xₜ) t

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -202,14 +202,14 @@ theorem hasMFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
     HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f' := by
   rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq,
     hasFDerivWithinAt_inter', continuousWithinAt_inter' h]
-  exact extChartAt_preimage_mem_nhdsWithin I x h
+  exact extChartAt_preimage_mem_nhdsWithin I h
 #align has_mfderiv_within_at_inter' hasMFDerivWithinAt_inter'
 
 theorem hasMFDerivWithinAt_inter (h : t ∈ 𝓝 x) :
     HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f' := by
   rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter,
     continuousWithinAt_inter h]
-  exact extChartAt_preimage_mem_nhds I x h
+  exact extChartAt_preimage_mem_nhds I h
 #align has_mfderiv_within_at_inter hasMFDerivWithinAt_inter
 
 theorem HasMFDerivWithinAt.union (hs : HasMFDerivWithinAt I I' f s x f')
@@ -294,14 +294,14 @@ theorem mdifferentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
     MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
   rw [MDifferentiableWithinAt, MDifferentiableWithinAt, extChartAt_preimage_inter_eq,
     differentiableWithinAt_inter, continuousWithinAt_inter ht]
-  exact extChartAt_preimage_mem_nhds I x ht
+  exact extChartAt_preimage_mem_nhds I ht
 #align mdifferentiable_within_at_inter mdifferentiableWithinAt_inter
 
 theorem mdifferentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
     MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
   rw [MDifferentiableWithinAt, MDifferentiableWithinAt, extChartAt_preimage_inter_eq,
     differentiableWithinAt_inter', continuousWithinAt_inter' ht]
-  exact extChartAt_preimage_mem_nhdsWithin I x ht
+  exact extChartAt_preimage_mem_nhdsWithin I ht
 #align mdifferentiable_within_at_inter' mdifferentiableWithinAt_inter'
 
 theorem MDifferentiableAt.mdifferentiableWithinAt (h : MDifferentiableAt I I' f x) :
@@ -350,7 +350,7 @@ theorem mfderivWithin_univ : mfderivWithin I I' f univ = mfderiv I I' f := by
 theorem mfderivWithin_inter (ht : t ∈ 𝓝 x) :
     mfderivWithin I I' f (s ∩ t) x = mfderivWithin I I' f s x := by
   rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
-    fderivWithin_inter (extChartAt_preimage_mem_nhds I x ht)]
+    fderivWithin_inter (extChartAt_preimage_mem_nhds I ht)]
 #align mfderiv_within_inter mfderivWithin_inter
 
 theorem mfderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : mfderivWithin I I' f s x = mfderiv I I' f x := by
@@ -551,7 +551,7 @@ theorem HasMFDerivWithinAt.congr_of_eventuallyEq (h : HasMFDerivWithinAt I I' f
   · have :
       (extChartAt I x).symm ⁻¹' {y | f₁ y = f y} ∈
         𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
-      extChartAt_preimage_mem_nhdsWithin I x h₁
+      extChartAt_preimage_mem_nhdsWithin I h₁
     apply Filter.mem_of_superset this fun y => _
     simp (config := { contextual := true }) only [hx, mfld_simps]
   · simp only [hx, mfld_simps]
@@ -667,7 +667,7 @@ theorem writtenInExtChartAt_comp (h : ContinuousWithinAt f s x) :
       𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x := by
   apply
     @Filter.mem_of_superset _ _ (f ∘ (extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) _
-      (extChartAt_preimage_mem_nhdsWithin I x
+      (extChartAt_preimage_mem_nhdsWithin I
         (h.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _ _)))
   mfld_set_tac
 #align written_in_ext_chart_comp writtenInExtChartAt_comp
@@ -685,7 +685,7 @@ theorem HasMFDerivWithinAt.comp (hg : HasMFDerivWithinAt I' I'' g u (f x) g')
     have :
       (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' (f x)).source) ∈
         𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
-      extChartAt_preimage_mem_nhdsWithin I x
+      extChartAt_preimage_mem_nhdsWithin I
         (hf.1.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _ _))
     unfold HasMFDerivWithinAt at *
     rw [← hasFDerivWithinAt_inter' this, ← extChartAt_preimage_inter_eq] at hf ⊢