chore: make the model with corners implicit in differential geometry …

…statements (#17687)

Currently, the model with corners `I` is explicit in many (most?) differential geometry statements. However, when rewriting, or applying theorems, it can be inferred from the context 95% of the time. Therefore, we make it implicit in most statements: the rule of thumb is that in `variable` lines we should have `{I : ModelWithCorners 𝕜 E H}`, and use `variable (I) in` for definitions. 

This looks like a clear improvement to me, making proofs more readable and avoiding clutter. For the few cases where we need to provide it explicitly, named arguments work well.

No mathematical change at all, just arguments implicitness.

Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

@@ -22,7 +22,7 @@ noncomputable instance : ChartedSpace ℂ ℍ :=
   UpperHalfPlane.isOpenEmbedding_coe.singletonChartedSpace
 
 instance : SmoothManifoldWithCorners 𝓘(ℂ) ℍ :=
-  UpperHalfPlane.isOpenEmbedding_coe.singleton_smoothManifoldWithCorners 𝓘(ℂ)
+  UpperHalfPlane.isOpenEmbedding_coe.singleton_smoothManifoldWithCorners
 
 /-- The inclusion map `ℍ → ℂ` is a smooth map of manifolds. -/
 theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) ((↑) : ℍ → ℂ) := fun _ => contMDiffAt_extChartAt

Mathlib/Geometry/Manifold/AnalyticManifold.lean

@@ -29,7 +29,7 @@ open scoped Manifold Filter Topology
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*}
-  [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M]
+  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M]
 
 /-!
 ## `analyticGroupoid`
@@ -41,6 +41,7 @@ analytic on the interior, and map the interior to itself.  This allows us to def
 
 section analyticGroupoid
 
+variable (I) in
 /-- Given a model with corners `(E, H)`, we define the pregroupoid of analytic transformations of
 `H` as the maps that are `AnalyticOn` when read in `E` through `I`.  Using `AnalyticOn`
 rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/
@@ -74,6 +75,7 @@ def analyticPregroupoid : Pregroupoid H where
     simp only [mfld_simps, ← hx] at hy1 ⊢
     rw [fg _ hy1]
 
+variable (I) in
 /-- Given a model with corners `(E, H)`, we define the groupoid of analytic transformations of
 `H` as the maps that are `AnalyticOn` when read in `E` through `I`.  Using `AnalyticOn`
 rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/
@@ -95,15 +97,15 @@ theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) :
     e.symm.trans e ∈ analyticGroupoid I :=
   haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
     PartialHomeomorph.symm_trans_self _
-  StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_analyticGroupoid I e.open_target) this
+  StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_analyticGroupoid e.open_target) this
 
 /-- The analytic groupoid is closed under restriction. -/
 instance : ClosedUnderRestriction (analyticGroupoid I) :=
   (closedUnderRestriction_iff_id_le _).mpr
     (by
       rw [StructureGroupoid.le_iff]
       rintro e ⟨s, hs, hes⟩
-      exact (analyticGroupoid I).mem_of_eqOnSource' _ _ (ofSet_mem_analyticGroupoid I hs) hes)
+      exact (analyticGroupoid I).mem_of_eqOnSource' _ _ (ofSet_mem_analyticGroupoid hs) hes)
 
 /-- `f ∈ analyticGroupoid` iff it and its inverse are analytic within `range I`. -/
 lemma mem_analyticGroupoid {I : ModelWithCorners 𝕜 E H} {f : PartialHomeomorph H H} :

Mathlib/Geometry/Manifold/BumpFunction.lean

@@ -95,7 +95,7 @@ theorem ball_inter_range_eq_ball_inter_target :
     ball (extChartAt I c c) f.rOut ∩ range I =
       ball (extChartAt I c c) f.rOut ∩ (extChartAt I c).target :=
   (subset_inter inter_subset_left f.ball_subset).antisymm <| inter_subset_inter_right _ <|
-    extChartAt_target_subset_range _ _
+    extChartAt_target_subset_range _
 
 section FiniteDimensional
 
@@ -120,7 +120,7 @@ theorem support_eq_inter_preimage :
 
 theorem isOpen_support : IsOpen (support f) := by
   rw [support_eq_inter_preimage]
-  exact isOpen_extChartAt_preimage I c isOpen_ball
+  exact isOpen_extChartAt_preimage c isOpen_ball
 
 theorem support_eq_symm_image :
     support f = (extChartAt I c).symm '' (ball (extChartAt I c c) f.rOut ∩ range I) := by
@@ -157,7 +157,7 @@ theorem le_one : f x ≤ 1 :=
 
 theorem eventuallyEq_one_of_dist_lt (hs : x ∈ (chartAt H c).source)
     (hd : dist (extChartAt I c x) (extChartAt I c c) < f.rIn) : f =ᶠ[𝓝 x] 1 := by
-  filter_upwards [IsOpen.mem_nhds (isOpen_extChartAt_preimage I c isOpen_ball) ⟨hs, hd⟩]
+  filter_upwards [IsOpen.mem_nhds (isOpen_extChartAt_preimage c isOpen_ball) ⟨hs, hd⟩]
   rintro z ⟨hzs, hzd⟩
   exact f.one_of_dist_le hzs <| le_of_lt hzd
 
@@ -183,7 +183,7 @@ theorem nonempty_support : (support f).Nonempty :=
 theorem isCompact_symm_image_closedBall :
     IsCompact ((extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I)) :=
   ((isCompact_closedBall _ _).inter_right I.isClosed_range).image_of_continuousOn <|
-    (continuousOn_extChartAt_symm _ _).mono f.closedBall_subset
+    (continuousOn_extChartAt_symm _).mono f.closedBall_subset
 
 end FiniteDimensional
 
@@ -194,7 +194,7 @@ theorem nhdsWithin_range_basis :
     (𝓝[range I] extChartAt I c c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
       closedBall (extChartAt I c c) f.rOut ∩ range I := by
   refine ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
-    (extChartAt_target_mem_nhdsWithin _ _)).to_hasBasis' ?_ ?_
+    (extChartAt_target_mem_nhdsWithin _)).to_hasBasis' ?_ ?_
   · rintro R ⟨hR0, hsub⟩
     exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩
   · exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos)
@@ -206,7 +206,7 @@ theorem isClosed_image_of_isClosed {s : Set M} (hsc : IsClosed s) (hs : s ⊆ su
     IsClosed (extChartAt I c '' s) := by
   rw [f.image_eq_inter_preimage_of_subset_support hs]
   refine ContinuousOn.preimage_isClosed_of_isClosed
-    ((continuousOn_extChartAt_symm _ _).mono f.closedBall_subset) ?_ hsc
+    ((continuousOn_extChartAt_symm _).mono f.closedBall_subset) ?_ hsc
   exact IsClosed.inter isClosed_ball I.isClosed_range
 
 /-- If `f` is a smooth bump function and `s` closed subset of the support of `f` (i.e., of the open
@@ -260,8 +260,6 @@ protected theorem hasCompactSupport : HasCompactSupport f :=
   f.isCompact_symm_image_closedBall.of_isClosed_subset isClosed_closure
     f.tsupport_subset_symm_image_closedBall
 
-variable (I)
-
 variable (c) in
 /-- The closures of supports of smooth bump functions centered at `c` form a basis of `𝓝 c`.
 In other words, each of these closures is a neighborhood of `c` and each neighborhood of `c`
@@ -271,7 +269,7 @@ theorem nhds_basis_tsupport :
   have :
     (𝓝 c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
       (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) := by
-    rw [← map_extChartAt_symm_nhdsWithin_range I c]
+    rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c]
     exact nhdsWithin_range_basis.map _
   exact this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩)
     fun f _ => f.tsupport_mem_nhds
@@ -282,10 +280,10 @@ neighborhood of `c` and each neighborhood of `c` includes `support f` for some
 `f : SmoothBumpFunction I c` such that `tsupport f ⊆ s`. -/
 theorem nhds_basis_support {s : Set M} (hs : s ∈ 𝓝 c) :
     (𝓝 c).HasBasis (fun f : SmoothBumpFunction I c => tsupport f ⊆ s) fun f => support f :=
-  ((nhds_basis_tsupport I c).restrict_subset hs).to_hasBasis'
+  ((nhds_basis_tsupport c).restrict_subset hs).to_hasBasis'
     (fun f hf => ⟨f, hf.2, subset_closure⟩) fun f _ => f.support_mem_nhds
 
-variable [SmoothManifoldWithCorners I M] {I}
+variable [SmoothManifoldWithCorners I M]
 
 /-- A smooth bump function is infinitely smooth. -/
 protected theorem smooth : Smooth I 𝓘(ℝ) f := by

Mathlib/Geometry/Manifold/Complex.lean

@@ -55,10 +55,10 @@ theorem Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax {f : M →
   have hI : range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
   have H₁ : 𝓝[range I] (e c) = 𝓝 (e c) := by rw [hI, nhdsWithin_univ]
   have H₂ : map e.symm (𝓝 (e c)) = 𝓝 c := by
-    rw [← map_extChartAt_symm_nhdsWithin_range I c, H₁]
+    rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
   rw [← H₂, eventually_map]
   replace hd : ∀ᶠ y in 𝓝 (e c), DifferentiableAt ℂ (f ∘ e.symm) y := by
-    have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin I c
+    have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
     filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
     have hys : e.symm y ∈ (chartAt H c).source := by
       rw [← extChartAt_source I c]
@@ -68,7 +68,7 @@ theorem Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax {f : M →
       e.right_inv hyt] at hy₂
     exact hy₂.2
   convert norm_eventually_eq_of_isLocalMax hd _
-  · exact congr_arg f (extChartAt_to_inv _ _).symm
+  · exact congr_arg f (extChartAt_to_inv _).symm
   · simpa only [e, IsLocalMax, IsMaxFilter, ← H₂, (· ∘ ·), extChartAt_to_inv] using hc
 
 /-!

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -35,7 +35,7 @@ section Atlas
 
 theorem contMDiff_model : ContMDiff I 𝓘(𝕜, E) n I := by
   intro x
-  refine (contMDiffAt_iff _ _).mpr ⟨I.continuousAt, ?_⟩
+  refine contMDiffAt_iff.mpr ⟨I.continuousAt, ?_⟩
   simp only [mfld_simps]
   refine contDiffWithinAt_id.congr_of_eventuallyEq ?_ ?_
   · exact Filter.eventuallyEq_of_mem self_mem_nhdsWithin fun x₂ => I.right_inv
@@ -50,16 +50,16 @@ theorem contMDiffOn_model_symm : ContMDiffOn 𝓘(𝕜, E) I n I.symm (range I)
 /-- An atlas member is `C^n` for any `n`. -/
 theorem contMDiffOn_of_mem_maximalAtlas (h : e ∈ maximalAtlas I M) : ContMDiffOn I I n e e.source :=
   ContMDiffOn.of_le
-    ((contDiffWithinAt_localInvariantProp I I ∞).liftPropOn_of_mem_maximalAtlas
-      (contDiffWithinAtProp_id I) h)
+    ((contDiffWithinAt_localInvariantProp ∞).liftPropOn_of_mem_maximalAtlas
+      contDiffWithinAtProp_id h)
     le_top
 
 /-- The inverse of an atlas member is `C^n` for any `n`. -/
 theorem contMDiffOn_symm_of_mem_maximalAtlas (h : e ∈ maximalAtlas I M) :
     ContMDiffOn I I n e.symm e.target :=
   ContMDiffOn.of_le
-    ((contDiffWithinAt_localInvariantProp I I ∞).liftPropOn_symm_of_mem_maximalAtlas
-      (contDiffWithinAtProp_id I) h)
+    ((contDiffWithinAt_localInvariantProp ∞).liftPropOn_symm_of_mem_maximalAtlas
+      contDiffWithinAtProp_id h)
     le_top
 
 theorem contMDiffAt_of_mem_maximalAtlas (h : e ∈ maximalAtlas I M) (hx : x ∈ e.source) :
@@ -71,18 +71,18 @@ theorem contMDiffAt_symm_of_mem_maximalAtlas {x : H} (h : e ∈ maximalAtlas I M
   (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 :=
-  contMDiffOn_of_mem_maximalAtlas <| chart_mem_maximalAtlas I x
+  contMDiffOn_of_mem_maximalAtlas <| chart_mem_maximalAtlas x
 
 theorem contMDiffOn_chart_symm : ContMDiffOn I I n (chartAt H x).symm (chartAt H x).target :=
-  contMDiffOn_symm_of_mem_maximalAtlas <| chart_mem_maximalAtlas I x
+  contMDiffOn_symm_of_mem_maximalAtlas <| chart_mem_maximalAtlas x
 
 theorem contMDiffAt_extend {x : M} (he : e ∈ maximalAtlas I M) (hx : x ∈ e.source) :
     ContMDiffAt I 𝓘(𝕜, E) n (e.extend I) x :=
   (contMDiff_model _).comp x <| contMDiffAt_of_mem_maximalAtlas he hx
 
 theorem contMDiffAt_extChartAt' {x' : M} (h : x' ∈ (chartAt H x).source) :
     ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x) x' :=
-  contMDiffAt_extend (chart_mem_maximalAtlas I x) h
+  contMDiffAt_extend (chart_mem_maximalAtlas x) h
 
 theorem contMDiffAt_extChartAt : ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x) x :=
   contMDiffAt_extChartAt' <| mem_chart_source H x
@@ -99,14 +99,13 @@ theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I M) :
 
 theorem contMDiffOn_extChartAt_symm (x : M) :
     ContMDiffOn 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target := by
-  convert contMDiffOn_extend_symm (chart_mem_maximalAtlas I x)
+  convert contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)
   rw [extChartAt_target, I.image_eq]
 
 /-- An element of `contDiffGroupoid ⊤ I` is `C^n` for any `n`. -/
 theorem contMDiffOn_of_mem_contDiffGroupoid {e' : PartialHomeomorph H H}
     (h : e' ∈ contDiffGroupoid ⊤ I) : ContMDiffOn I I n e' e'.source :=
-  (contDiffWithinAt_localInvariantProp I I n).liftPropOn_of_mem_groupoid
-    (contDiffWithinAtProp_id I) h
+  (contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_groupoid contDiffWithinAtProp_id h
 
 end Atlas
 

Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

@@ -28,11 +28,11 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   -- declare the prerequisites for a charted space `M` over the pair `(E, H)`.
   {E : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
-  (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M]
+  {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M]
   -- declare the prerequisites for a charted space `M'` over the pair `(E', H')`.
   {E' : Type*}
   [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
-  (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M']
+  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*} [TopologicalSpace M']
   -- declare the prerequisites for a charted space `M''` over the pair `(E'', H'')`.
   {E'' : Type*}
   [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H'']
@@ -43,7 +43,6 @@ variable [ChartedSpace H M] [ChartedSpace H' M'] [ChartedSpace H'' M'']
   -- declare functions, sets, points and smoothness indices
   {e : PartialHomeomorph M H}
   {e' : PartialHomeomorph M' H'} {f f₁ : M → M'} {s s₁ t : Set M} {x : M} {m n : ℕ∞}
-variable {I I'}
 
 /-! ### Smoothness of the composition of smooth functions between manifolds -/
 
@@ -61,8 +60,8 @@ theorem ContMDiffWithinAt.comp {t : Set M'} {g : M' → M''} (x : M)
   rw [this] at hg
   have A : ∀ᶠ y in 𝓝[e.symm ⁻¹' s ∩ range I] e x, f (e.symm y) ∈ t ∧ f (e.symm y) ∈ e'.source := by
     simp only [e, ← map_extChartAt_nhdsWithin, eventually_map]
-    filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds I' (f x)),
-      inter_mem_nhdsWithin s (extChartAt_source_mem_nhds I x)]
+    filter_upwards [hf.1.tendsto (extChartAt_source_mem_nhds (I := I') (f x)),
+      inter_mem_nhdsWithin s (extChartAt_source_mem_nhds (I := I) x)]
     rintro x' (hfx' : f x' ∈ e'.source) ⟨hx's, hx'⟩
     simp only [e.map_source hx', true_and, e.left_inv hx', st hx's, *]
   refine ((hg.2.comp _ (hf.2.mono inter_subset_right) inter_subset_left).mono_of_mem
@@ -184,7 +183,7 @@ section id
 
 theorem contMDiff_id : ContMDiff I I n (id : M → M) :=
   ContMDiff.of_le
-    ((contDiffWithinAt_localInvariantProp I I ∞).liftProp_id (contDiffWithinAtProp_id I)) le_top
+    ((contDiffWithinAt_localInvariantProp ∞).liftProp_id contDiffWithinAtProp_id) le_top
 
 theorem smooth_id : Smooth I I (id : M → M) :=
   contMDiff_id
@@ -310,7 +309,7 @@ open TopologicalSpace
 
 theorem contMdiffAt_subtype_iff {n : ℕ∞} {U : Opens M} {f : M → M'} {x : U} :
     ContMDiffAt I I' n (fun x : U ↦ f x) x ↔ ContMDiffAt I I' n f x :=
-  ((contDiffWithinAt_localInvariantProp I I' n).liftPropAt_iff_comp_subtype_val _ _).symm
+  ((contDiffWithinAt_localInvariantProp n).liftPropAt_iff_comp_subtype_val _ _).symm
 
 theorem contMDiff_subtype_val {n : ℕ∞} {U : Opens M} : ContMDiff I I n (Subtype.val : U → M) :=
   fun _ ↦ contMdiffAt_subtype_iff.mpr contMDiffAt_id
@@ -330,7 +329,7 @@ theorem ContMDiff.extend_one [T2Space M] [One M'] {n : ℕ∞} {U : Opens M} {f
 theorem contMDiff_inclusion {n : ℕ∞} {U V : Opens M} (h : U ≤ V) :
     ContMDiff I I n (Opens.inclusion h : U → V) := by
   rintro ⟨x, hx : x ∈ U⟩
-  apply (contDiffWithinAt_localInvariantProp I I n).liftProp_inclusion
+  apply (contDiffWithinAt_localInvariantProp n).liftProp_inclusion
   intro y
   dsimp only [ContDiffWithinAtProp, id_comp, preimage_univ]
   rw [Set.univ_inter]
@@ -364,7 +363,7 @@ variable {e : M → H} (h : IsOpenEmbedding e) {n : WithTop ℕ}
 then `e` is smooth. -/
 lemma contMDiff_isOpenEmbedding [Nonempty M] :
     haveI := h.singletonChartedSpace; ContMDiff I I n e := by
-  haveI := h.singleton_smoothManifoldWithCorners I
+  haveI := h.singleton_smoothManifoldWithCorners (I := I)
   rw [@contMDiff_iff _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace]
   use h.continuous
   intros x y
@@ -376,7 +375,7 @@ lemma contMDiff_isOpenEmbedding [Nonempty M] :
   rw [h.toPartialHomeomorph_right_inv]
   · rw [I.right_inv]
     apply mem_of_subset_of_mem _ hz.1
-    exact haveI := h.singletonChartedSpace; extChartAt_target_subset_range I x
+    exact haveI := h.singletonChartedSpace; extChartAt_target_subset_range (I := I) x
   · -- `hz` implies that `z ∈ range (I ∘ e)`
     have := hz.1
     rw [@extChartAt_target _ _ _ _ _ _ _ _ _ _ h.singletonChartedSpace] at this
@@ -388,13 +387,12 @@ lemma contMDiff_isOpenEmbedding [Nonempty M] :
 @[deprecated (since := "2024-10-18")]
 alias contMDiff_openEmbedding := contMDiff_isOpenEmbedding
 
-variable {I I'}
 /-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
 then the inverse of `e` is smooth. -/
 lemma contMDiffOn_isOpenEmbedding_symm [Nonempty M] :
     haveI := h.singletonChartedSpace; ContMDiffOn I I
       n (IsOpenEmbedding.toPartialHomeomorph e h).symm (range e) := by
-  haveI := h.singleton_smoothManifoldWithCorners I
+  haveI := h.singleton_smoothManifoldWithCorners (I := I)
   rw [@contMDiffOn_iff]
   constructor
   · rw [← h.toPartialHomeomorph_target]
@@ -410,7 +408,7 @@ lemma contMDiffOn_isOpenEmbedding_symm [Nonempty M] :
       exact hz.2.1
     rw [h.toPartialHomeomorph_right_inv e this]
     apply I.right_inv
-    exact mem_of_subset_of_mem (extChartAt_target_subset_range _ _) hz.1
+    exact mem_of_subset_of_mem (extChartAt_target_subset_range _) hz.1
 
 @[deprecated (since := "2024-10-18")]
 alias contMDiffOn_openEmbedding_symm := contMDiffOn_isOpenEmbedding_symm