diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean
index 45772d8d62ff6..aede75f666ab9 100644
--- a/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean
+++ b/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
diff --git a/Mathlib/Geometry/Manifold/AnalyticManifold.lean b/Mathlib/Geometry/Manifold/AnalyticManifold.lean
index 8ef606a4540a1..9a1ab30e1daa9 100644
--- a/Mathlib/Geometry/Manifold/AnalyticManifold.lean
+++ b/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,7 +97,7 @@ 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) :=
@@ -103,7 +105,7 @@ instance : ClosedUnderRestriction (analyticGroupoid I) :=
     (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} :
diff --git a/Mathlib/Geometry/Manifold/BumpFunction.lean b/Mathlib/Geometry/Manifold/BumpFunction.lean
index 16f7d52a36180..fa6698b53773a 100644
--- a/Mathlib/Geometry/Manifold/BumpFunction.lean
+++ b/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
diff --git a/Mathlib/Geometry/Manifold/Complex.lean b/Mathlib/Geometry/Manifold/Complex.lean
index a9ea94cdde69c..4d7fa4e80bc64 100644
--- a/Mathlib/Geometry/Manifold/Complex.lean
+++ b/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
 
 /-!
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
index 61057854d30c6..c4d0007f3c70a 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
+++ b/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,10 +71,10 @@ 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 :=
@@ -82,7 +82,7 @@ theorem contMDiffAt_extend {x : M} (he : e ∈ maximalAtlas I M) (hx : x ∈ e.s
 
 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
 
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean b/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
index b79ff42cc1ad9..a1064a541b84a 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
+++ b/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
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
index e52bf1aa65520..a9aa326b800c8 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
@@ -55,11 +55,11 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   -- Prerequisite typeclasses to say that `M` is a smooth manifold over the pair `(E, H)`
   {E : Type*}
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
-  (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+  {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
   -- Prerequisite typeclasses to say that `M'` is a smooth manifold over the pair `(E', H')`
   {E' : Type*}
   [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
-  (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
   -- Prerequisite typeclasses to say that `M''` is a smooth manifold over the pair `(E'', H'')`
   {E'' : Type*}
   [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H'']
@@ -68,6 +68,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {e : PartialHomeomorph M H}
   {e' : PartialHomeomorph M' H'} {f f₁ : M → M'} {s s₁ t : Set M} {x : M} {m n : ℕ∞}
 
+variable (I I') in
 /-- Property in the model space of a model with corners of being `C^n` within at set at a point,
 when read in the model vector space. This property will be lifted to manifolds to define smooth
 functions between manifolds. -/
@@ -81,7 +82,7 @@ theorem contDiffWithinAtProp_self_source {f : E → H'} {s : Set E} {x : E} :
 
 theorem contDiffWithinAtProp_self {f : E → E'} {s : Set E} {x : E} :
     ContDiffWithinAtProp 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x :=
-  contDiffWithinAtProp_self_source 𝓘(𝕜, E')
+  contDiffWithinAtProp_self_source
 
 theorem contDiffWithinAtProp_self_target {f : H → E'} {s : Set H} {x : H} :
     ContDiffWithinAtProp I 𝓘(𝕜, E') n f s x ↔
@@ -143,17 +144,20 @@ theorem contDiffWithinAtProp_id (x : H) : ContDiffWithinAtProp I I n id univ x :
   · simp only [ModelWithCorners.right_inv I hy, mfld_simps]
   · simp only [mfld_simps]
 
+variable (I I') in
 /-- A function is `n` times continuously differentiable within a set at a point in a manifold if
 it is continuous and it is `n` times continuously differentiable in this set around this point, when
 read in the preferred chart at this point. -/
 def ContMDiffWithinAt (n : ℕ∞) (f : M → M') (s : Set M) (x : M) :=
   LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
 
+variable (I I') in
 /-- Abbreviation for `ContMDiffWithinAt I I' ⊤ f s x`. See also documentation for `Smooth`.
 -/
 abbrev SmoothWithinAt (f : M → M') (s : Set M) (x : M) :=
   ContMDiffWithinAt I I' ⊤ f s x
 
+variable (I I') in
 /-- A function is `n` times continuously differentiable at a point in a manifold if
 it is continuous and it is `n` times continuously differentiable around this point, when
 read in the preferred chart at this point. -/
@@ -167,26 +171,31 @@ theorem contMDiffAt_iff {n : ℕ∞} {f : M → M'} {x : M} :
           (extChartAt I x x) :=
   liftPropAt_iff.trans <| by rw [ContDiffWithinAtProp, preimage_univ, univ_inter]; rfl
 
+variable (I I') in
 /-- Abbreviation for `ContMDiffAt I I' ⊤ f x`. See also documentation for `Smooth`. -/
 abbrev SmoothAt (f : M → M') (x : M) :=
   ContMDiffAt I I' ⊤ f x
 
+variable (I I') in
 /-- A function is `n` times continuously differentiable in a set of a manifold if it is continuous
 and, for any pair of points, it is `n` times continuously differentiable on this set in the charts
 around these points. -/
 def ContMDiffOn (n : ℕ∞) (f : M → M') (s : Set M) :=
   ∀ x ∈ s, ContMDiffWithinAt I I' n f s x
 
+variable (I I') in
 /-- Abbreviation for `ContMDiffOn I I' ⊤ f s`. See also documentation for `Smooth`. -/
 abbrev SmoothOn (f : M → M') (s : Set M) :=
   ContMDiffOn I I' ⊤ f s
 
+variable (I I') in
 /-- A function is `n` times continuously differentiable in a manifold if it is continuous
 and, for any pair of points, it is `n` times continuously differentiable in the charts
 around these points. -/
 def ContMDiff (n : ℕ∞) (f : M → M') :=
   ∀ x, ContMDiffAt I I' n f x
 
+variable (I I') in
 /-- Abbreviation for `ContMDiff I I' ⊤ f`.
 Short note to work with these abbreviations: a lemma of the form `ContMDiffFoo.bar` will
 apply fine to an assumption `SmoothFoo` using dot notation or normal notation.
@@ -197,8 +206,6 @@ This also applies to `SmoothAt`, `SmoothOn` and `SmoothWithinAt`. -/
 abbrev Smooth (f : M → M') :=
   ContMDiff I I' ⊤ f
 
-variable {I I'}
-
 /-! ### Deducing smoothness from higher smoothness -/
 
 theorem ContMDiffWithinAt.of_le (hf : ContMDiffWithinAt I I' n f s x) (le : m ≤ n) :
@@ -287,7 +294,7 @@ theorem contMDiffWithinAt_iff' :
           (extChartAt I x x) := by
   simp only [ContMDiffWithinAt, liftPropWithinAt_iff']
   exact and_congr_right fun hc => contDiffWithinAt_congr_nhds <|
-    hc.nhdsWithin_extChartAt_symm_preimage_inter_range I I'
+    hc.nhdsWithin_extChartAt_symm_preimage_inter_range
 
 /-- One can reformulate smoothness within a set at a point as continuity within this set at this
 point, and smoothness in the corresponding extended chart in the target. -/
@@ -298,7 +305,7 @@ theorem contMDiffWithinAt_iff_target :
   have cont :
     ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔
         ContinuousWithinAt f s x :=
-      and_iff_left_of_imp <| (continuousAt_extChartAt _ _).comp_continuousWithinAt
+      and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt
   simp_rw [cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
     ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
     chartAt_self_eq, PartialHomeomorph.refl_apply, id_comp]
@@ -332,9 +339,9 @@ theorem contMDiffWithinAt_iff_source_of_mem_maximalAtlas
     ContMDiffWithinAt I I' n f s x ↔
       ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I)
         (e.extend I x) := by
-  have h2x := hx; rw [← e.extend_source I] at h2x
+  have h2x := hx; rw [← e.extend_source (I := I)] at h2x
   simp_rw [ContMDiffWithinAt,
-    (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_indep_chart_source he hx,
+    (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart_source he hx,
     StructureGroupoid.liftPropWithinAt_self_source,
     e.extend_symm_continuousWithinAt_comp_right_iff, contDiffWithinAtProp_self_source,
     ContDiffWithinAtProp, Function.comp, e.left_inv hx, (e.extend I).left_inv h2x]
@@ -345,7 +352,7 @@ theorem contMDiffWithinAt_iff_source_of_mem_source
     ContMDiffWithinAt I I' n f s x' ↔
       ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (extChartAt I x).symm)
         ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x') :=
-  contMDiffWithinAt_iff_source_of_mem_maximalAtlas (chart_mem_maximalAtlas I x) hx'
+  contMDiffWithinAt_iff_source_of_mem_maximalAtlas (chart_mem_maximalAtlas x) hx'
 
 theorem contMDiffAt_iff_source_of_mem_source
     [SmoothManifoldWithCorners I M] {x' : M} (hx' : x' ∈ (chartAt H x).source) :
@@ -358,14 +365,14 @@ theorem contMDiffWithinAt_iff_target_of_mem_source
     ContMDiffWithinAt I I' n f s x ↔
       ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) s x := by
   simp_rw [ContMDiffWithinAt]
-  rw [(contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_indep_chart_target
-      (chart_mem_maximalAtlas I' y) hy,
+  rw [(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart_target
+      (chart_mem_maximalAtlas y) hy,
     and_congr_right]
   intro hf
   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]
+  rw [← extChartAt_source (I := I')] at hy
+  simp_rw [(continuousAt_extChartAt' hy).comp_continuousWithinAt hf]
   rfl
 
 theorem contMDiffAt_iff_target_of_mem_source
@@ -383,7 +390,7 @@ theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtl
       ContinuousWithinAt f s x ∧
         ContDiffWithinAt 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm)
           ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x) :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_indep_chart he hx he' hy
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart he hx he' hy
 
 /-- An alternative formulation of `contMDiffWithinAt_iff_of_mem_maximalAtlas`
   if the set if `s` lies in `e.source`. -/
@@ -395,7 +402,7 @@ theorem contMDiffWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I M)
           (e.extend I x) := by
   rw [contMDiffWithinAt_iff_of_mem_maximalAtlas he he' hx hy, and_congr_right_iff]
   refine fun _ => contDiffWithinAt_congr_nhds ?_
-  simp_rw [nhdsWithin_eq_iff_eventuallyEq, e.extend_symm_preimage_inter_range_eventuallyEq I hs hx]
+  simp_rw [nhdsWithin_eq_iff_eventuallyEq, e.extend_symm_preimage_inter_range_eventuallyEq hs hx]
 
 /-- One can reformulate smoothness within a set at a point as continuity within this set at this
 point, and smoothness in any chart containing that point. -/
@@ -405,8 +412,8 @@ theorem contMDiffWithinAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (char
       ContinuousWithinAt f s x' ∧
         ContDiffWithinAt 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
           ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x') :=
-  contMDiffWithinAt_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas _ x)
-    (chart_mem_maximalAtlas _ y) hx hy
+  contMDiffWithinAt_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x)
+    (chart_mem_maximalAtlas y) hx hy
 
 theorem contMDiffWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
     (hy : f x' ∈ (chartAt H' y).source) :
@@ -421,9 +428,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 hx, ←
-    map_extChartAt_nhdsWithin' I 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' hx,
+    ← map_extChartAt_nhdsWithin' hx, inter_comm, nhdsWithin_inter_of_mem]
+  exact hc (extChartAt_source_mem_nhds' hy)
 
 theorem contMDiffAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
     (hy : f x' ∈ (chartAt H' y).source) :
@@ -447,7 +454,7 @@ theorem contMDiffOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I M)
     ContMDiffOn I I' n f s ↔
       ContDiffOn 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s) :=
   (contMDiffOn_iff_of_mem_maximalAtlas he he' hs h2s).trans <| and_iff_right_of_imp fun h ↦
-    (e.continuousOn_writtenInExtend_iff _ _ hs h2s).1 h.continuousOn
+    (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn
 
 /-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
   into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
@@ -459,7 +466,7 @@ theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H
     ContMDiffOn I I' n f s ↔
       ContinuousOn f s ∧
         ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) :=
-  contMDiffOn_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas I x) (chart_mem_maximalAtlas I' y) hs
+  contMDiffOn_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hs
     h2s
 
 /-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
@@ -472,8 +479,8 @@ theorem contMDiffOn_iff_of_subset_source' {x : M} {y : M'} (hs : s ⊆ (extChart
     ContMDiffOn I I' n f s ↔
         ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) := by
   rw [extChartAt_source] at hs h2s
-  exact contMDiffOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas I x)
-    (chart_mem_maximalAtlas I' y) hs h2s
+  exact contMDiffOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
+    (chart_mem_maximalAtlas y) hs h2s
 
 /-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
 extended chart. -/
@@ -497,7 +504,7 @@ theorem contMDiffOn_iff :
     · simp only [w, hz, mfld_simps]
     · mfld_set_tac
   · rintro ⟨hcont, hdiff⟩ x hx
-    refine (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_iff.mpr ?_
+    refine (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_iff.mpr ?_
     refine ⟨hcont x hx, ?_⟩
     dsimp [ContDiffWithinAtProp]
     convert hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1
@@ -632,7 +639,7 @@ theorem contMDiffWithinAt_iff_nat :
 theorem ContMDiffWithinAt.mono_of_mem (hf : ContMDiffWithinAt I I' n f s x) (hts : s ∈ 𝓝[t] x) :
     ContMDiffWithinAt I I' n f t x :=
   StructureGroupoid.LocalInvariantProp.liftPropWithinAt_mono_of_mem
-    (contDiffWithinAtProp_mono_of_mem I I' n) hf hts
+    (contDiffWithinAtProp_mono_of_mem n) hf hts
 
 theorem ContMDiffWithinAt.mono (hf : ContMDiffWithinAt I I' n f s x) (hts : t ⊆ s) :
     ContMDiffWithinAt I I' n f t x :=
@@ -647,7 +654,7 @@ theorem contMDiffWithinAt_insert_self :
     ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x := by
   simp only [contMDiffWithinAt_iff, continuousWithinAt_insert_self]
   refine Iff.rfl.and <| (contDiffWithinAt_congr_nhds ?_).trans contDiffWithinAt_insert_self
-  simp only [← map_extChartAt_nhdsWithin I, nhdsWithin_insert, Filter.map_sup, Filter.map_pure]
+  simp only [← map_extChartAt_nhdsWithin, nhdsWithin_insert, Filter.map_sup, Filter.map_pure]
 
 alias ⟨ContMDiffWithinAt.of_insert, _⟩ := contMDiffWithinAt_insert_self
 
@@ -674,15 +681,15 @@ theorem Smooth.smoothOn (hf : Smooth I I' f) : SmoothOn I I' f s :=
 
 theorem contMDiffWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
     ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_inter' ht
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_inter' ht
 
 theorem contMDiffWithinAt_inter (ht : t ∈ 𝓝 x) :
     ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_inter ht
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_inter ht
 
 theorem ContMDiffWithinAt.contMDiffAt (h : ContMDiffWithinAt I I' n f s x) (ht : s ∈ 𝓝 x) :
     ContMDiffAt I I' n f x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropAt_of_liftPropWithinAt h ht
+  (contDiffWithinAt_localInvariantProp n).liftPropAt_of_liftPropWithinAt h ht
 
 theorem SmoothWithinAt.smoothAt (h : SmoothWithinAt I I' f s x) (ht : s ∈ 𝓝 x) :
     SmoothAt I I' f x :=
@@ -704,7 +711,7 @@ theorem contMDiffOn_iff_source_of_mem_maximalAtlas [SmoothManifoldWithCorners I
   rw [contMDiffWithinAt_iff_source_of_mem_maximalAtlas he (hs hx)]
   apply contMDiffWithinAt_congr_nhds
   simp_rw [nhdsWithin_eq_iff_eventuallyEq,
-    e.extend_symm_preimage_inter_range_eventuallyEq I hs (hs hx)]
+    e.extend_symm_preimage_inter_range_eventuallyEq hs (hs hx)]
 
 -- Porting note: didn't compile; fixed by golfing the proof and moving parts to lemmas
 /-- A function is `C^n` within a set at a point, for `n : ℕ`, if and only if it is `C^n` on
@@ -723,13 +730,13 @@ theorem contMDiffWithinAt_iff_contMDiffOn_nhds
   rcases (contMDiffWithinAt_iff'.1 h).2.contDiffOn le_rfl with ⟨v, hmem, hsub, hv⟩
   have hxs' : extChartAt I x x ∈ (extChartAt I x).target ∩
       (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) :=
-    ⟨(extChartAt I x).map_source (mem_extChartAt_source _ _), by rwa [extChartAt_to_inv], by
+    ⟨(extChartAt I x).map_source (mem_extChartAt_source _), by rwa [extChartAt_to_inv], by
       rw [extChartAt_to_inv]; apply mem_extChartAt_source⟩
   rw [insert_eq_of_mem hxs'] at hmem hsub
   -- Then `(extChartAt I x).symm '' v` is the neighborhood we are looking for.
   refine ⟨(extChartAt I x).symm '' v, ?_, ?_⟩
-  · rw [← map_extChartAt_symm_nhdsWithin I,
-      h.1.nhdsWithin_extChartAt_symm_preimage_inter_range I I']
+  · rw [← map_extChartAt_symm_nhdsWithin (I := I),
+      h.1.nhdsWithin_extChartAt_symm_preimage_inter_range (I := I) (I' := I')]
     exact image_mem_map hmem
   · have hv₁ : (extChartAt I x).symm '' v ⊆ (extChartAt I x).source :=
       image_subset_iff.2 fun y hy ↦ (extChartAt I x).map_target (hsub hy).1
@@ -761,35 +768,35 @@ theorem contMDiffAt_iff_contMDiffAt_nhds
 
 theorem ContMDiffWithinAt.congr (h : ContMDiffWithinAt I I' n f s x) (h₁ : ∀ y ∈ s, f₁ y = f y)
     (hx : f₁ x = f x) : ContMDiffWithinAt I I' n f₁ s x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_congr h h₁ hx
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr h h₁ hx
 
 theorem contMDiffWithinAt_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
     ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_congr_iff h₁ hx
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff h₁ hx
 
 theorem ContMDiffWithinAt.congr_of_eventuallyEq (h : ContMDiffWithinAt I I' n f s x)
     (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : ContMDiffWithinAt I I' n f₁ s x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_congr_of_eventuallyEq h h₁ hx
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_of_eventuallyEq h h₁ hx
 
 theorem Filter.EventuallyEq.contMDiffWithinAt_iff (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
     ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropWithinAt_congr_iff_of_eventuallyEq h₁ hx
+  (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_congr_iff_of_eventuallyEq h₁ hx
 
 theorem ContMDiffAt.congr_of_eventuallyEq (h : ContMDiffAt I I' n f x) (h₁ : f₁ =ᶠ[𝓝 x] f) :
     ContMDiffAt I I' n f₁ x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropAt_congr_of_eventuallyEq h h₁
+  (contDiffWithinAt_localInvariantProp n).liftPropAt_congr_of_eventuallyEq h h₁
 
 theorem Filter.EventuallyEq.contMDiffAt_iff (h₁ : f₁ =ᶠ[𝓝 x] f) :
     ContMDiffAt I I' n f₁ x ↔ ContMDiffAt I I' n f x :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropAt_congr_iff_of_eventuallyEq h₁
+  (contDiffWithinAt_localInvariantProp n).liftPropAt_congr_iff_of_eventuallyEq h₁
 
 theorem ContMDiffOn.congr (h : ContMDiffOn I I' n f s) (h₁ : ∀ y ∈ s, f₁ y = f y) :
     ContMDiffOn I I' n f₁ s :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropOn_congr h h₁
+  (contDiffWithinAt_localInvariantProp n).liftPropOn_congr h h₁
 
 theorem contMDiffOn_congr (h₁ : ∀ y ∈ s, f₁ y = f y) :
     ContMDiffOn I I' n f₁ s ↔ ContMDiffOn I I' n f s :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropOn_congr_iff h₁
+  (contDiffWithinAt_localInvariantProp n).liftPropOn_congr_iff h₁
 
 theorem ContMDiffOn.congr_mono (hf : ContMDiffOn I I' n f s) (h₁ : ∀ y ∈ s₁, f₁ y = f y)
     (hs : s₁ ⊆ s) : ContMDiffOn I I' n f₁ s₁ :=
@@ -801,8 +808,8 @@ theorem ContMDiffOn.congr_mono (hf : ContMDiffOn I I' n f s) (h₁ : ∀ y ∈ s
 /-- Being `C^n` is a local property. -/
 theorem contMDiffOn_of_locally_contMDiffOn
     (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u)) : ContMDiffOn I I' n f s :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftPropOn_of_locally_liftPropOn h
+  (contDiffWithinAt_localInvariantProp n).liftPropOn_of_locally_liftPropOn h
 
 theorem contMDiff_of_locally_contMDiffOn (h : ∀ x, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f u) :
     ContMDiff I I' n f :=
-  (contDiffWithinAt_localInvariantProp I I' n).liftProp_of_locally_liftPropOn h
+  (contDiffWithinAt_localInvariantProp n).liftProp_of_locally_liftPropOn h
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Product.lean b/Mathlib/Geometry/Manifold/ContMDiff/Product.lean
index 5c76e05789139..fcd0a708a6a66 100644
--- a/Mathlib/Geometry/Manifold/ContMDiff/Product.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiff/Product.lean
@@ -23,11 +23,11 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   -- declare 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] [ChartedSpace H M]
+  {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
   -- declare 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'] [ChartedSpace H' M']
+  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
   -- declare a charted space `N` over the pair `(F, G)`.
   {F : Type*}
   [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
@@ -38,7 +38,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {J' : ModelWithCorners 𝕜 F' G'} {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N']
   -- declare functions, sets, points and smoothness indices
   {f : M → M'} {s : Set M} {x : M} {n : ℕ∞}
-variable {I I'}
 
 section ProdMk
 
@@ -129,7 +128,7 @@ theorem contMDiffWithinAt_fst {s : Set (M × N)} {p : M × N} :
   rw [contMDiffWithinAt_iff']
   refine ⟨continuousWithinAt_fst, contDiffWithinAt_fst.congr (fun y hy => ?_) ?_⟩
   · exact (extChartAt I p.1).right_inv ⟨hy.1.1.1, hy.1.2.1⟩
-  · exact (extChartAt I p.1).right_inv <| (extChartAt I p.1).map_source (mem_extChartAt_source _ _)
+  · exact (extChartAt I p.1).right_inv <| (extChartAt I p.1).map_source (mem_extChartAt_source _)
 
 theorem ContMDiffWithinAt.fst {f : N → M × M'} {s : Set N} {x : N}
     (hf : ContMDiffWithinAt J (I.prod I') n f s x) :
@@ -185,7 +184,7 @@ theorem contMDiffWithinAt_snd {s : Set (M × N)} {p : M × N} :
   rw [contMDiffWithinAt_iff']
   refine ⟨continuousWithinAt_snd, contDiffWithinAt_snd.congr (fun y hy => ?_) ?_⟩
   · exact (extChartAt J p.2).right_inv ⟨hy.1.1.2, hy.1.2.2⟩
-  · exact (extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _ _)
+  · exact (extChartAt J p.2).right_inv <| (extChartAt J p.2).map_source (mem_extChartAt_source _)
 
 theorem ContMDiffWithinAt.snd {f : N → M × M'} {s : Set N} {x : N}
     (hf : ContMDiffWithinAt J (I.prod I') n f s x) :
diff --git a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
index efcc63b456d66..0f305e578a8e3 100644
--- a/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
@@ -76,12 +76,12 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N →
       x₀ := by
   have h4f : ContinuousAt (fun x => f x (g x)) x₀ :=
     ContinuousAt.comp_of_eq hf.continuousAt (continuousAt_id.prod hg.continuousAt) rfl
-  have h4f := h4f.preimage_mem_nhds (extChartAt_source_mem_nhds I' (f x₀ (g x₀)))
+  have h4f := h4f.preimage_mem_nhds (extChartAt_source_mem_nhds (I := I') (f x₀ (g x₀)))
   have h3f := contMDiffAt_iff_contMDiffAt_nhds.mp (hf.of_le <| (self_le_add_left 1 m).trans hmn)
   have h2f : ∀ᶠ x₂ in 𝓝 x₀, ContMDiffAt I I' 1 (f x₂) (g x₂) := by
     refine ((continuousAt_id.prod hg.continuousAt).tendsto.eventually h3f).mono fun x hx => ?_
     exact hx.comp (g x) (contMDiffAt_const.prod_mk contMDiffAt_id)
-  have h2g := hg.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds I (g x₀))
+  have h2g := hg.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds (I := I) (g x₀))
   have :
     ContDiffWithinAt 𝕜 m
       (fun x =>
@@ -130,9 +130,9 @@ 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 h2x₂.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds _ _)
+    · exact extChartAt_preimage_mem_nhds' hx₂ (extChartAt_source_mem_nhds (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` -/
   -- Porting note: added
@@ -153,19 +153,19 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N →
     intro x₂ hx₂ h2x₂ h3x₂
     symm
     rw [(h2x₂.mdifferentiableAt le_rfl).mfderiv]
-    have hI := (contDiffWithinAt_ext_coord_change I (g x₂) (g x₀) <|
+    have hI := (contDiffWithinAt_ext_coord_change (I := I) (g x₂) (g x₀) <|
       PartialEquiv.mem_symm_trans_source _ hx₂ <|
-        mem_extChartAt_source I (g x₂)).differentiableWithinAt le_top
+        mem_extChartAt_source (g x₂)).differentiableWithinAt le_top
     have hI' :=
-      (contDiffWithinAt_ext_coord_change I' (f x₀ (g x₀)) (f x₂ (g x₂)) <|
-            PartialEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂)))
+      (contDiffWithinAt_ext_coord_change (f x₀ (g x₀)) (f x₂ (g x₂)) <|
+            PartialEquiv.mem_symm_trans_source _ (mem_extChartAt_source (f x₂ (g x₂)))
               h3x₂).differentiableWithinAt le_top
     have h3f := (h2x₂.mdifferentiableAt le_rfl).differentiableWithinAt_writtenInExtChartAt
     refine fderivWithin.comp₃ _ hI' h3f hI ?_ ?_ ?_ ?_ (I.uniqueDiffOn _ <| mem_range_self _)
     · exact fun x _ => mem_range_self _
     · exact fun x _ => mem_range_self _
     · simp_rw [writtenInExtChartAt, Function.comp_apply,
-        (extChartAt I (g x₂)).left_inv (mem_extChartAt_source I (g x₂))]
+        (extChartAt I (g x₂)).left_inv (mem_extChartAt_source (g x₂))]
     · simp_rw [Function.comp_apply, (extChartAt I (g x₀)).left_inv hx₂]
   refine this.congr_of_eventuallyEq ?_
   filter_upwards [h2g, h4f] with x hx h2x
@@ -223,12 +223,12 @@ theorem ContMDiffOn.continuousOn_tangentMapWithin_aux {f : H → H'} {s : Set H}
         (f p.fst,
           (fderivWithin 𝕜 (writtenInExtChartAt I I' p.fst f) (I.symm ⁻¹' s ∩ range I)
                 ((extChartAt I p.fst) p.fst) : E →L[𝕜] E') p.snd)) (Prod.fst ⁻¹' s) by
-    have A := (tangentBundleModelSpaceHomeomorph H I).continuous
+    have A := (tangentBundleModelSpaceHomeomorph I).continuous
     rw [continuous_iff_continuousOn_univ] at A
     have B :=
-      ((tangentBundleModelSpaceHomeomorph H' I').symm.continuous.comp_continuousOn h).comp' A
+      ((tangentBundleModelSpaceHomeomorph I').symm.continuous.comp_continuousOn h).comp' A
     have :
-      univ ∩ tangentBundleModelSpaceHomeomorph H I ⁻¹' (Prod.fst ⁻¹' s) =
+      univ ∩ tangentBundleModelSpaceHomeomorph I ⁻¹' (Prod.fst ⁻¹' s) =
         π E (TangentSpace I) ⁻¹' s := by
       ext ⟨x, v⟩; simp only [mfld_simps]
     rw [this] at B
@@ -390,7 +390,7 @@ theorem ContMDiffOn.contMDiffOn_tangentMapWithin
     apply UniqueMDiffOn.inter _ l.open_source
     rw [ho, inter_comm]
     exact hs.inter o_open
-  have U'l : UniqueMDiffOn I s'l := U'.uniqueMDiffOn_preimage (mdifferentiable_chart _ _)
+  have U'l : UniqueMDiffOn I s'l := U'.uniqueMDiffOn_preimage (mdifferentiable_chart _)
   have diff_f : ContMDiffOn I I' n f s' := hf.mono (by unfold_let s'; mfld_set_tac)
   have diff_r : ContMDiffOn I' I' n r r.source := contMDiffOn_chart
   have diff_rf : ContMDiffOn I I' n (r ∘ f) s' := by
@@ -461,7 +461,7 @@ theorem ContMDiffOn.contMDiffOn_tangentMapWithin
           tangentMap I I l.symm (il.symm (Dl q)) := by
         refine tangentMapWithin_eq_tangentMap U'lq ?_
         -- Porting note: the arguments below were underscores.
-        refine mdifferentiableAt_atlas_symm I (chart_mem_atlas H (TotalSpace.proj p)) ?_
+        refine mdifferentiableAt_atlas_symm (chart_mem_atlas H (TotalSpace.proj p)) ?_
         simp only [Dl, il, hq, mfld_simps]
       rw [this, tangentMap_chart_symm, hDl]
       · simp only [il, hq, mfld_simps]
@@ -487,7 +487,7 @@ theorem ContMDiffOn.contMDiffOn_tangentMapWithin
         apply tangentMapWithin_eq_tangentMap
         · apply r.open_source.uniqueMDiffWithinAt _
           simp [hq]
-        · exact mdifferentiableAt_atlas I' (chart_mem_atlas H' (f p.proj)) hq.1.1
+        · exact mdifferentiableAt_atlas (chart_mem_atlas H' (f p.proj)) hq.1.1
       have : f p.proj = (tangentMapWithin I I' f s p).1 := rfl
       rw [A]
       dsimp [Dr, ir, s', r, l]
@@ -538,8 +538,6 @@ end tangentMap
 
 namespace TangentBundle
 
-variable (I M)
-
 open Bundle
 
 /-- The derivative of the zero section of the tangent bundle maps `⟨x, v⟩` to `⟨⟨x, 0⟩, ⟨v, 0⟩⟩`.
diff --git a/Mathlib/Geometry/Manifold/ContMDiffMap.lean b/Mathlib/Geometry/Manifold/ContMDiffMap.lean
index 9eac199f01e6d..8566926007fa4 100644
--- a/Mathlib/Geometry/Manifold/ContMDiffMap.lean
+++ b/Mathlib/Geometry/Manifold/ContMDiffMap.lean
@@ -14,8 +14,8 @@ bundled maps.
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type*}
-  [TopologicalSpace H] {H' : Type*} [TopologicalSpace H'] (I : ModelWithCorners 𝕜 E H)
-  (I' : ModelWithCorners 𝕜 E' H') (M : Type*) [TopologicalSpace M] [ChartedSpace H M] (M' : Type*)
+  [TopologicalSpace H] {H' : Type*} [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
+  {I' : ModelWithCorners 𝕜 E' H'} (M : Type*) [TopologicalSpace M] [ChartedSpace H M] (M' : Type*)
   [TopologicalSpace M'] [ChartedSpace H' M'] {E'' : Type*} [NormedAddCommGroup E'']
   [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''}
   {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M'']
@@ -24,10 +24,12 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom
   [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
   {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞)
 
+variable (I I') in
 /-- Bundled `n` times continuously differentiable maps. -/
 def ContMDiffMap :=
   { f : M → M' // ContMDiff I I' n f }
 
+variable (I I') in
 /-- Bundled smooth maps. -/
 abbrev SmoothMap :=
   ContMDiffMap I I' M M' ⊤
@@ -43,7 +45,7 @@ open scoped Manifold
 
 namespace ContMDiffMap
 
-variable {I} {I'} {M} {M'} {n}
+variable {M} {M'} {n}
 
 instance instFunLike : FunLike C^n⟮I, M; I', M'⟯ M M' where
   coe := Subtype.val
diff --git a/Mathlib/Geometry/Manifold/Diffeomorph.lean b/Mathlib/Geometry/Manifold/Diffeomorph.lean
index fa71b1fc3e365..88e23753a1297 100644
--- a/Mathlib/Geometry/Manifold/Diffeomorph.lean
+++ b/Mathlib/Geometry/Manifold/Diffeomorph.lean
@@ -497,14 +497,14 @@ def toTransDiffeomorph (e : E ≃ₘ[𝕜] F) : M ≃ₘ⟮I, I.transDiffeomorph
     · simp only [Equiv.coe_refl, id, (· ∘ ·), I.coe_extChartAt_transDiffeomorph,
         (extChartAt I x).right_inv hy.1]
     · exact
-      ⟨(extChartAt I x).map_source (mem_extChartAt_source I x), trivial, by simp only [mfld_simps]⟩
+      ⟨(extChartAt I x).map_source (mem_extChartAt_source x), trivial, by simp only [mfld_simps]⟩
   contMDiff_invFun x := by
     refine contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩
     refine e.symm.contDiff.contDiffWithinAt.congr' (fun y hy => ?_) ?_
     · simp only [mem_inter_iff, I.extChartAt_transDiffeomorph_target] at hy
       simp only [Equiv.coe_refl, Equiv.refl_symm, id, (· ∘ ·),
         I.coe_extChartAt_transDiffeomorph_symm, (extChartAt I x).right_inv hy.1]
-    exact ⟨(extChartAt _ x).map_source (mem_extChartAt_source _ x), trivial, by
+    exact ⟨(extChartAt _ x).map_source (mem_extChartAt_source x), trivial, by
       simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]⟩
 
 variable {I M}
diff --git a/Mathlib/Geometry/Manifold/Instances/Real.lean b/Mathlib/Geometry/Manifold/Instances/Real.lean
index f3df629fd809b..9b54f975c0526 100644
--- a/Mathlib/Geometry/Manifold/Instances/Real.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Real.lean
@@ -323,7 +323,7 @@ instance Icc_smooth_manifold (x y : ℝ) [Fact (x < y)] :
   either the left chart or the right chart, leaving 4 possibilities that we handle successively. -/
   rcases he with (rfl | rfl) <;> rcases he' with (rfl | rfl)
   · -- `e = left chart`, `e' = left chart`
-    exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _ _ _)).1
+    exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1
   · -- `e = left chart`, `e' = right chart`
     apply M.contDiffOn.congr
     rintro _ ⟨⟨hz₁, hz₂⟩, ⟨⟨z, hz₀⟩, rfl⟩⟩
@@ -347,7 +347,7 @@ instance Icc_smooth_manifold (x y : ℝ) [Fact (x < y)] :
       PiLp.neg_apply, update_same, max_eq_left, hz₀, hz₁.le, mfld_simps]
     abel
   ·-- `e = right chart`, `e' = right chart`
-    exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _ _ _)).1
+    exact (mem_groupoid_of_pregroupoid.mpr (symm_trans_mem_contDiffGroupoid _)).1
 
 /-! Register the manifold structure on `Icc 0 1`, and also its zero and one. -/
 
diff --git a/Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean b/Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
index afe2f7f2112cb..8ee99e793fb7c 100644
--- a/Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
+++ b/Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean
@@ -44,12 +44,12 @@ theorem chartAt_source {a : Rˣ} : (chartAt R a).source = Set.univ :=
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedAlgebra 𝕜 R]
 
 instance : SmoothManifoldWithCorners 𝓘(𝕜, R) Rˣ :=
-  isOpenEmbedding_val.singleton_smoothManifoldWithCorners 𝓘(𝕜, R)
+  isOpenEmbedding_val.singleton_smoothManifoldWithCorners
 
 /-- For a complete normed ring `R`, the embedding of the units `Rˣ` into `R` is a smooth map between
 manifolds. -/
 lemma contMDiff_val {m : ℕ∞} : ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) m (val : Rˣ → R) :=
-  contMDiff_isOpenEmbedding 𝓘(𝕜, R) Units.isOpenEmbedding_val
+  contMDiff_isOpenEmbedding Units.isOpenEmbedding_val
 
 /-- The units of a complete normed ring form a Lie group. -/
 instance : LieGroup 𝓘(𝕜, R) Rˣ where
diff --git a/Mathlib/Geometry/Manifold/IntegralCurve.lean b/Mathlib/Geometry/Manifold/IntegralCurve.lean
index b16bd2c24cde9..624dbdbf85a0b 100644
--- a/Mathlib/Geometry/Manifold/IntegralCurve.lean
+++ b/Mathlib/Geometry/Manifold/IntegralCurve.lean
@@ -161,12 +161,12 @@ lemma IsIntegralCurveOn.hasDerivAt (hγ : IsIntegralCurveOn γ v s) {t : ℝ} (h
   have hsrc := extChartAt_source I (γ t₀) ▸ hsrc
   rw [hasDerivAt_iff_hasFDerivAt, ← hasMFDerivAt_iff_hasFDerivAt]
   apply (HasMFDerivAt.comp t
-    (hasMFDerivAt_extChartAt I hsrc) (hγ _ ht)).congr_mfderiv
+    (hasMFDerivAt_extChartAt (I := I) hsrc) (hγ _ ht)).congr_mfderiv
   rw [ContinuousLinearMap.ext_iff]
   intro a
   rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
     ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
-    mfderiv_chartAt_eq_tangentCoordChange I hsrc]
+    mfderiv_chartAt_eq_tangentCoordChange hsrc]
   rfl
 
 variable [SmoothManifoldWithCorners I M] in
@@ -174,17 +174,17 @@ lemma IsIntegralCurveAt.eventually_hasDerivAt (hγ : IsIntegralCurveAt γ v t₀
     ∀ᶠ t in 𝓝 t₀, HasDerivAt ((extChartAt I (γ t₀)) ∘ γ)
       (tangentCoordChange I (γ t) (γ t₀) (γ t) (v (γ t))) t := by
   apply eventually_mem_nhds_iff.mpr
-    (hγ.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds I _)) |>.and hγ |>.mono
+    (hγ.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds (I := I) _)) |>.and hγ |>.mono
   rintro t ⟨ht1, ht2⟩
   have hsrc := mem_of_mem_nhds ht1
   rw [mem_preimage, extChartAt_source I (γ t₀)] at hsrc
   rw [hasDerivAt_iff_hasFDerivAt, ← hasMFDerivAt_iff_hasFDerivAt]
-  apply (HasMFDerivAt.comp t (hasMFDerivAt_extChartAt I hsrc) ht2).congr_mfderiv
+  apply (HasMFDerivAt.comp t (hasMFDerivAt_extChartAt (I := I) hsrc) ht2).congr_mfderiv
   rw [ContinuousLinearMap.ext_iff]
   intro a
   rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
     ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
-    mfderiv_chartAt_eq_tangentCoordChange I hsrc]
+    mfderiv_chartAt_eq_tangentCoordChange hsrc]
   rfl
 
 /-! ### Translation lemmas -/
@@ -344,9 +344,9 @@ theorem exists_isIntegralCurveAt_of_contMDiffAt [CompleteSpace E]
   have hf3' := mem_of_mem_of_subset hf3 interior_subset
   have hft1 := mem_preimage.mp <|
     mem_of_mem_of_subset hf3' (extChartAt I x₀).target_subset_preimage_source
-  have hft2 := mem_extChartAt_source I xₜ
+  have hft2 := mem_extChartAt_source (I := 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
@@ -368,7 +368,7 @@ lemma exists_isIntegralCurveAt_of_contMDiffAt_boundaryless
     [CompleteSpace E] [BoundarylessManifold I M]
     (hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) x₀) :
     ∃ γ : ℝ → M, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀ :=
-  exists_isIntegralCurveAt_of_contMDiffAt t₀ hv (BoundarylessManifold.isInteriorPoint I)
+  exists_isIntegralCurveAt_of_contMDiffAt t₀ hv BoundarylessManifold.isInteriorPoint
 
 variable {t₀}
 
@@ -394,7 +394,7 @@ theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt (hγt₀ : I.IsInteriorPoi
   -- internal lemmas to reduce code duplication
   have hsrc {g} (hg : IsIntegralCurveAt g v t₀) :
     ∀ᶠ t in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t := eventually_mem_nhds_iff.mpr <|
-      continuousAt_def.mp hg.continuousAt _ <| extChartAt_source_mem_nhds I (g t₀)
+      continuousAt_def.mp hg.continuousAt _ <| extChartAt_source_mem_nhds (g t₀)
   have hmem {g : ℝ → M} {t} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t) :
     g t ∈ (extChartAt I (g t₀)).source := mem_preimage.mp <| mem_of_mem_nhds ht
   have hdrv {g} (hg : IsIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀) : ∀ᶠ t in 𝓝 t₀,
@@ -407,7 +407,7 @@ theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt (hγt₀ : I.IsInteriorPoi
       apply ht2.congr_deriv
       congr <;>
       rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]
-    · apply ((continuousAt_extChartAt I (g t₀)).comp hg.continuousAt).preimage_mem_nhds
+    · apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds
       rw [Function.comp_apply, ← h']
       exact hs
   have heq {g} (hg : IsIntegralCurveAt g v t₀) :
@@ -425,7 +425,7 @@ theorem isIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless [Boundaryless
     (hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) (γ t₀))
     (hγ : IsIntegralCurveAt γ v t₀) (hγ' : IsIntegralCurveAt γ' v t₀) (h : γ t₀ = γ' t₀) :
     γ =ᶠ[𝓝 t₀] γ' :=
-  isIntegralCurveAt_eventuallyEq_of_contMDiffAt (BoundarylessManifold.isInteriorPoint I) hv hγ hγ' h
+  isIntegralCurveAt_eventuallyEq_of_contMDiffAt BoundarylessManifold.isInteriorPoint hv hγ hγ' h
 
 variable [T2Space M] {a b : ℝ}
 
@@ -477,7 +477,7 @@ theorem isIntegralCurveOn_Ioo_eqOn_of_contMDiff_boundaryless [BoundarylessManifo
     (hγ : IsIntegralCurveOn γ v (Ioo a b)) (hγ' : IsIntegralCurveOn γ' v (Ioo a b))
     (h : γ t₀ = γ' t₀) : EqOn γ γ' (Ioo a b) :=
   isIntegralCurveOn_Ioo_eqOn_of_contMDiff
-    ht₀ (fun _ _ ↦ BoundarylessManifold.isInteriorPoint I) hv hγ hγ' h
+    ht₀ (fun _ _ ↦ BoundarylessManifold.isInteriorPoint) hv hγ hγ' h
 
 /-- Global integral curves are unique.
 
@@ -500,7 +500,7 @@ theorem isIntegralCurve_eq_of_contMDiff (hγt : ∀ t, I.IsInteriorPoint (γ t))
 theorem isIntegralCurve_Ioo_eq_of_contMDiff_boundaryless [BoundarylessManifold I M]
     (hv : ContMDiff I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)))
     (hγ : IsIntegralCurve γ v) (hγ' : IsIntegralCurve γ' v) (h : γ t₀ = γ' t₀) : γ = γ' :=
-  isIntegralCurve_eq_of_contMDiff (fun _ ↦ BoundarylessManifold.isInteriorPoint I) hv hγ hγ' h
+  isIntegralCurve_eq_of_contMDiff (fun _ ↦ BoundarylessManifold.isInteriorPoint) hv hγ hγ' h
 
 /-- For a global integral curve `γ`, if it crosses itself at `a b : ℝ`, then it is periodic with
 period `a - b`. -/
diff --git a/Mathlib/Geometry/Manifold/InteriorBoundary.lean b/Mathlib/Geometry/Manifold/InteriorBoundary.lean
index ae3c3a754f493..2fc03bd7d0a9a 100644
--- a/Mathlib/Geometry/Manifold/InteriorBoundary.lean
+++ b/Mathlib/Geometry/Manifold/InteriorBoundary.lean
@@ -50,14 +50,17 @@ open scoped Topology
 -- Let `M` be a manifold with corners over the pair `(E, H)`.
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-  {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
+  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
 
 namespace ModelWithCorners
+
+variable (I) in
 /-- `p ∈ M` is an interior point of a manifold `M` iff its image in the extended chart
 lies in the interior of the model space. -/
 def IsInteriorPoint (x : M) := extChartAt I x x ∈ interior (range I)
 
+variable (I) in
 /-- `p ∈ M` is a boundary point of a manifold `M` iff its image in the extended chart
 lies on the boundary of the model space. -/
 def IsBoundaryPoint (x : M) := extChartAt I x x ∈ frontier (range I)
@@ -68,8 +71,8 @@ protected def interior : Set M := { x : M | I.IsInteriorPoint x }
 
 lemma isInteriorPoint_iff {x : M} :
     I.IsInteriorPoint x ↔ extChartAt I x x ∈ interior (extChartAt I x).target :=
-  ⟨fun h ↦ (chartAt H x).mem_interior_extend_target _ (mem_chart_target H x) h,
-    fun h ↦ PartialHomeomorph.interior_extend_target_subset_interior_range _ _ h⟩
+  ⟨fun h ↦ (chartAt H x).mem_interior_extend_target (mem_chart_target H x) h,
+    fun h ↦ PartialHomeomorph.interior_extend_target_subset_interior_range _ h⟩
 
 variable (M) in
 /-- The **boundary** of a manifold `M` is the set of its boundary points. -/
@@ -106,7 +109,6 @@ lemma compl_interior : (I.interior M)ᶜ = I.boundary M:= by
 lemma compl_boundary : (I.boundary M)ᶜ = I.interior M:= by
   rw [← compl_interior, compl_compl]
 
-variable {I} in
 lemma _root_.range_mem_nhds_isInteriorPoint {x : M} (h : I.IsInteriorPoint x) :
     range I ∈ 𝓝 (extChartAt I x x) := by
   rw [mem_nhds_iff]
@@ -126,11 +128,11 @@ variable [I.Boundaryless]
 /-- Boundaryless `ModelWithCorners` implies boundaryless manifold. -/
 instance : BoundarylessManifold I M where
   isInteriorPoint' x := by
-    let r := ((chartAt H x).isOpen_extend_target I).interior_eq
+    let r := ((chartAt H x).isOpen_extend_target (I := I)).interior_eq
     have : extChartAt I x = (chartAt H x).extend I := rfl
     rw [← this] at r
     rw [isInteriorPoint_iff, r]
-    exact PartialEquiv.map_source _ (mem_extChartAt_source _ _)
+    exact PartialEquiv.map_source _ (mem_extChartAt_source _)
 
 end Boundaryless
 
@@ -145,18 +147,18 @@ lemma _root_.BoundarylessManifold.isInteriorPoint {x : M} [BoundarylessManifold
 
 /-- If `I` is boundaryless, `M` has full interior. -/
 lemma interior_eq_univ [BoundarylessManifold I M] : I.interior M = univ :=
-  eq_univ_of_forall fun _ => BoundarylessManifold.isInteriorPoint I
+  eq_univ_of_forall fun _ => BoundarylessManifold.isInteriorPoint
 
 /-- Boundaryless manifolds have empty boundary. -/
 lemma Boundaryless.boundary_eq_empty [BoundarylessManifold I M] : I.boundary M = ∅ := by
   rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]
 
 instance [BoundarylessManifold I M] : IsEmpty (I.boundary M) :=
-  isEmpty_coe_sort.mpr (Boundaryless.boundary_eq_empty I)
+  isEmpty_coe_sort.mpr Boundaryless.boundary_eq_empty
 
 /-- `M` is boundaryless iff its boundary is empty. -/
 lemma Boundaryless.iff_boundary_eq_empty : I.boundary M = ∅ ↔ BoundarylessManifold I M := by
-  refine ⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty I⟩
+  refine ⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty⟩
   intro x
   show x ∈ I.interior M
   rw [← compl_interior, compl_empty_iff] at h
@@ -172,11 +174,11 @@ end BoundarylessManifold
 /-! Interior and boundary of the product of two manifolds. -/
 section prod
 
-variable {I}
+variable
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
   {H' : Type*} [TopologicalSpace H']
   {N : Type*} [TopologicalSpace N] [ChartedSpace H' N]
-  (J : ModelWithCorners 𝕜 E' H') {x : M} {y : N}
+  {J : ModelWithCorners 𝕜 E' H'} {x : M} {y : N}
 
 /-- The interior of `M × N` is the product of the interiors of `M` and `N`. -/
 lemma interior_prod :
@@ -198,7 +200,7 @@ lemma interior_prod :
 lemma boundary_prod :
     (I.prod J).boundary (M × N) = Set.prod univ (J.boundary N) ∪ Set.prod (I.boundary M) univ := by
   let h := calc (I.prod J).boundary (M × N)
-    _ = ((I.prod J).interior (M × N))ᶜ := (I.prod J).compl_interior.symm
+    _ = ((I.prod J).interior (M × N))ᶜ := compl_interior.symm
     _ = ((I.interior M) ×ˢ (J.interior N))ᶜ := by rw [interior_prod]
     _ = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ := by rw [compl_prod_eq_union]
   rw [h, I.compl_interior, J.compl_interior, union_comm]
@@ -207,14 +209,14 @@ lemma boundary_prod :
 /-- If `M` is boundaryless, `∂(M×N) = M × ∂N`. -/
 lemma boundary_of_boundaryless_left [BoundarylessManifold I M] :
     (I.prod J).boundary (M × N) = Set.prod (univ : Set M) (J.boundary N) := by
-  rw [boundary_prod, Boundaryless.boundary_eq_empty I]
+  rw [boundary_prod, Boundaryless.boundary_eq_empty (I := I)]
   have : Set.prod (∅ : Set M) (univ : Set N) = ∅ := Set.empty_prod
   rw [this, union_empty]
 
 /-- If `N` is boundaryless, `∂(M×N) = ∂M × N`. -/
 lemma boundary_of_boundaryless_right [BoundarylessManifold J N] :
     (I.prod J).boundary (M × N) = Set.prod (I.boundary M) (univ : Set N) := by
-  rw [boundary_prod, Boundaryless.boundary_eq_empty J]
+  rw [boundary_prod, Boundaryless.boundary_eq_empty (I := J)]
   have : Set.prod (univ : Set M) (∅ : Set N) = ∅ := Set.prod_empty
   rw [this, empty_union]
 
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean b/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
index cbdbcb8afc391..f7b0ade18a085 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
@@ -32,15 +32,19 @@ open Bundle Set Topology
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
-  (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+  {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
-  (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
   {E'' : Type*} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H'']
-  (I'' : ModelWithCorners 𝕜 E'' H'') {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M'']
+  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M'']
 
 section ModelWithCorners
 namespace ModelWithCorners
 
+/- In general, the model with corner `I` is implicit in most theorems in differential geometry, but
+this section is about `I` as a map, not as a parameter. Therefore, we make it explicit. -/
+variable (I)
+
 /-! #### Model with corners -/
 
 protected theorem hasMFDerivAt {x} : HasMFDerivAt I 𝓘(𝕜, E) I x (ContinuousLinearMap.id _ _) :=
@@ -98,7 +102,7 @@ theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.sour
   · apply IsOpen.mem_nhds ((PartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1
 
 theorem mdifferentiableOn_atlas (h : e ∈ atlas H M) : MDifferentiableOn I I e e.source :=
-  fun _x hx => (mdifferentiableAt_atlas I h hx).mdifferentiableWithinAt
+  fun _x hx => (mdifferentiableAt_atlas h hx).mdifferentiableWithinAt
 
 theorem mdifferentiableAt_atlas_symm (h : e ∈ atlas H M) {x : H} (hx : x ∈ e.target) :
     MDifferentiableAt I I e.symm x := by
@@ -119,13 +123,13 @@ theorem mdifferentiableAt_atlas_symm (h : e ∈ atlas H M) {x : H} (hx : x ∈ e
   · apply IsOpen.mem_nhds ((PartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1
 
 theorem mdifferentiableOn_atlas_symm (h : e ∈ atlas H M) : MDifferentiableOn I I e.symm e.target :=
-  fun _x hx => (mdifferentiableAt_atlas_symm I h hx).mdifferentiableWithinAt
+  fun _x hx => (mdifferentiableAt_atlas_symm h hx).mdifferentiableWithinAt
 
 theorem mdifferentiable_of_mem_atlas (h : e ∈ atlas H M) : e.MDifferentiable I I :=
-  ⟨mdifferentiableOn_atlas I h, mdifferentiableOn_atlas_symm I h⟩
+  ⟨mdifferentiableOn_atlas h, mdifferentiableOn_atlas_symm h⟩
 
 theorem mdifferentiable_chart (x : M) : (chartAt H x).MDifferentiable I I :=
-  mdifferentiable_of_mem_atlas _ (chart_mem_atlas _ _)
+  mdifferentiable_of_mem_atlas (chart_mem_atlas _ _)
 
 end Charts
 
@@ -133,7 +137,6 @@ end Charts
 /-! ### Differentiable partial homeomorphisms -/
 
 namespace PartialHomeomorph.MDifferentiable
-variable {I I' I''}
 variable {e : PartialHomeomorph M M'} (he : e.MDifferentiable I I') {e' : PartialHomeomorph M' M''}
 include he
 
@@ -151,7 +154,7 @@ theorem symm_comp_deriv {x : M} (hx : x ∈ e.source) :
   have : mfderiv I I (e.symm ∘ e) x = (mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) :=
     mfderiv_comp x (he.mdifferentiableAt_symm (e.map_source hx)) (he.mdifferentiableAt hx)
   rw [← this]
-  have : mfderiv I I (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id I
+  have : mfderiv I I (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id
   rw [← this]
   apply Filter.EventuallyEq.mfderiv_eq
   have : e.source ∈ 𝓝 x := e.open_source.mem_nhds hx
@@ -218,24 +221,22 @@ end PartialHomeomorph.MDifferentiable
 
 section extChartAt
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*}
-  [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} {x y : M}
+variable [SmoothManifoldWithCorners I M] {s : Set M} {x y : M}
 
 theorem hasMFDerivAt_extChartAt (h : y ∈ (chartAt H x).source) :
     HasMFDerivAt I 𝓘(𝕜, E) (extChartAt I x) y (mfderiv I I (chartAt H x) y : _) :=
-  I.hasMFDerivAt.comp y ((mdifferentiable_chart I x).mdifferentiableAt h).hasMFDerivAt
+  I.hasMFDerivAt.comp y ((mdifferentiable_chart x).mdifferentiableAt h).hasMFDerivAt
 
 theorem hasMFDerivWithinAt_extChartAt (h : y ∈ (chartAt H x).source) :
     HasMFDerivWithinAt I 𝓘(𝕜, E) (extChartAt I x) s y (mfderiv I I (chartAt H x) y : _) :=
-  (hasMFDerivAt_extChartAt I h).hasMFDerivWithinAt
+  (hasMFDerivAt_extChartAt h).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_extChartAt (h : y ∈ (chartAt H x).source) :
     MDifferentiableAt I 𝓘(𝕜, E) (extChartAt I x) y :=
-  (hasMFDerivAt_extChartAt I h).mdifferentiableAt
+  (hasMFDerivAt_extChartAt h).mdifferentiableAt
 
 theorem mdifferentiableOn_extChartAt :
     MDifferentiableOn I 𝓘(𝕜, E) (extChartAt I x) (chartAt H x).source := fun _y hy =>
-  (hasMFDerivWithinAt_extChartAt I hy).mdifferentiableWithinAt
+  (hasMFDerivWithinAt_extChartAt hy).mdifferentiableWithinAt
 
 end extChartAt
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
index b1835322451ff..883bc8a09c31f 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
@@ -123,12 +123,12 @@ theorem mdifferentiableWithinAt_univ :
 theorem mdifferentiableWithinAt_inter (ht : t ∈ 𝓝 x) :
     MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
   rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
-    (differentiableWithinAt_localInvariantProp I I').liftPropWithinAt_inter ht]
+    differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter ht]
 
 theorem mdifferentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
     MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x := by
   rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
-    (differentiableWithinAt_localInvariantProp I I').liftPropWithinAt_inter' ht]
+    differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter' ht]
 
 theorem MDifferentiableAt.mdifferentiableWithinAt (h : MDifferentiableAt I I' f x) :
     MDifferentiableWithinAt I I' f s x :=
@@ -169,7 +169,7 @@ theorem ContMDiffWithinAt.mdifferentiableWithinAt (hf : ContMDiffWithinAt I I' n
   suffices h : MDifferentiableWithinAt I I' f (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x by
     rwa [mdifferentiableWithinAt_inter'] at h
     apply hf.1.preimage_mem_nhdsWithin
-    exact extChartAt_source_mem_nhds I' (f x)
+    exact extChartAt_source_mem_nhds (f x)
   rw [mdifferentiableWithinAt_iff]
   exact ⟨hf.1.mono inter_subset_left, (hf.2.differentiableWithinAt hn).mono (by mfld_set_tac)⟩
 
@@ -255,8 +255,8 @@ 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
-        (h.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _ _)))
+      (extChartAt_preimage_mem_nhdsWithin
+        (h.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _)))
   mfld_set_tac
 
 variable {f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}
@@ -287,7 +287,7 @@ theorem mdifferentiableWithinAt_iff_of_mem_source {x' : M} {y : M'}
       ContinuousWithinAt f s x' ∧
         DifferentiableWithinAt 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
           ((extChartAt I x).symm ⁻¹' s ∩ Set.range I) ((extChartAt I x) x') :=
-  (differentiableWithinAt_localInvariantProp I I').liftPropWithinAt_indep_chart
+  differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart
     (StructureGroupoid.chart_mem_maximalAtlas _ x) hx (StructureGroupoid.chart_mem_maximalAtlas _ y)
     hy
 
@@ -330,13 +330,13 @@ 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 h
+  exact extChartAt_preimage_mem_nhdsWithin h
 
 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 h
+  exact extChartAt_preimage_mem_nhds h
 
 theorem HasMFDerivWithinAt.union (hs : HasMFDerivWithinAt I I' f s x f')
     (ht : HasMFDerivWithinAt I I' f t x f') : HasMFDerivWithinAt I I' f (s ∪ t) x f' := by
@@ -403,7 +403,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 ht)]
+    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]
 
 theorem mfderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : mfderivWithin I I' f s x = mfderiv I I' f x := by
   rw [← mfderivWithin_univ, ← univ_inter s, mfderivWithin_inter h]
@@ -479,7 +479,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 h₁
+      extChartAt_preimage_mem_nhdsWithin h₁
     apply Filter.mem_of_superset this fun y => _
     simp (config := { contextual := true }) only [hx, mfld_simps]
   · simp only [hx, mfld_simps]
@@ -586,8 +586,8 @@ 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
-        (hf.1.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _ _))
+      extChartAt_preimage_mem_nhdsWithin
+        (hf.1.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _))
     unfold HasMFDerivWithinAt at *
     rw [← hasFDerivWithinAt_inter' this, ← extChartAt_preimage_inter_eq] at hf ⊢
     have : writtenInExtChartAt I I' x f ((extChartAt I x) x) = (extChartAt I' (f x)) (f x) := by
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean b/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
index 88e42b72004c0..6d30a6a3b1c43 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
@@ -116,11 +116,12 @@ We use the names `MDifferentiable` and `mfderiv`, where the prefix letter `m` me
 -/
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*}
+  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type*}
   [TopologicalSpace M] [ChartedSpace H M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
-  {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type*}
+  {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*}
   [TopologicalSpace M'] [ChartedSpace H' M']
 
+variable (I I') in
 /-- Property in the model space of a model with corners of being differentiable within at set at a
 point, when read in the model vector space. This property will be lifted to manifolds to define
 differentiable functions between manifolds. -/
@@ -177,15 +178,18 @@ theorem differentiableWithinAt_localInvariantProp :
 @[deprecated (since := "2024-10-10")]
 alias differentiable_within_at_localInvariantProp := differentiableWithinAt_localInvariantProp
 
+variable (I) in
 /-- Predicate ensuring that, at a point and within a set, a function can have at most one
 derivative. This is expressed using the preferred chart at the considered point. -/
 def UniqueMDiffWithinAt (s : Set M) (x : M) :=
   UniqueDiffWithinAt 𝕜 ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x)
 
+variable (I) in
 /-- Predicate ensuring that, at all points of a set, a function can have at most one derivative. -/
 def UniqueMDiffOn (s : Set M) :=
   ∀ x ∈ s, UniqueMDiffWithinAt I s x
 
+variable (I I') in
 /-- `MDifferentiableWithinAt I I' f s x` indicates that the function `f` between manifolds
 has a derivative at the point `x` within the set `s`.
 This is a generalization of `DifferentiableWithinAt` to manifolds.
@@ -206,19 +210,18 @@ theorem mdifferentiableWithinAt_iff' (f : M → M') (s : Set M) (x : M) :
 @[deprecated (since := "2024-04-30")]
 alias mdifferentiableWithinAt_iff_liftPropWithinAt := mdifferentiableWithinAt_iff'
 
-variable {I I'} in
 theorem MDifferentiableWithinAt.continuousWithinAt {f : M → M'} {s : Set M} {x : M}
     (hf : MDifferentiableWithinAt I I' f s x) :
     ContinuousWithinAt f s x :=
   mdifferentiableWithinAt_iff' .. |>.1 hf |>.1
 
-variable {I I'} in
 theorem MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt
     {f : M → M'} {s : Set M} {x : M} (hf : MDifferentiableWithinAt I I' f s x) :
     DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f)
       ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x) :=
   mdifferentiableWithinAt_iff' .. |>.1 hf |>.2
 
+variable (I I') in
 /-- `MDifferentiableAt I I' f x` indicates that the function `f` between manifolds
 has a derivative at the point `x`.
 This is a generalization of `DifferentiableAt` to manifolds.
@@ -242,35 +245,35 @@ theorem mdifferentiableAt_iff (f : M → M') (x : M) :
 @[deprecated (since := "2024-04-30")]
 alias mdifferentiableAt_iff_liftPropAt := mdifferentiableAt_iff
 
-variable {I I'} in
 theorem MDifferentiableAt.continuousAt {f : M → M'} {x : M} (hf : MDifferentiableAt I I' f x) :
     ContinuousAt f x :=
   mdifferentiableAt_iff .. |>.1 hf |>.1
 
-variable {I I'} in
 theorem MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt {f : M → M'} {x : M}
     (hf : MDifferentiableAt I I' f x) :
     DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range I) ((extChartAt I x) x) :=
   mdifferentiableAt_iff .. |>.1 hf |>.2
 
+variable (I I') in
 /-- `MDifferentiableOn I I' f s` indicates that the function `f` between manifolds
 has a derivative within `s` at all points of `s`.
 This is a generalization of `DifferentiableOn` to manifolds. -/
 def MDifferentiableOn (f : M → M') (s : Set M) :=
   ∀ x ∈ s, MDifferentiableWithinAt I I' f s x
 
+variable (I I') in
 /-- `MDifferentiable I I' f` indicates that the function `f` between manifolds
 has a derivative everywhere.
 This is a generalization of `Differentiable` to manifolds. -/
 def MDifferentiable (f : M → M') :=
   ∀ x, MDifferentiableAt I I' f x
 
+variable (I I') in
 /-- Prop registering if a partial homeomorphism is a local diffeomorphism on its source -/
 def PartialHomeomorph.MDifferentiable (f : PartialHomeomorph M M') :=
   MDifferentiableOn I I' f f.source ∧ MDifferentiableOn I' I f.symm f.target
 
-variable [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
-
+variable (I I') in
 /-- `HasMFDerivWithinAt I I' f s x f'` indicates that the function `f` between manifolds
 has, at the point `x` and within the set `s`, the derivative `f'`. Here, `f'` is a continuous linear
 map from the tangent space at `x` to the tangent space at `f x`.
@@ -288,6 +291,7 @@ def HasMFDerivWithinAt (f : M → M') (s : Set M) (x : M)
     HasFDerivWithinAt (writtenInExtChartAt I I' x f : E → E') f'
       ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x)
 
+variable (I I') in
 /-- `HasMFDerivAt I I' f x f'` indicates that the function `f` between manifolds
 has, at the point `x`, the derivative `f'`. Here, `f'` is a continuous linear
 map from the tangent space at `x` to the tangent space at `f x`.
@@ -301,6 +305,7 @@ def HasMFDerivAt (f : M → M') (x : M) (f' : TangentSpace I x →L[𝕜] Tangen
     HasFDerivWithinAt (writtenInExtChartAt I I' x f : E → E') f' (range I) ((extChartAt I x) x)
 
 open Classical in
+variable (I I') in
 /-- Let `f` be a function between two smooth manifolds. Then `mfderivWithin I I' f s x` is the
 derivative of `f` at `x` within `s`, as a continuous linear map from the tangent space at `x` to the
 tangent space at `f x`. -/
@@ -312,6 +317,7 @@ def mfderivWithin (f : M → M') (s : Set M) (x : M) : TangentSpace I x →L[
   else 0
 
 open Classical in
+variable (I I') in
 /-- Let `f` be a function between two smooth manifolds. Then `mfderiv I I' f x` is the derivative of
 `f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at
 `f x`. -/
@@ -320,10 +326,12 @@ def mfderiv (f : M → M') (x : M) : TangentSpace I x →L[𝕜] TangentSpace I'
     (fderivWithin 𝕜 (writtenInExtChartAt I I' x f : E → E') (range I) ((extChartAt I x) x) : _)
   else 0
 
+variable (I I') in
 /-- The derivative within a set, as a map between the tangent bundles -/
 def tangentMapWithin (f : M → M') (s : Set M) : TangentBundle I M → TangentBundle I' M' := fun p =>
   ⟨f p.1, (mfderivWithin I I' f s p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
 
+variable (I I') in
 /-- The derivative, as a map between the tangent bundles -/
 def tangentMap (f : M → M') : TangentBundle I M → TangentBundle I' M' := fun p =>
   ⟨f p.1, (mfderiv I I' f p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
index e80b20105886e..2bbe312b6c383 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
@@ -27,12 +27,12 @@ section SpecificFunctions
 /-! ### Differentiability of specific functions -/
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*}
+  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type*}
   [TopologicalSpace M] [ChartedSpace H M] {E' : Type*}
   [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
-  (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
   {E'' : Type*} [NormedAddCommGroup E''] [NormedSpace 𝕜 E'']
-  {H'' : Type*} [TopologicalSpace H''] (I'' : ModelWithCorners 𝕜 E'' H'') {M'' : Type*}
+  {H'' : Type*} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type*}
   [TopologicalSpace M''] [ChartedSpace H'' M'']
 
 namespace ContinuousLinearMap
@@ -107,34 +107,34 @@ theorem hasMFDerivAt_id (x : M) :
     HasMFDerivAt I I (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) := by
   refine ⟨continuousAt_id, ?_⟩
   have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y := by
-    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin I x)
+    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
     mfld_set_tac
   apply HasFDerivWithinAt.congr_of_eventuallyEq (hasFDerivWithinAt_id _ _) this
   simp only [mfld_simps]
 
 theorem hasMFDerivWithinAt_id (s : Set M) (x : M) :
     HasMFDerivWithinAt I I (@id M) s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) :=
-  (hasMFDerivAt_id I x).hasMFDerivWithinAt
+  (hasMFDerivAt_id x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_id : MDifferentiableAt I I (@id M) x :=
-  (hasMFDerivAt_id I x).mdifferentiableAt
+  (hasMFDerivAt_id x).mdifferentiableAt
 
 theorem mdifferentiableWithinAt_id : MDifferentiableWithinAt I I (@id M) s x :=
-  (mdifferentiableAt_id I).mdifferentiableWithinAt
+  mdifferentiableAt_id.mdifferentiableWithinAt
 
-theorem mdifferentiable_id : MDifferentiable I I (@id M) := fun _ => mdifferentiableAt_id I
+theorem mdifferentiable_id : MDifferentiable I I (@id M) := fun _ => mdifferentiableAt_id
 
 theorem mdifferentiableOn_id : MDifferentiableOn I I (@id M) s :=
-  (mdifferentiable_id I).mdifferentiableOn
+  mdifferentiable_id.mdifferentiableOn
 
 @[simp, mfld_simps]
 theorem mfderiv_id : mfderiv I I (@id M) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x) :=
-  HasMFDerivAt.mfderiv (hasMFDerivAt_id I x)
+  HasMFDerivAt.mfderiv (hasMFDerivAt_id x)
 
 theorem mfderivWithin_id (hxs : UniqueMDiffWithinAt I s x) :
     mfderivWithin I I (@id M) s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x) := by
-  rw [MDifferentiable.mfderivWithin (mdifferentiableAt_id I) hxs]
-  exact mfderiv_id I
+  rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]
+  exact mfderiv_id
 
 @[simp, mfld_simps]
 theorem tangentMap_id : tangentMap I I (id : M → M) = id := by ext1 ⟨x, v⟩; simp [tangentMap]
@@ -162,28 +162,28 @@ theorem hasMFDerivAt_const (c : M') (x : M) :
 
 theorem hasMFDerivWithinAt_const (c : M') (s : Set M) (x : M) :
     HasMFDerivWithinAt I I' (fun _ : M => c) s x (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
-  (hasMFDerivAt_const I I' c x).hasMFDerivWithinAt
+  (hasMFDerivAt_const c x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_const : MDifferentiableAt I I' (fun _ : M => c) x :=
-  (hasMFDerivAt_const I I' c x).mdifferentiableAt
+  (hasMFDerivAt_const c x).mdifferentiableAt
 
 theorem mdifferentiableWithinAt_const : MDifferentiableWithinAt I I' (fun _ : M => c) s x :=
-  (mdifferentiableAt_const I I').mdifferentiableWithinAt
+  mdifferentiableAt_const.mdifferentiableWithinAt
 
 theorem mdifferentiable_const : MDifferentiable I I' fun _ : M => c := fun _ =>
-  mdifferentiableAt_const I I'
+  mdifferentiableAt_const
 
 theorem mdifferentiableOn_const : MDifferentiableOn I I' (fun _ : M => c) s :=
-  (mdifferentiable_const I I').mdifferentiableOn
+  mdifferentiable_const.mdifferentiableOn
 
 @[simp, mfld_simps]
 theorem mfderiv_const :
     mfderiv I I' (fun _ : M => c) x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
-  HasMFDerivAt.mfderiv (hasMFDerivAt_const I I' c x)
+  HasMFDerivAt.mfderiv (hasMFDerivAt_const c x)
 
 theorem mfderivWithin_const (hxs : UniqueMDiffWithinAt I s x) :
     mfderivWithin I I' (fun _ : M => c) s x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
-  (hasMFDerivWithinAt_const _ _ _ _ _).mfderivWithin hxs
+  (hasMFDerivWithinAt_const _ _ _).mfderivWithin hxs
 
 end Const
 
@@ -202,42 +202,42 @@ theorem hasMFDerivAt_fst (x : M × M') :
     apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
     mfld_set_tac
     -/
-    filter_upwards [extChartAt_target_mem_nhdsWithin (I.prod I') x] with y hy
+    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
     rw [extChartAt_prod] at hy
     exact (extChartAt I x.1).right_inv hy.1
   apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_fst this
   -- Porting note: next line was `simp only [mfld_simps]`
-  exact (extChartAt I x.1).right_inv <| (extChartAt I x.1).map_source (mem_extChartAt_source _ _)
+  exact (extChartAt I x.1).right_inv <| (extChartAt I x.1).map_source (mem_extChartAt_source _)
 
 theorem hasMFDerivWithinAt_fst (s : Set (M × M')) (x : M × M') :
     HasMFDerivWithinAt (I.prod I') I Prod.fst s x
       (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
-  (hasMFDerivAt_fst I I' x).hasMFDerivWithinAt
+  (hasMFDerivAt_fst x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_fst {x : M × M'} : MDifferentiableAt (I.prod I') I Prod.fst x :=
-  (hasMFDerivAt_fst I I' x).mdifferentiableAt
+  (hasMFDerivAt_fst x).mdifferentiableAt
 
 theorem mdifferentiableWithinAt_fst {s : Set (M × M')} {x : M × M'} :
     MDifferentiableWithinAt (I.prod I') I Prod.fst s x :=
-  (mdifferentiableAt_fst I I').mdifferentiableWithinAt
+  mdifferentiableAt_fst.mdifferentiableWithinAt
 
 theorem mdifferentiable_fst : MDifferentiable (I.prod I') I (Prod.fst : M × M' → M) := fun _ =>
-  mdifferentiableAt_fst I I'
+  mdifferentiableAt_fst
 
 theorem mdifferentiableOn_fst {s : Set (M × M')} : MDifferentiableOn (I.prod I') I Prod.fst s :=
-  (mdifferentiable_fst I I').mdifferentiableOn
+  mdifferentiable_fst.mdifferentiableOn
 
 @[simp, mfld_simps]
 theorem mfderiv_fst {x : M × M'} :
     mfderiv (I.prod I') I Prod.fst x =
       ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
-  (hasMFDerivAt_fst I I' x).mfderiv
+  (hasMFDerivAt_fst x).mfderiv
 
 theorem mfderivWithin_fst {s : Set (M × M')} {x : M × M'}
     (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
     mfderivWithin (I.prod I') I Prod.fst s x =
       ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) := by
-  rw [MDifferentiable.mfderivWithin (mdifferentiableAt_fst I I') hxs]; exact mfderiv_fst I I'
+  rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]; exact mfderiv_fst
 
 @[simp, mfld_simps]
 theorem tangentMap_prod_fst {p : TangentBundle (I.prod I') (M × M')} :
@@ -264,42 +264,42 @@ theorem hasMFDerivAt_snd (x : M × M') :
     apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin (I.prod I') x)
     mfld_set_tac
     -/
-    filter_upwards [extChartAt_target_mem_nhdsWithin (I.prod I') x] with y hy
+    filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
     rw [extChartAt_prod] at hy
     exact (extChartAt I' x.2).right_inv hy.2
   apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_snd this
   -- Porting note: the next line was `simp only [mfld_simps]`
-  exact (extChartAt I' x.2).right_inv <| (extChartAt I' x.2).map_source (mem_extChartAt_source _ _)
+  exact (extChartAt I' x.2).right_inv <| (extChartAt I' x.2).map_source (mem_extChartAt_source _)
 
 theorem hasMFDerivWithinAt_snd (s : Set (M × M')) (x : M × M') :
     HasMFDerivWithinAt (I.prod I') I' Prod.snd s x
       (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) :=
-  (hasMFDerivAt_snd I I' x).hasMFDerivWithinAt
+  (hasMFDerivAt_snd x).hasMFDerivWithinAt
 
 theorem mdifferentiableAt_snd {x : M × M'} : MDifferentiableAt (I.prod I') I' Prod.snd x :=
-  (hasMFDerivAt_snd I I' x).mdifferentiableAt
+  (hasMFDerivAt_snd x).mdifferentiableAt
 
 theorem mdifferentiableWithinAt_snd {s : Set (M × M')} {x : M × M'} :
     MDifferentiableWithinAt (I.prod I') I' Prod.snd s x :=
-  (mdifferentiableAt_snd I I').mdifferentiableWithinAt
+  mdifferentiableAt_snd.mdifferentiableWithinAt
 
 theorem mdifferentiable_snd : MDifferentiable (I.prod I') I' (Prod.snd : M × M' → M') := fun _ =>
-  mdifferentiableAt_snd I I'
+  mdifferentiableAt_snd
 
 theorem mdifferentiableOn_snd {s : Set (M × M')} : MDifferentiableOn (I.prod I') I' Prod.snd s :=
-  (mdifferentiable_snd I I').mdifferentiableOn
+  mdifferentiable_snd.mdifferentiableOn
 
 @[simp, mfld_simps]
 theorem mfderiv_snd {x : M × M'} :
     mfderiv (I.prod I') I' Prod.snd x =
       ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) :=
-  (hasMFDerivAt_snd I I' x).mfderiv
+  (hasMFDerivAt_snd x).mfderiv
 
 theorem mfderivWithin_snd {s : Set (M × M')} {x : M × M'}
     (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
     mfderivWithin (I.prod I') I' Prod.snd s x =
       ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2) := by
-  rw [MDifferentiable.mfderivWithin (mdifferentiableAt_snd I I') hxs]; exact mfderiv_snd I I'
+  rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]; exact mfderiv_snd
 
 @[simp, mfld_simps]
 theorem tangentMap_prod_snd {p : TangentBundle (I.prod I') (M × M')} :
@@ -315,8 +315,6 @@ theorem tangentMapWithin_prod_snd {s : Set (M × M')} {p : TangentBundle (I.prod
   · rcases p with ⟨⟩; rfl
   · exact hs
 
-variable {I I' I''}
-
 theorem MDifferentiableAt.mfderiv_prod {f : M → M'} {g : M → M''} {x : M}
     (hf : MDifferentiableAt I I' f x) (hg : MDifferentiableAt I I'' g x) :
     mfderiv I (I'.prod I'') (fun x => (f x, g x)) x =
@@ -326,18 +324,16 @@ theorem MDifferentiableAt.mfderiv_prod {f : M → M'} {g : M → M''} {x : M}
   exact hf.differentiableWithinAt_writtenInExtChartAt.fderivWithin_prod
     hg.differentiableWithinAt_writtenInExtChartAt (I.uniqueDiffOn _ (mem_range_self _))
 
-variable (I I' I'')
-
 theorem mfderiv_prod_left {x₀ : M} {y₀ : M'} :
     mfderiv I (I.prod I') (fun x => (x, y₀)) x₀ =
       ContinuousLinearMap.inl 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) := by
-  refine ((mdifferentiableAt_id I).mfderiv_prod (mdifferentiableAt_const I I')).trans ?_
+  refine (mdifferentiableAt_id.mfderiv_prod mdifferentiableAt_const).trans ?_
   rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inl]
 
 theorem mfderiv_prod_right {x₀ : M} {y₀ : M'} :
     mfderiv I' (I.prod I') (fun y => (x₀, y)) y₀ =
       ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀) := by
-  refine ((mdifferentiableAt_const I' I).mfderiv_prod (mdifferentiableAt_id I')).trans ?_
+  refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
   rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]
 
 /-- The total derivative of a function in two variables is the sum of the partial derivatives.
@@ -350,12 +346,11 @@ theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'}
         mfderiv (I.prod I') I'' (fun z : M × M' => f (z.1, p.2)) p +
           mfderiv (I.prod I') I'' (fun z : M × M' => f (p.1, z.2)) p := by
   dsimp only
-  erw [mfderiv_comp_of_eq hf ((mdifferentiableAt_fst I I').prod_mk (mdifferentiableAt_const _ _))
-      rfl,
-    mfderiv_comp_of_eq hf ((mdifferentiableAt_const _ _).prod_mk (mdifferentiableAt_snd I I')) rfl,
+  erw [mfderiv_comp_of_eq hf (mdifferentiableAt_fst.prod_mk mdifferentiableAt_const) rfl,
+    mfderiv_comp_of_eq hf (mdifferentiableAt_const.prod_mk mdifferentiableAt_snd) rfl,
     ← ContinuousLinearMap.comp_add,
-    (mdifferentiableAt_fst I I').mfderiv_prod (mdifferentiableAt_const (I.prod I') I'),
-    (mdifferentiableAt_const (I.prod I') I).mfderiv_prod (mdifferentiableAt_snd I I'), mfderiv_fst,
+    mdifferentiableAt_fst.mfderiv_prod mdifferentiableAt_const,
+    mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_snd, mfderiv_fst,
     mfderiv_snd, mfderiv_const, mfderiv_const]
   symm
   convert ContinuousLinearMap.comp_id <| mfderiv (.prod I I') I'' f (p.1, p.2)
@@ -374,7 +369,6 @@ canonical, but in this case (the tangent space of a vector space) it is canonica
 
 section Group
 
-variable {I}
 variable {z : M} {f g : M → E'} {f' g' : TangentSpace I z →L[𝕜] E'}
 
 theorem HasMFDerivAt.add (hf : HasMFDerivAt I 𝓘(𝕜, E') f z f')
@@ -460,7 +454,6 @@ end Group
 
 section AlgebraOverRing
 
-variable {I}
 variable {z : M} {F' : Type*} [NormedRing F'] [NormedAlgebra 𝕜 F'] {p q : M → F'}
   {p' q' : TangentSpace I z →L[𝕜] F'}
 
@@ -495,7 +488,6 @@ end AlgebraOverRing
 
 section AlgebraOverCommRing
 
-variable {I}
 variable {z : M} {F' : Type*} [NormedCommRing F'] [NormedAlgebra 𝕜 F'] {p q : M → F'}
   {p' q' : TangentSpace I z →L[𝕜] F'}
 
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean b/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
index 633857d4ac0f7..4814f3ebcafdf 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
@@ -19,7 +19,7 @@ open Bundle
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
-  (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+  {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
   [SmoothManifoldWithCorners I M]
 
 /-- The derivative of the chart at a base point is the chart of the tangent bundle, composed with
@@ -31,7 +31,7 @@ theorem tangentMap_chart {p q : TangentBundle I M} (h : q.1 ∈ (chartAt H p.1).
   dsimp [tangentMap]
   rw [MDifferentiableAt.mfderiv]
   · rfl
-  · exact mdifferentiableAt_atlas _ (chart_mem_atlas _ _) h
+  · exact mdifferentiableAt_atlas (chart_mem_atlas _ _) h
 
 /-- The derivative of the inverse of the chart at a base point is the inverse of the chart of the
 tangent bundle, composed with the identification between the tangent bundle of the model space and
@@ -41,7 +41,7 @@ theorem tangentMap_chart_symm {p : TangentBundle I M} {q : TangentBundle I H}
     tangentMap I I (chartAt H p.1).symm q =
       (chartAt (ModelProd H E) p).symm (TotalSpace.toProd H E q) := by
   dsimp only [tangentMap]
-  rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm _ (chart_mem_atlas _ _) h)]
+  rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm (chart_mem_atlas _ _) h)]
   simp only [ContinuousLinearMap.coe_coe, TangentBundle.chartAt, h, tangentBundleCore,
     mfld_simps, (· ∘ ·)]
   -- `simp` fails to apply `PartialEquiv.prod_symm` with `ModelProd`
@@ -50,7 +50,7 @@ theorem tangentMap_chart_symm {p : TangentBundle I M} {q : TangentBundle I H}
 
 lemma mfderiv_chartAt_eq_tangentCoordChange {x y : M} (hsrc : x ∈ (chartAt H y).source) :
     mfderiv I I (chartAt H y) x = tangentCoordChange I x y x := by
-  have := mdifferentiableAt_atlas I (ChartedSpace.chart_mem_atlas _) hsrc
+  have := mdifferentiableAt_atlas (I := I) (ChartedSpace.chart_mem_atlas _) hsrc
   simp [mfderiv, if_pos this, Function.comp_assoc]
 
 /-- The preimage under the projection from the tangent bundle of a set with unique differential in
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean b/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
index 076089056c123..4facc7f820910 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
+++ b/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
@@ -44,7 +44,7 @@ theorem UniqueMDiffWithinAt.image_denseRange (hs : UniqueMDiffWithinAt I s x)
     {f : M → M'} {f' : E →L[𝕜] E'} (hf : HasMFDerivWithinAt I I' f s x f')
     (hd : DenseRange f') : UniqueMDiffWithinAt I' (f '' s) (f x) := by
   /- Rewrite in coordinates, apply `HasFDerivWithinAt.uniqueDiffWithinAt`. -/
-  have := hs.inter' <| hf.1 (extChartAt_source_mem_nhds I' (f x))
+  have := hs.inter' <| hf.1 (extChartAt_source_mem_nhds (I := I') (f x))
   refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt
   case pt => simp only [mfld_simps]
   case sub1 => mfld_set_tac
@@ -92,8 +92,8 @@ theorem UniqueMDiffOn.uniqueDiffOn_target_inter (hs : UniqueMDiffOn I s) (x : M)
   apply UniqueMDiffOn.uniqueDiffOn
   rw [← PartialEquiv.image_source_inter_eq', inter_comm, extChartAt_source]
   exact (hs.inter (chartAt H x).open_source).image_denseRange'
-    (fun y hy ↦ hasMFDerivWithinAt_extChartAt I hy.2)
-    fun y hy ↦ ((mdifferentiable_chart _ _).mfderiv_surjective hy.2).denseRange
+    (fun y hy ↦ hasMFDerivWithinAt_extChartAt hy.2)
+    fun y hy ↦ ((mdifferentiable_chart _).mfderiv_surjective hy.2).denseRange
 
 variable [SmoothManifoldWithCorners I M]  in
 /-- When considering functions between manifolds, this statement shows up often. It entails
@@ -107,7 +107,7 @@ theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage (hs : UniqueMDiffOn I s) (x :
     intro z hz
     apply (hs z hz.1).inter'
     apply (hf z hz.1).preimage_mem_nhdsWithin
-    exact (isOpen_extChartAt_source I' y).mem_nhds hz.2
+    exact (isOpen_extChartAt_source y).mem_nhds hz.2
   this.uniqueDiffOn_target_inter _
 
 end
@@ -120,7 +120,7 @@ variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {Z : M → Type
 
 theorem Trivialization.mdifferentiable (e : Trivialization F (π F Z)) [MemTrivializationAtlas e] :
     e.toPartialHomeomorph.MDifferentiable (I.prod 𝓘(𝕜, F)) (I.prod 𝓘(𝕜, F)) :=
-  ⟨(e.smoothOn I).mdifferentiableOn, (e.smoothOn_symm I).mdifferentiableOn⟩
+  ⟨e.smoothOn.mdifferentiableOn, e.smoothOn_symm.mdifferentiableOn⟩
 
 theorem UniqueMDiffWithinAt.smooth_bundle_preimage {p : TotalSpace F Z}
     (hs : UniqueMDiffWithinAt I s p.proj) :
diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean
index d0c29cb8d57a6..db39ef95a11c9 100644
--- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean
+++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean
@@ -371,7 +371,6 @@ theorem IsSubordinate.support_subset {fs : SmoothBumpCovering ι I M s} {U : M 
   Subset.trans subset_closure (h i)
 
 variable (I) in
-
 /-- Let `M` be a smooth manifold with corners modelled on a finite dimensional real vector space.
 Suppose also that `M` is a Hausdorff `σ`-compact topological space. Let `s` be a closed set
 in `M` and `U : M → Set M` be a collection of sets such that `U x ∈ 𝓝 x` for every `x ∈ s`.
@@ -383,7 +382,7 @@ theorem exists_isSubordinate [T2Space M] [SigmaCompactSpace M] (hs : IsClosed s)
   haveI : LocallyCompactSpace H := I.locallyCompactSpace
   haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
   -- Next we choose a covering by supports of smooth bump functions
-  have hB := fun x hx => SmoothBumpFunction.nhds_basis_support I (hU x hx)
+  have hB := fun x hx => SmoothBumpFunction.nhds_basis_support (I := I) (hU x hx)
   rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with
     ⟨ι, c, f, hf, hsub', hfin⟩
   choose hcs hfU using hf
@@ -718,7 +717,7 @@ theorem IsOpen.exists_msmooth_support_eq {s : Set M} (hs : IsOpen s) :
   · apply SmoothPartitionOfUnity.smooth_finsum_smul
     intro c x hx
     apply (g_diff c (chartAt H c x)).comp
-    exact contMDiffAt_of_mem_maximalAtlas (SmoothManifoldWithCorners.chart_mem_maximalAtlas I _)
+    exact contMDiffAt_of_mem_maximalAtlas (SmoothManifoldWithCorners.chart_mem_maximalAtlas _)
       (hf c hx)
   · intro x
     apply finsum_nonneg (fun c ↦ h''g c x)
diff --git a/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean b/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
index d8ac4a298bca8..6cc1c879d0531 100644
--- a/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
+++ b/Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
@@ -82,13 +82,13 @@ section TypeCat
 
 /-- The sheaf of smooth functions from `M` to `N`, as a sheaf of types. -/
 def smoothSheaf : TopCat.Sheaf (Type u) (TopCat.of M) :=
-  (contDiffWithinAt_localInvariantProp IM I ⊤).sheaf M N
+  (contDiffWithinAt_localInvariantProp (I := IM) (I' := I) ⊤).sheaf M N
 
 variable {M}
 
 instance smoothSheaf.coeFun (U : (Opens (TopCat.of M))ᵒᵖ) :
     CoeFun ((smoothSheaf IM I M N).presheaf.obj U) (fun _ ↦ ↑(unop U) → N) :=
-  (contDiffWithinAt_localInvariantProp IM I ⊤).sheafHasCoeToFun _ _ _
+  (contDiffWithinAt_localInvariantProp ⊤).sheafHasCoeToFun _ _ _
 
 open Manifold in
 /-- The object of `smoothSheaf IM I M N` for the open set `U` in `M` is
@@ -135,12 +135,12 @@ variable {IM I N}
 @[simp] lemma smoothSheaf.eval_germ (U : Opens M) (x : M) (hx : x ∈ U)
     (f : (smoothSheaf IM I M N).presheaf.obj (op U)) :
     smoothSheaf.eval IM I N (x : M) ((smoothSheaf IM I M N).presheaf.germ U x hx f) = f ⟨x, hx⟩ :=
-  TopCat.stalkToFiber_germ ((contDiffWithinAt_localInvariantProp IM I ⊤).localPredicate M N) _ _ _ _
+  TopCat.stalkToFiber_germ ((contDiffWithinAt_localInvariantProp ⊤).localPredicate M N) _ _ _ _
 
 lemma smoothSheaf.smooth_section {U : (Opens (TopCat.of M))ᵒᵖ}
     (f : (smoothSheaf IM I M N).presheaf.obj U) :
     Smooth IM I f :=
-  (contDiffWithinAt_localInvariantProp IM I ⊤).section_spec _ _ _ _
+  (contDiffWithinAt_localInvariantProp ⊤).section_spec _ _ _ _
 
 end TypeCat
 
@@ -278,7 +278,7 @@ example : (CategoryTheory.sheafCompose _ (CategoryTheory.forget CommRingCat.{u})
 
 instance smoothSheafCommRing.coeFun (U : (Opens (TopCat.of M))ᵒᵖ) :
     CoeFun ((smoothSheafCommRing IM I M R).presheaf.obj U) (fun _ ↦ ↑(unop U) → R) :=
-  (contDiffWithinAt_localInvariantProp IM I ⊤).sheafHasCoeToFun _ _ _
+  (contDiffWithinAt_localInvariantProp ⊤).sheafHasCoeToFun _ _ _
 
 open CategoryTheory Limits
 
diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
index 85e1eada2814c..f93d14d8c5e1b 100644
--- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
+++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
@@ -496,11 +496,10 @@ section contDiffGroupoid
 
 
 variable {m n : ℕ∞} {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*}
+  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type*}
   [TopologicalSpace M]
 
-variable (n)
-
+variable (n I) in
 /-- 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
@@ -539,13 +538,12 @@ def contDiffPregroupoid : Pregroupoid H where
     simp only [mfld_simps] at hy1 ⊢
     rw [fg _ hy1]
 
+variable (n I) in
 /-- 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 (contDiffPregroupoid n I)
 
-variable {n}
-
 /-- Inclusion of the groupoid of `C^n` local diffeos in the groupoid of `C^m` local diffeos when
 `m ≤ n` -/
 theorem contDiffGroupoid_le (h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGroupoid m I := by
@@ -570,8 +568,6 @@ theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H :
   · refine I.continuous.comp_continuousOn (u.symm.continuousOn.comp I.continuousOn_symm ?_)
     exact (mapsTo_preimage _ _).mono_left inter_subset_left
 
-variable (n)
-
 /-- An identity partial homeomorphism belongs to the `C^n` groupoid. -/
 theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
     PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I := by
@@ -587,7 +583,7 @@ theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) :
     e.symm.trans e ∈ contDiffGroupoid n I :=
   haveI : e.symm.trans e ≈ PartialHomeomorph.ofSet e.target e.open_target :=
     PartialHomeomorph.symm_trans_self _
-  StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_contDiffGroupoid n I e.open_target) this
+  StructureGroupoid.mem_of_eqOnSource _ (ofSet_mem_contDiffGroupoid e.open_target) this
 
 variable {E' H' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
 
@@ -616,7 +612,7 @@ instance : ClosedUnderRestriction (contDiffGroupoid n I) :=
       rw [StructureGroupoid.le_iff]
       rintro e ⟨s, hs, hes⟩
       apply (contDiffGroupoid n I).mem_of_eqOnSource' _ _ _ hes
-      exact ofSet_mem_contDiffGroupoid n I hs)
+      exact ofSet_mem_contDiffGroupoid hs)
 
 end contDiffGroupoid
 
@@ -670,7 +666,7 @@ model with corners `I`. -/
 def maximalAtlas :=
   (contDiffGroupoid ∞ I).maximalAtlas M
 
-variable {M}
+variable {I M}
 
 theorem subset_maximalAtlas [SmoothManifoldWithCorners I M] : atlas H M ⊆ maximalAtlas I M :=
   StructureGroupoid.subset_maximalAtlas _
@@ -679,8 +675,6 @@ theorem chart_mem_maximalAtlas [SmoothManifoldWithCorners I M] (x : M) :
     chartAt H x ∈ maximalAtlas I M :=
   StructureGroupoid.chart_mem_maximalAtlas _ x
 
-variable {I}
-
 theorem compatible_of_mem_maximalAtlas {e e' : PartialHomeomorph M H} (he : e ∈ maximalAtlas I M)
     (he' : e' ∈ maximalAtlas I M) : e.symm.trans e' ∈ contDiffGroupoid ∞ I :=
   StructureGroupoid.compatible_of_mem_maximalAtlas he he'
@@ -721,7 +715,7 @@ end SmoothManifoldWithCorners
 
 theorem PartialHomeomorph.singleton_smoothManifoldWithCorners
     {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-    {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
+    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
     {M : Type*} [TopologicalSpace M] (e : PartialHomeomorph M H) (h : e.source = Set.univ) :
     @SmoothManifoldWithCorners 𝕜 _ E _ _ H _ I M _ (e.singletonChartedSpace h) :=
   @SmoothManifoldWithCorners.mk' _ _ _ _ _ _ _ _ _ _ (id _) <|
@@ -729,10 +723,10 @@ theorem PartialHomeomorph.singleton_smoothManifoldWithCorners
 
 theorem IsOpenEmbedding.singleton_smoothManifoldWithCorners {𝕜 : Type*} [NontriviallyNormedField 𝕜]
     {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H]
-    (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [Nonempty M] {f : M → H}
+    {I : ModelWithCorners 𝕜 E H} {M : Type*} [TopologicalSpace M] [Nonempty M] {f : M → H}
     (h : IsOpenEmbedding f) :
     @SmoothManifoldWithCorners 𝕜 _ E _ _ H _ I M _ h.singletonChartedSpace :=
-  (h.toPartialHomeomorph f).singleton_smoothManifoldWithCorners I (by simp)
+  (h.toPartialHomeomorph f).singleton_smoothManifoldWithCorners (by simp)
 
 @[deprecated (since := "2024-10-18")]
 alias OpenEmbedding.singleton_smoothManifoldWithCorners :=
@@ -743,7 +737,7 @@ namespace TopologicalSpace.Opens
 open TopologicalSpace
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*}
+  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type*}
   [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] (s : Opens M)
 
 instance : SmoothManifoldWithCorners I s :=
@@ -757,8 +751,8 @@ open scoped Topology
 
 variable {𝕜 E M H E' M' H' : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] [TopologicalSpace H] [TopologicalSpace M] (f f' : PartialHomeomorph M H)
-  (I : ModelWithCorners 𝕜 E H) [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
-  [TopologicalSpace M'] (I' : ModelWithCorners 𝕜 E' H') {s t : Set M}
+  {I : ModelWithCorners 𝕜 E H} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
+  [TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s t : Set M}
 
 /-!
 ### Extended charts
@@ -772,6 +766,7 @@ as `PartialEquiv`.
 
 namespace PartialHomeomorph
 
+variable (I) in
 /-- Given a chart `f` on a manifold with corners, `f.extend I` is the extended chart to the model
 vector space. -/
 @[simp, mfld_simps]
@@ -812,13 +807,13 @@ theorem extend_left_inv {x : M} (hxf : x ∈ f.source) : (f.extend I).symm (f.ex
 
 /-- Variant of `f.extend_left_inv I`, stated in terms of images. -/
 lemma extend_left_inv' (ht : t ⊆ f.source) : ((f.extend I).symm ∘ (f.extend I)) '' t = t :=
-  EqOn.image_eq_self (fun _ hx ↦ f.extend_left_inv I (ht hx))
+  EqOn.image_eq_self (fun _ hx ↦ f.extend_left_inv (ht hx))
 
 theorem extend_source_mem_nhds {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝 x :=
-  (isOpen_extend_source f I).mem_nhds <| by rwa [f.extend_source I]
+  (isOpen_extend_source f).mem_nhds <| by rwa [f.extend_source]
 
 theorem extend_source_mem_nhdsWithin {x : M} (h : x ∈ f.source) : (f.extend I).source ∈ 𝓝[s] x :=
-  mem_nhdsWithin_of_mem_nhds <| extend_source_mem_nhds f I h
+  mem_nhdsWithin_of_mem_nhds <| extend_source_mem_nhds f h
 
 theorem continuousOn_extend : ContinuousOn (f.extend I) (f.extend I).source := by
   refine I.continuous.comp_continuousOn ?_
@@ -826,7 +821,7 @@ theorem continuousOn_extend : ContinuousOn (f.extend I) (f.extend I).source := b
   exact f.continuousOn
 
 theorem continuousAt_extend {x : M} (h : x ∈ f.source) : ContinuousAt (f.extend I) x :=
-  (continuousOn_extend f I).continuousAt <| extend_source_mem_nhds f I h
+  (continuousOn_extend f).continuousAt <| extend_source_mem_nhds f h
 
 theorem map_extend_nhds {x : M} (hy : x ∈ f.source) :
     map (f.extend I) (𝓝 x) = 𝓝[range I] f.extend I x := by
@@ -834,16 +829,16 @@ theorem map_extend_nhds {x : M} (hy : x ∈ f.source) :
 
 theorem map_extend_nhds_of_boundaryless [I.Boundaryless] {x : M} (hx : x ∈ f.source) :
     map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x) := by
-  rw [f.map_extend_nhds _ hx, I.range_eq_univ, nhdsWithin_univ]
+  rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_univ]
 
 theorem extend_target_mem_nhdsWithin {y : M} (hy : y ∈ f.source) :
     (f.extend I).target ∈ 𝓝[range I] f.extend I y := by
-  rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f I hy]
-  exact image_mem_map (extend_source_mem_nhds _ _ hy)
+  rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f hy]
+  exact image_mem_map (extend_source_mem_nhds _ hy)
 
 theorem extend_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless] {x} (hx : x ∈ f.source)
     {s : Set M} (h : s ∈ 𝓝 x) : (f.extend I) '' s ∈ 𝓝 ((f.extend I) x) := by
-  rw [← f.map_extend_nhds_of_boundaryless _ hx, Filter.mem_map]
+  rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_map]
   filter_upwards [h] using subset_preimage_image (f.extend I) s
 
 theorem extend_target_subset_range : (f.extend I).target ⊆ range I := by simp only [mfld_simps]
@@ -863,8 +858,8 @@ lemma mem_interior_extend_target {y : H} (hy : y ∈ f.target)
 
 theorem nhdsWithin_extend_target_eq {y : M} (hy : y ∈ f.source) :
     𝓝[(f.extend I).target] f.extend I y = 𝓝[range I] f.extend I y :=
-  (nhdsWithin_mono _ (extend_target_subset_range _ _)).antisymm <|
-    nhdsWithin_le_of_mem (extend_target_mem_nhdsWithin _ _ hy)
+  (nhdsWithin_mono _ (extend_target_subset_range _)).antisymm <|
+    nhdsWithin_le_of_mem (extend_target_mem_nhdsWithin _ hy)
 
 theorem continuousAt_extend_symm' {x : E} (h : x ∈ (f.extend I).target) :
     ContinuousAt (f.extend I).symm x :=
@@ -872,10 +867,10 @@ theorem continuousAt_extend_symm' {x : E} (h : x ∈ (f.extend I).target) :
 
 theorem continuousAt_extend_symm {x : M} (h : x ∈ f.source) :
     ContinuousAt (f.extend I).symm (f.extend I x) :=
-  continuousAt_extend_symm' f I <| (f.extend I).map_source <| by rwa [f.extend_source]
+  continuousAt_extend_symm' f <| (f.extend I).map_source <| by rwa [f.extend_source]
 
 theorem continuousOn_extend_symm : ContinuousOn (f.extend I).symm (f.extend I).target := fun _ h =>
-  (continuousAt_extend_symm' _ _ h).continuousWithinAt
+  (continuousAt_extend_symm' _ h).continuousWithinAt
 
 theorem extend_symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {g : M → X}
     {s : Set M} {x : M} :
@@ -885,52 +880,52 @@ theorem extend_symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {
 
 theorem isOpen_extend_preimage' {s : Set E} (hs : IsOpen s) :
     IsOpen ((f.extend I).source ∩ f.extend I ⁻¹' s) :=
-  (continuousOn_extend f I).isOpen_inter_preimage (isOpen_extend_source _ _) hs
+  (continuousOn_extend f).isOpen_inter_preimage (isOpen_extend_source _) hs
 
 theorem isOpen_extend_preimage {s : Set E} (hs : IsOpen s) :
     IsOpen (f.source ∩ f.extend I ⁻¹' s) := by
-  rw [← extend_source f I]; exact isOpen_extend_preimage' f I hs
+  rw [← extend_source f (I := I)]; exact isOpen_extend_preimage' f hs
 
 theorem map_extend_nhdsWithin_eq_image {y : M} (hy : y ∈ f.source) :
     map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' ((f.extend I).source ∩ s)] f.extend I y := by
   set e := f.extend I
   calc
     map e (𝓝[s] y) = map e (𝓝[e.source ∩ s] y) :=
-      congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f I hy)).symm
+      congr_arg (map e) (nhdsWithin_inter_of_mem (extend_source_mem_nhdsWithin f hy)).symm
     _ = 𝓝[e '' (e.source ∩ s)] e y :=
       ((f.extend I).leftInvOn.mono inter_subset_left).map_nhdsWithin_eq
         ((f.extend I).left_inv <| by rwa [f.extend_source])
-        (continuousAt_extend_symm f I hy).continuousWithinAt
-        (continuousAt_extend f I hy).continuousWithinAt
+        (continuousAt_extend_symm f hy).continuousWithinAt
+        (continuousAt_extend f hy).continuousWithinAt
 
 theorem map_extend_nhdsWithin_eq_image_of_subset {y : M} (hy : y ∈ f.source) (hs : s ⊆ f.source) :
     map (f.extend I) (𝓝[s] y) = 𝓝[f.extend I '' s] f.extend I y := by
-  rw [map_extend_nhdsWithin_eq_image _ _ hy, inter_eq_self_of_subset_right]
+  rw [map_extend_nhdsWithin_eq_image _ hy, inter_eq_self_of_subset_right]
   rwa [extend_source]
 
 theorem map_extend_nhdsWithin {y : M} (hy : y ∈ f.source) :
     map (f.extend I) (𝓝[s] y) = 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y := by
-  rw [map_extend_nhdsWithin_eq_image f I hy, nhdsWithin_inter, ←
-    nhdsWithin_extend_target_eq _ _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
+  rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
+    nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
     inter_comm]
 
 theorem map_extend_symm_nhdsWithin {y : M} (hy : y ∈ f.source) :
     map (f.extend I).symm (𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y) = 𝓝[s] y := by
-  rw [← map_extend_nhdsWithin f I hy, map_map, Filter.map_congr, map_id]
-  exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ _ hy)
+  rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]
+  exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)
 
 theorem map_extend_symm_nhdsWithin_range {y : M} (hy : y ∈ f.source) :
     map (f.extend I).symm (𝓝[range I] f.extend I y) = 𝓝 y := by
-  rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f I hy, preimage_univ, univ_inter]
+  rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]
 
 theorem tendsto_extend_comp_iff {α : Type*} {l : Filter α} {g : α → M}
     (hg : ∀ᶠ z in l, g z ∈ f.source) {y : M} (hy : y ∈ f.source) :
     Tendsto (f.extend I ∘ g) l (𝓝 (f.extend I y)) ↔ Tendsto g l (𝓝 y) := by
-  refine ⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ _ hy).tendsto.comp⟩
-  have := (f.continuousAt_extend_symm I hy).tendsto.comp h
-  rw [extend_left_inv _ _ hy] at this
+  refine ⟨fun h u hu ↦ mem_map.2 ?_, (continuousAt_extend _ hy).tendsto.comp⟩
+  have := (f.continuousAt_extend_symm hy).tendsto.comp h
+  rw [extend_left_inv _ hy] at this
   filter_upwards [hg, mem_map.1 (this hu)] with z hz hzu
-  simpa only [(· ∘ ·), extend_left_inv _ _ hz, mem_preimage] using hzu
+  simpa only [(· ∘ ·), extend_left_inv _ hz, mem_preimage] using hzu
 
 -- there is no definition `writtenInExtend` but we already use some made-up names in this file
 theorem continuousWithinAt_writtenInExtend_iff {f' : PartialHomeomorph M' H'} {g : M → M'} {y : M}
@@ -939,11 +934,11 @@ theorem continuousWithinAt_writtenInExtend_iff {f' : PartialHomeomorph M' H'} {g
       ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I y) ↔ ContinuousWithinAt g s y := by
   unfold ContinuousWithinAt
   simp only [comp_apply]
-  rw [extend_left_inv _ _ hy, f'.tendsto_extend_comp_iff _ _ hgy,
-    ← f.map_extend_symm_nhdsWithin I hy, tendsto_map'_iff]
-  rw [← f.map_extend_nhdsWithin I hy, eventually_map]
+  rw [extend_left_inv _ hy, f'.tendsto_extend_comp_iff _ hgy,
+    ← f.map_extend_symm_nhdsWithin (I := I) hy, tendsto_map'_iff]
+  rw [← f.map_extend_nhdsWithin (I := I) hy, eventually_map]
   filter_upwards [inter_mem_nhdsWithin _ (f.open_source.mem_nhds hy)] with z hz
-  rw [comp_apply, extend_left_inv _ _ hz.2]
+  rw [comp_apply, extend_left_inv _ hz.2]
   exact hmaps hz.1
 
 -- there is no definition `writtenInExtend` but we already use some made-up names in this file
@@ -955,7 +950,7 @@ theorem continuousOn_writtenInExtend_iff {f' : PartialHomeomorph M' H'} {g : M 
     ContinuousOn (f'.extend I' ∘ g ∘ (f.extend I).symm) (f.extend I '' s) ↔ ContinuousOn g s := by
   refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_
   refine (continuousWithinAt_congr_nhds ?_).trans
-    (continuousWithinAt_writtenInExtend_iff _ _ _ (hs hx) (hmaps hx) hmaps)
+    (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)
   rw [← map_extend_nhdsWithin_eq_image_of_subset, ← map_extend_nhdsWithin]
   exacts [hs hx, hs hx, hs]
 
@@ -963,11 +958,11 @@ theorem continuousOn_writtenInExtend_iff {f' : PartialHomeomorph M' H'} {g : M 
 in the source is a neighborhood of the preimage, within a set. -/
 theorem extend_preimage_mem_nhdsWithin {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
     (f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x := by
-  rwa [← map_extend_symm_nhdsWithin f I h, mem_map] at ht
+  rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht
 
 theorem extend_preimage_mem_nhds {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝 x) :
     (f.extend I).symm ⁻¹' t ∈ 𝓝 (f.extend I x) := by
-  apply (continuousAt_extend_symm f I h).preimage_mem_nhds
+  apply (continuousAt_extend_symm f h).preimage_mem_nhds
   rwa [(f.extend I).left_inv]
   rwa [f.extend_source]
 
@@ -994,8 +989,8 @@ theorem extend_symm_preimage_inter_range_eventuallyEq_aux {s : Set M} {x : M} (h
 theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs : s ⊆ f.source)
     (hx : x ∈ f.source) :
     ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)] f.extend I '' s := by
-  rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ _ hx,
-    map_extend_nhdsWithin_eq_image_of_subset _ _ hx hs]
+  rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx,
+    map_extend_nhdsWithin_eq_image_of_subset _ hx hs]
 
 /-! We use the name `extend_coord_change` for `(f'.extend I).symm ≫ f.extend I`. -/
 
@@ -1038,7 +1033,7 @@ theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtl
 theorem contDiffWithinAt_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I M)
     (hf' : f' ∈ maximalAtlas I M) {x : E} (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
     ContDiffWithinAt 𝕜 ⊤ (f.extend I ∘ (f'.extend I).symm) (range I) x := by
-  apply (contDiffOn_extend_coord_change I hf hf' x hx).mono_of_mem
+  apply (contDiffOn_extend_coord_change hf hf' x hx).mono_of_mem
   rw [extend_coord_change_source] at hx ⊢
   obtain ⟨z, hz, rfl⟩ := hx
   exact I.image_mem_nhdsWithin ((PartialHomeomorph.open_source _).mem_nhds hz)
@@ -1046,7 +1041,7 @@ theorem contDiffWithinAt_extend_coord_change [ChartedSpace H M] (hf : f ∈ maxi
 theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I M)
     (hf' : f' ∈ maximalAtlas I M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
     ContDiffWithinAt 𝕜 ⊤ (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x) := by
-  refine contDiffWithinAt_extend_coord_change I hf hf' ?_
+  refine contDiffWithinAt_extend_coord_change hf hf' ?_
   rw [← extend_image_source_inter]
   exact mem_image_of_mem _ ⟨hxf', hxf⟩
 
@@ -1056,6 +1051,7 @@ open PartialHomeomorph
 
 variable [ChartedSpace H M] [ChartedSpace H' M']
 
+variable (I) in
 /-- The preferred extended chart on a manifold with corners around a point `x`, from a neighborhood
 of `x` to the model vector space. -/
 @[simp, mfld_simps]
@@ -1068,21 +1064,23 @@ theorem extChartAt_coe (x : M) : ⇑(extChartAt I x) = I ∘ chartAt H x :=
 theorem extChartAt_coe_symm (x : M) : ⇑(extChartAt I x).symm = (chartAt H x).symm ∘ I.symm :=
   rfl
 
+variable (I) in
 theorem extChartAt_source (x : M) : (extChartAt I x).source = (chartAt H x).source :=
-  extend_source _ _
+  extend_source _
 
 theorem isOpen_extChartAt_source (x : M) : IsOpen (extChartAt I x).source :=
-  isOpen_extend_source _ _
+  isOpen_extend_source _
 
 theorem mem_extChartAt_source (x : M) : x ∈ (extChartAt I x).source := by
   simp only [extChartAt_source, mem_chart_source]
 
 theorem mem_extChartAt_target (x : M) : extChartAt I x x ∈ (extChartAt I x).target :=
-  (extChartAt I x).map_source <| mem_extChartAt_source _ _
+  (extChartAt I x).map_source <| mem_extChartAt_source _
 
+variable (I) in
 theorem extChartAt_target (x : M) :
     (extChartAt I x).target = I.symm ⁻¹' (chartAt H x).target ∩ range I :=
-  extend_target _ _
+  extend_target _
 
 theorem uniqueDiffOn_extChartAt_target (x : M) : UniqueDiffOn 𝕜 (extChartAt I x).target := by
   rw [extChartAt_target]
@@ -1090,64 +1088,64 @@ theorem uniqueDiffOn_extChartAt_target (x : M) : UniqueDiffOn 𝕜 (extChartAt I
 
 theorem uniqueDiffWithinAt_extChartAt_target (x : M) :
     UniqueDiffWithinAt 𝕜 (extChartAt I x).target (extChartAt I x x) :=
-  uniqueDiffOn_extChartAt_target I x _ <| mem_extChartAt_target I x
+  uniqueDiffOn_extChartAt_target x _ <| mem_extChartAt_target x
 
 theorem extChartAt_to_inv (x : M) : (extChartAt I x).symm ((extChartAt I x) x) = x :=
-  (extChartAt I x).left_inv (mem_extChartAt_source I x)
+  (extChartAt I x).left_inv (mem_extChartAt_source x)
 
 theorem mapsTo_extChartAt {x : M} (hs : s ⊆ (chartAt H x).source) :
     MapsTo (extChartAt I x) s ((extChartAt I x).symm ⁻¹' s ∩ range I) :=
-  mapsTo_extend _ _ hs
+  mapsTo_extend _ hs
 
 theorem extChartAt_source_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
     (extChartAt I x).source ∈ 𝓝 x' :=
-  extend_source_mem_nhds _ _ <| by rwa [← extChartAt_source I]
+  extend_source_mem_nhds _ <| by rwa [← extChartAt_source I]
 
 theorem extChartAt_source_mem_nhds (x : M) : (extChartAt I x).source ∈ 𝓝 x :=
-  extChartAt_source_mem_nhds' I (mem_extChartAt_source I x)
+  extChartAt_source_mem_nhds' (mem_extChartAt_source x)
 
 theorem extChartAt_source_mem_nhdsWithin' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
     (extChartAt I x).source ∈ 𝓝[s] x' :=
-  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds' I h)
+  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds' h)
 
 theorem extChartAt_source_mem_nhdsWithin (x : M) : (extChartAt I x).source ∈ 𝓝[s] x :=
-  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds I x)
+  mem_nhdsWithin_of_mem_nhds (extChartAt_source_mem_nhds x)
 
 theorem continuousOn_extChartAt (x : M) : ContinuousOn (extChartAt I x) (extChartAt I x).source :=
-  continuousOn_extend _ _
+  continuousOn_extend _
 
 theorem continuousAt_extChartAt' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
     ContinuousAt (extChartAt I x) x' :=
-  continuousAt_extend _ _ <| by rwa [← extChartAt_source I]
+  continuousAt_extend _ <| by rwa [← extChartAt_source I]
 
 theorem continuousAt_extChartAt (x : M) : ContinuousAt (extChartAt I x) x :=
-  continuousAt_extChartAt' _ (mem_extChartAt_source I x)
+  continuousAt_extChartAt' (mem_extChartAt_source x)
 
 theorem map_extChartAt_nhds' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     map (extChartAt I x) (𝓝 y) = 𝓝[range I] extChartAt I x y :=
-  map_extend_nhds _ _ <| by rwa [← extChartAt_source I]
+  map_extend_nhds _ <| by rwa [← extChartAt_source I]
 
 theorem map_extChartAt_nhds (x : M) : map (extChartAt I x) (𝓝 x) = 𝓝[range I] extChartAt I x x :=
-  map_extChartAt_nhds' I <| mem_extChartAt_source I x
+  map_extChartAt_nhds' <| mem_extChartAt_source x
 
 theorem map_extChartAt_nhds_of_boundaryless [I.Boundaryless] (x : M) :
     map (extChartAt I x) (𝓝 x) = 𝓝 (extChartAt I x x) := by
   rw [extChartAt]
-  exact map_extend_nhds_of_boundaryless (chartAt H x) I (mem_chart_source H x)
+  exact map_extend_nhds_of_boundaryless (chartAt H x) (mem_chart_source H x)
 
 variable {x} in
 theorem extChartAt_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless]
     {x : M} (hx : s ∈ 𝓝 x) : extChartAt I x '' s ∈ 𝓝 (extChartAt I x x) := by
   rw [extChartAt]
-  exact extend_image_nhd_mem_nhds_of_boundaryless _ I (mem_chart_source H x) hx
+  exact extend_image_nhd_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx
 
 theorem extChartAt_target_mem_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x y :=
-  extend_target_mem_nhdsWithin _ _ <| by rwa [← extChartAt_source I]
+  extend_target_mem_nhdsWithin _ <| by rwa [← extChartAt_source I]
 
 theorem extChartAt_target_mem_nhdsWithin (x : M) :
     (extChartAt I x).target ∈ 𝓝[range I] extChartAt I x x :=
-  extChartAt_target_mem_nhdsWithin' I (mem_extChartAt_source I x)
+  extChartAt_target_mem_nhdsWithin' (mem_extChartAt_source x)
 
 /-- If we're boundaryless, `extChartAt` has open target -/
 theorem isOpen_extChartAt_target [I.Boundaryless] (x : M) : IsOpen (extChartAt I x).target := by
@@ -1157,109 +1155,109 @@ theorem isOpen_extChartAt_target [I.Boundaryless] (x : M) : IsOpen (extChartAt I
 /-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of the key point -/
 theorem extChartAt_target_mem_nhds [I.Boundaryless] (x : M) :
     (extChartAt I x).target ∈ 𝓝 (extChartAt I x x) := by
-  convert extChartAt_target_mem_nhdsWithin I x
+  convert extChartAt_target_mem_nhdsWithin x
   simp only [I.range_eq_univ, nhdsWithin_univ]
 
 /-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of any of its points -/
 theorem extChartAt_target_mem_nhds' [I.Boundaryless] {x : M} {y : E}
     (m : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∈ 𝓝 y :=
-  (isOpen_extChartAt_target I x).mem_nhds m
+  (isOpen_extChartAt_target x).mem_nhds m
 
 theorem extChartAt_target_subset_range (x : M) : (extChartAt I x).target ⊆ range I := by
   simp only [mfld_simps]
 
 theorem nhdsWithin_extChartAt_target_eq' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y :=
-  nhdsWithin_extend_target_eq _ _ <| by rwa [← extChartAt_source I]
+  nhdsWithin_extend_target_eq _ <| by rwa [← extChartAt_source I]
 
 theorem nhdsWithin_extChartAt_target_eq (x : M) :
     𝓝[(extChartAt I x).target] (extChartAt I x) x = 𝓝[range I] (extChartAt I x) x :=
-  nhdsWithin_extChartAt_target_eq' I (mem_extChartAt_source I x)
+  nhdsWithin_extChartAt_target_eq' (mem_extChartAt_source x)
 
 theorem continuousAt_extChartAt_symm'' {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
     ContinuousAt (extChartAt I x).symm y :=
-  continuousAt_extend_symm' _ _ h
+  continuousAt_extend_symm' _ h
 
 theorem continuousAt_extChartAt_symm' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
     ContinuousAt (extChartAt I x).symm (extChartAt I x x') :=
-  continuousAt_extChartAt_symm'' I <| (extChartAt I x).map_source h
+  continuousAt_extChartAt_symm'' <| (extChartAt I x).map_source h
 
 theorem continuousAt_extChartAt_symm (x : M) :
     ContinuousAt (extChartAt I x).symm ((extChartAt I x) x) :=
-  continuousAt_extChartAt_symm' I (mem_extChartAt_source I x)
+  continuousAt_extChartAt_symm' (mem_extChartAt_source x)
 
 theorem continuousOn_extChartAt_symm (x : M) :
     ContinuousOn (extChartAt I x).symm (extChartAt I x).target :=
-  fun _y hy => (continuousAt_extChartAt_symm'' _ hy).continuousWithinAt
+  fun _y hy => (continuousAt_extChartAt_symm'' hy).continuousWithinAt
 
 theorem isOpen_extChartAt_preimage' (x : M) {s : Set E} (hs : IsOpen s) :
     IsOpen ((extChartAt I x).source ∩ extChartAt I x ⁻¹' s) :=
-  isOpen_extend_preimage' _ _ hs
+  isOpen_extend_preimage' _ hs
 
 theorem isOpen_extChartAt_preimage (x : M) {s : Set E} (hs : IsOpen s) :
     IsOpen ((chartAt H x).source ∩ extChartAt I x ⁻¹' s) := by
   rw [← extChartAt_source I]
-  exact isOpen_extChartAt_preimage' I x hs
+  exact isOpen_extChartAt_preimage' x hs
 
 theorem map_extChartAt_nhdsWithin_eq_image' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     map (extChartAt I x) (𝓝[s] y) =
       𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x y :=
-  map_extend_nhdsWithin_eq_image _ _ <| by rwa [← extChartAt_source I]
+  map_extend_nhdsWithin_eq_image _ <| by rwa [← extChartAt_source I]
 
 theorem map_extChartAt_nhdsWithin_eq_image (x : M) :
     map (extChartAt I x) (𝓝[s] x) =
       𝓝[extChartAt I x '' ((extChartAt I x).source ∩ s)] extChartAt I x x :=
-  map_extChartAt_nhdsWithin_eq_image' I (mem_extChartAt_source I x)
+  map_extChartAt_nhdsWithin_eq_image' (mem_extChartAt_source x)
 
 theorem map_extChartAt_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     map (extChartAt I x) (𝓝[s] y) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y :=
-  map_extend_nhdsWithin _ _ <| by rwa [← extChartAt_source I]
+  map_extend_nhdsWithin _ <| by rwa [← extChartAt_source I]
 
 theorem map_extChartAt_nhdsWithin (x : M) :
     map (extChartAt I x) (𝓝[s] x) = 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x :=
-  map_extChartAt_nhdsWithin' I (mem_extChartAt_source I x)
+  map_extChartAt_nhdsWithin' (mem_extChartAt_source x)
 
 theorem map_extChartAt_symm_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y) =
       𝓝[s] y :=
-  map_extend_symm_nhdsWithin _ _ <| by rwa [← extChartAt_source I]
+  map_extend_symm_nhdsWithin _ <| by rwa [← extChartAt_source I]
 
 theorem map_extChartAt_symm_nhdsWithin_range' {x y : M} (hy : y ∈ (extChartAt I x).source) :
     map (extChartAt I x).symm (𝓝[range I] extChartAt I x y) = 𝓝 y :=
-  map_extend_symm_nhdsWithin_range _ _ <| by rwa [← extChartAt_source I]
+  map_extend_symm_nhdsWithin_range _ <| by rwa [← extChartAt_source I]
 
 theorem map_extChartAt_symm_nhdsWithin (x : M) :
     map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x x) =
       𝓝[s] x :=
-  map_extChartAt_symm_nhdsWithin' I (mem_extChartAt_source I x)
+  map_extChartAt_symm_nhdsWithin' (mem_extChartAt_source x)
 
 theorem map_extChartAt_symm_nhdsWithin_range (x : M) :
     map (extChartAt I x).symm (𝓝[range I] extChartAt I x x) = 𝓝 x :=
-  map_extChartAt_symm_nhdsWithin_range' I (mem_extChartAt_source I x)
+  map_extChartAt_symm_nhdsWithin_range' (mem_extChartAt_source x)
 
 /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
 in the source is a neighborhood of the preimage, within a set. -/
 theorem extChartAt_preimage_mem_nhdsWithin' {x x' : M} (h : x' ∈ (extChartAt I x).source)
     (ht : t ∈ 𝓝[s] x') :
     (extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x' := by
-  rwa [← map_extChartAt_symm_nhdsWithin' I h, mem_map] at ht
+  rwa [← map_extChartAt_symm_nhdsWithin' h, mem_map] at ht
 
 /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of the
 base point is a neighborhood of the preimage, within a set. -/
 theorem extChartAt_preimage_mem_nhdsWithin {x : M} (ht : t ∈ 𝓝[s] x) :
     (extChartAt I x).symm ⁻¹' t ∈ 𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
-  extChartAt_preimage_mem_nhdsWithin' I (mem_extChartAt_source I x) ht
+  extChartAt_preimage_mem_nhdsWithin' (mem_extChartAt_source x) ht
 
 theorem extChartAt_preimage_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source)
     (ht : t ∈ 𝓝 x') : (extChartAt I x).symm ⁻¹' t ∈ 𝓝 (extChartAt I x x') :=
-  extend_preimage_mem_nhds _ _ (by rwa [← extChartAt_source I]) ht
+  extend_preimage_mem_nhds _ (by rwa [← extChartAt_source I]) ht
 
 /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
 is a neighborhood of the preimage. -/
 theorem extChartAt_preimage_mem_nhds {x : M} (ht : t ∈ 𝓝 x) :
     (extChartAt I x).symm ⁻¹' t ∈ 𝓝 ((extChartAt I x) x) := by
-  apply (continuousAt_extChartAt_symm I x).preimage_mem_nhds
-  rwa [(extChartAt I x).left_inv (mem_extChartAt_source _ _)]
+  apply (continuousAt_extChartAt_symm x).preimage_mem_nhds
+  rwa [(extChartAt I x).left_inv (mem_extChartAt_source _)]
 
 /-- Technical lemma to rewrite suitably the preimage of an intersection under an extended chart, to
 bring it into a convenient form to apply derivative lemmas. -/
@@ -1275,28 +1273,29 @@ theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range
         (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] (extChartAt I x x) := by
   rw [← (extChartAt I x).image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image,
     ← map_extChartAt_nhdsWithin, nhdsWithin_inter_of_mem']
-  exact hc (extChartAt_source_mem_nhds _ _)
+  exact hc (extChartAt_source_mem_nhds _)
 
 /-! We use the name `ext_coord_change` for `(extChartAt I x').symm ≫ extChartAt I x`. -/
 
 theorem ext_coord_change_source (x x' : M) :
     ((extChartAt I x').symm ≫ extChartAt I x).source =
       I '' ((chartAt H x').symm ≫ₕ chartAt H x).source :=
-  extend_coord_change_source _ _ _
+  extend_coord_change_source _ _
 
 open SmoothManifoldWithCorners
 
 theorem contDiffOn_ext_coord_change [SmoothManifoldWithCorners I M] (x x' : M) :
     ContDiffOn 𝕜 ⊤ (extChartAt I x ∘ (extChartAt I x').symm)
       ((extChartAt I x').symm ≫ extChartAt I x).source :=
-  contDiffOn_extend_coord_change I (chart_mem_maximalAtlas I x) (chart_mem_maximalAtlas I x')
+  contDiffOn_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x')
 
 theorem contDiffWithinAt_ext_coord_change [SmoothManifoldWithCorners I M] (x x' : M) {y : E}
     (hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source) :
     ContDiffWithinAt 𝕜 ⊤ (extChartAt I x ∘ (extChartAt I x').symm) (range I) y :=
-  contDiffWithinAt_extend_coord_change I (chart_mem_maximalAtlas I x) (chart_mem_maximalAtlas I x')
+  contDiffWithinAt_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x')
     hy
 
+variable (I I') in
 /-- Conjugating a function to write it in the preferred charts around `x`.
 The manifold derivative of `f` will just be the derivative of this conjugated function. -/
 @[simp, mfld_simps]
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
index 02abb186cc8f9..001e1a6509395 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
@@ -122,7 +122,7 @@ section
 variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
   [TopologicalSpace (TotalSpace F E)] [∀ x, TopologicalSpace (E x)] {EB : Type*}
   [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type*} [TopologicalSpace HB]
-  (IB : ModelWithCorners 𝕜 EB HB) (E' : B → Type*) [∀ x, Zero (E' x)] {EM : Type*}
+  {IB : ModelWithCorners 𝕜 EB HB} (E' : B → Type*) [∀ x, Zero (E' x)] {EM : Type*}
   [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type*} [TopologicalSpace HM]
   {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M]
   {n : ℕ∞}
@@ -149,13 +149,13 @@ theorem FiberBundle.writtenInExtChartAt_trivializationAt {x : TotalSpace F E} {y
     (hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target) :
     writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) x
       (trivializationAt F E x.proj) y = y :=
-  writtenInExtChartAt_chartAt_comp _ _ hy
+  writtenInExtChartAt_chartAt_comp _ hy
 
 theorem FiberBundle.writtenInExtChartAt_trivializationAt_symm {x : TotalSpace F E} {y}
     (hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target) :
     writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (trivializationAt F E x.proj x)
       (trivializationAt F E x.proj).toPartialHomeomorph.symm y = y :=
-  writtenInExtChartAt_chartAt_symm_comp _ _ hy
+  writtenInExtChartAt_chartAt_symm_comp _ hy
 
 /-! ### Smoothness of maps in/out fiber bundles
 
@@ -165,8 +165,6 @@ bundle at all, just that it is a fiber bundle over a charted base space.
 
 namespace Bundle
 
-variable {IB}
-
 /-- Characterization of C^n functions into a smooth vector bundle. -/
 theorem contMDiffWithinAt_totalSpace (f : M → TotalSpace F E) {s : Set M} {x₀ : M} :
     ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔
@@ -251,7 +249,7 @@ end
 
 
 variable [NontriviallyNormedField 𝕜] {EB : Type*} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
-  {HB : Type*} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B]
+  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B]
   [ChartedSpace HB B] {EM : Type*} [NormedAddCommGroup EM]
   [NormedSpace 𝕜 EM] {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
   [TopologicalSpace M] [ChartedSpace HM M] {n : ℕ∞}
@@ -262,6 +260,7 @@ section WithTopology
 variable [TopologicalSpace (TotalSpace F E)] [∀ x, TopologicalSpace (E x)] (F E)
 variable [FiberBundle F E] [VectorBundle 𝕜 F E]
 
+variable (IB) in
 /-- When `B` is a smooth manifold with corners with respect to a model `IB` and `E` is a
 topological vector bundle over `B` with fibers isomorphic to `F`, then `SmoothVectorBundle F E IB`
 registers that the bundle is smooth, in the sense of having smooth transition functions.
@@ -294,31 +293,30 @@ theorem smoothOn_symm_coordChangeL :
 theorem contMDiffOn_coordChangeL :
     ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F))
       (e.baseSet ∩ e'.baseSet) :=
-  (smoothOn_coordChangeL IB e e').of_le le_top
+  (smoothOn_coordChangeL e e').of_le le_top
 
 theorem contMDiffOn_symm_coordChangeL :
     ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => ((e.coordChangeL 𝕜 e' b).symm : F →L[𝕜] F))
       (e.baseSet ∩ e'.baseSet) :=
-  (smoothOn_symm_coordChangeL IB e e').of_le le_top
+  (smoothOn_symm_coordChangeL e e').of_le le_top
 
 variable {e e'}
 
 theorem contMDiffAt_coordChangeL {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) :
     ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x :=
-  (contMDiffOn_coordChangeL IB e e').contMDiffAt <|
+  (contMDiffOn_coordChangeL e e').contMDiffAt <|
     (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨h, h'⟩
 
 theorem smoothAt_coordChangeL {x : B} (h : x ∈ e.baseSet) (h' : x ∈ e'.baseSet) :
     SmoothAt IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x :=
-  contMDiffAt_coordChangeL IB h h'
+  contMDiffAt_coordChangeL h h'
 
-variable {IB}
 variable {s : Set M} {f : M → B} {g : M → F} {x : M}
 
 protected theorem ContMDiffWithinAt.coordChangeL
     (hf : ContMDiffWithinAt IM IB n f s x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
     ContMDiffWithinAt IM 𝓘(𝕜, F →L[𝕜] F) n (fun y ↦ (e.coordChangeL 𝕜 e' (f y) : F →L[𝕜] F)) s x :=
-  (contMDiffAt_coordChangeL IB he he').comp_contMDiffWithinAt _ hf
+  (contMDiffAt_coordChangeL he he').comp_contMDiffWithinAt _ hf
 
 protected nonrec theorem ContMDiffAt.coordChangeL
     (hf : ContMDiffAt IM IB n f x) (he : f x ∈ e.baseSet) (he' : f x ∈ e'.baseSet) :
@@ -454,8 +452,8 @@ instance SmoothFiberwiseLinear.hasGroupoid :
     haveI : MemTrivializationAtlas e := ⟨he⟩
     haveI : MemTrivializationAtlas e' := ⟨he'⟩
     rw [mem_smoothFiberwiseLinear_iff]
-    refine ⟨_, _, e.open_baseSet.inter e'.open_baseSet, smoothOn_coordChangeL IB e e',
-      smoothOn_symm_coordChangeL IB e e', ?_⟩
+    refine ⟨_, _, e.open_baseSet.inter e'.open_baseSet, smoothOn_coordChangeL e e',
+      smoothOn_symm_coordChangeL e e', ?_⟩
     refine PartialHomeomorph.eqOnSourceSetoid.symm ⟨?_, ?_⟩
     · simp only [e.symm_trans_source_eq e', FiberwiseLinear.partialHomeomorph, trans_toPartialEquiv,
         symm_toPartialEquiv]
@@ -497,7 +495,7 @@ theorem Trivialization.contMDiffAt_iff {f : M → TotalSpace F E} {x₀ : M} (he
     ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
       ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧
       ContMDiffAt IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) x₀ :=
-  e.contMDiffWithinAt_iff _ he
+  e.contMDiffWithinAt_iff he
 
 theorem Trivialization.contMDiffOn_iff {f : M → TotalSpace F E} {s : Set M}
     (he : MapsTo f s e.source) :
@@ -505,46 +503,46 @@ theorem Trivialization.contMDiffOn_iff {f : M → TotalSpace F E} {s : Set M}
       ContMDiffOn IM IB n (fun x => (f x).proj) s ∧
       ContMDiffOn IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) s := by
   simp only [ContMDiffOn, ← forall_and]
-  exact forall₂_congr fun x hx ↦ e.contMDiffWithinAt_iff IB (he hx)
+  exact forall₂_congr fun x hx ↦ e.contMDiffWithinAt_iff (he hx)
 
 theorem Trivialization.contMDiff_iff {f : M → TotalSpace F E} (he : ∀ x, f x ∈ e.source) :
     ContMDiff IM (IB.prod 𝓘(𝕜, F)) n f ↔
       ContMDiff IM IB n (fun x => (f x).proj) ∧
       ContMDiff IM 𝓘(𝕜, F) n (fun x ↦ (e (f x)).2) :=
-  (forall_congr' fun x ↦ e.contMDiffAt_iff IB (he x)).trans forall_and
+  (forall_congr' fun x ↦ e.contMDiffAt_iff (he x)).trans forall_and
 
 theorem Trivialization.smoothWithinAt_iff {f : M → TotalSpace F E} {s : Set M} {x₀ : M}
     (he : f x₀ ∈ e.source) :
     SmoothWithinAt IM (IB.prod 𝓘(𝕜, F)) f s x₀ ↔
       SmoothWithinAt IM IB (fun x => (f x).proj) s x₀ ∧
       SmoothWithinAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) s x₀ :=
-  e.contMDiffWithinAt_iff IB he
+  e.contMDiffWithinAt_iff he
 
 theorem Trivialization.smoothAt_iff {f : M → TotalSpace F E} {x₀ : M} (he : f x₀ ∈ e.source) :
     SmoothAt IM (IB.prod 𝓘(𝕜, F)) f x₀ ↔
       SmoothAt IM IB (fun x => (f x).proj) x₀ ∧ SmoothAt IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) x₀ :=
-  e.contMDiffAt_iff IB he
+  e.contMDiffAt_iff he
 
 theorem Trivialization.smoothOn_iff {f : M → TotalSpace F E} {s : Set M}
     (he : MapsTo f s e.source) :
     SmoothOn IM (IB.prod 𝓘(𝕜, F)) f s ↔
       SmoothOn IM IB (fun x => (f x).proj) s ∧ SmoothOn IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) s :=
-  e.contMDiffOn_iff IB he
+  e.contMDiffOn_iff he
 
 theorem Trivialization.smooth_iff {f : M → TotalSpace F E} (he : ∀ x, f x ∈ e.source) :
     Smooth IM (IB.prod 𝓘(𝕜, F)) f ↔
       Smooth IM IB (fun x => (f x).proj) ∧ Smooth IM 𝓘(𝕜, F) (fun x ↦ (e (f x)).2) :=
-  e.contMDiff_iff IB he
+  e.contMDiff_iff he
 
 theorem Trivialization.smoothOn (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
     SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) e e.source := by
   have : SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) id e.source := smoothOn_id
-  rw [e.smoothOn_iff IB (mapsTo_id _)] at this
+  rw [e.smoothOn_iff (mapsTo_id _)] at this
   exact (this.1.prod_mk this.2).congr fun x hx ↦ (e.mk_proj_snd hx).symm
 
 theorem Trivialization.smoothOn_symm (e : Trivialization F (π F E)) [MemTrivializationAtlas e] :
     SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) e.toPartialHomeomorph.symm e.target := by
-  rw [e.smoothOn_iff IB e.toPartialHomeomorph.symm_mapsTo]
+  rw [e.smoothOn_iff e.toPartialHomeomorph.symm_mapsTo]
   refine ⟨smoothOn_fst.congr fun x hx ↦ e.proj_symm_apply hx, smoothOn_snd.congr fun x hx ↦ ?_⟩
   rw [e.apply_symm_apply hx]
 
@@ -614,10 +612,10 @@ instance Bundle.Prod.smoothVectorBundle : SmoothVectorBundle (F₁ × F₂) (E
     rw [SmoothOn]
     refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')
     refine ContMDiffOn.clm_prodMap ?_ ?_
-    · refine (smoothOn_coordChangeL IB e₁ e₁').mono ?_
+    · refine (smoothOn_coordChangeL e₁ e₁').mono ?_
       simp only [Trivialization.baseSet_prod, mfld_simps]
       mfld_set_tac
-    · refine (smoothOn_coordChangeL IB e₂ e₂').mono ?_
+    · refine (smoothOn_coordChangeL e₂ e₂').mono ?_
       simp only [Trivialization.baseSet_prod, mfld_simps]
       mfld_set_tac
 
@@ -631,6 +629,7 @@ namespace VectorPrebundle
 
 variable [∀ x, TopologicalSpace (E x)]
 
+variable (IB) in
 /-- Mixin for a `VectorPrebundle` stating smoothness of coordinate changes. -/
 class IsSmooth (a : VectorPrebundle 𝕜 F E) : Prop where
   exists_smoothCoordChange :
@@ -642,6 +641,7 @@ class IsSmooth (a : VectorPrebundle 𝕜 F E) : Prop where
 
 variable (a : VectorPrebundle 𝕜 F E) [ha : a.IsSmooth IB] {e e' : Pretrivialization F (π F E)}
 
+variable (IB) in
 /-- A randomly chosen coordinate change on a `SmoothVectorPrebundle`, given by
   the field `exists_coordChange`. Note that `a.smoothCoordChange` need not be the same as
   `a.coordChange`. -/
@@ -649,8 +649,6 @@ noncomputable def smoothCoordChange (he : e ∈ a.pretrivializationAtlas)
     (he' : e' ∈ a.pretrivializationAtlas) (b : B) : F →L[𝕜] F :=
   Classical.choose (ha.exists_smoothCoordChange e he e' he') b
 
-variable {IB}
-
 theorem smoothOn_smoothCoordChange (he : e ∈ a.pretrivializationAtlas)
     (he' : e' ∈ a.pretrivializationAtlas) :
     SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (a.smoothCoordChange IB he he') (e.baseSet ∩ e'.baseSet) :=
@@ -669,7 +667,7 @@ theorem mk_smoothCoordChange (he : e ∈ a.pretrivializationAtlas)
     rw [e.proj_symm_apply' hb.1]; exact hb.2
   · exact a.smoothCoordChange_apply he he' hb v
 
-variable (IB)
+variable (IB) in
 /-- Make a `SmoothVectorBundle` from a `SmoothVectorPrebundle`. -/
 theorem smoothVectorBundle : @SmoothVectorBundle
     _ _ F E _ _ _ _ _ _ IB _ _ _ _ _ _ a.totalSpaceTopology _ a.toFiberBundle a.toVectorBundle :=
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean b/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
index 33808cd26cd8e..6708e0a288ed6 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Hom.lean
@@ -29,7 +29,7 @@ variable {𝕜 B F₁ F₂ M : Type*} {E₁ : B → Type*} {E₂ : B → Type*}
   [TopologicalSpace (TotalSpace F₂ E₂)] [∀ x, TopologicalSpace (E₂ x)]
   {EB : Type*}
   [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type*} [TopologicalSpace HB]
-  (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type*}
+  {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] {EM : Type*}
   [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type*} [TopologicalSpace HM]
   {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M]
   {n : ℕ∞} [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁]
@@ -45,8 +45,8 @@ theorem smoothOn_continuousLinearMapCoordChange
     SmoothOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂)
       (continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
       (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)) := by
-  have h₁ := smoothOn_coordChangeL IB e₁' e₁
-  have h₂ := smoothOn_coordChangeL IB e₂ e₂'
+  have h₁ := smoothOn_coordChangeL (IB := IB) e₁' e₁
+  have h₂ := smoothOn_coordChangeL (IB := IB) e₂ e₂'
   refine (h₁.mono ?_).cle_arrowCongr (h₂.mono ?_) <;> mfld_set_tac
 
 variable [∀ x, TopologicalAddGroup (E₂ x)] [∀ x, ContinuousSMul 𝕜 (E₂ x)]
@@ -58,8 +58,6 @@ theorem hom_chart (y₀ y : LE₁E₂) :
     Trivialization.coe_coe, PartialHomeomorph.refl_apply, Function.id_def,
     hom_trivializationAt_apply]
 
-variable {IB}
-
 theorem contMDiffAt_hom_bundle (f : M → LE₁E₂) {x₀ : M} {n : ℕ∞} :
     ContMDiffAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n f x₀ ↔
       ContMDiffAt IM IB n (fun x => (f x).1) x₀ ∧
@@ -81,7 +79,7 @@ instance Bundle.ContinuousLinearMap.vectorPrebundle.isSmooth :
   exists_smoothCoordChange := by
     rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
     exact ⟨continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂',
-      smoothOn_continuousLinearMapCoordChange IB,
+      smoothOn_continuousLinearMapCoordChange,
       continuousLinearMapCoordChange_apply (RingHom.id 𝕜) e₁ e₁' e₂ e₂'⟩
 
 instance SmoothVectorBundle.continuousLinearMap :
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean b/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean
index 30454293a1bd9..3671bb2677dac 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Pullback.lean
@@ -24,7 +24,7 @@ variable {𝕜 B B' M : Type*} (F : Type*) (E : B → Type*)
 variable [NontriviallyNormedField 𝕜] [∀ x, AddCommMonoid (E x)] [∀ x, Module 𝕜 (E x)]
   [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F E)]
   [∀ x, TopologicalSpace (E x)] {EB : Type*} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
-  {HB : Type*} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B]
+  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B]
   [ChartedSpace HB B] [SmoothManifoldWithCorners IB B] {EB' : Type*} [NormedAddCommGroup EB']
   [NormedSpace 𝕜 EB'] {HB' : Type*} [TopologicalSpace HB'] (IB' : ModelWithCorners 𝕜 EB' HB')
   [TopologicalSpace B'] [ChartedSpace HB' B'] [SmoothManifoldWithCorners IB' B'] [FiberBundle F E]
@@ -35,7 +35,7 @@ vector bundle `f *ᵖ E` is a smooth vector bundle. -/
 instance SmoothVectorBundle.pullback : SmoothVectorBundle F (f *ᵖ E) IB' where
   smoothOn_coordChangeL := by
     rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
-    refine ((smoothOn_coordChangeL _ e e').comp f.smooth.smoothOn fun b hb => hb).congr ?_
+    refine ((smoothOn_coordChangeL e e').comp f.smooth.smoothOn fun b hb => hb).congr ?_
     rintro b (hb : f b ∈ e.baseSet ∩ e'.baseSet); ext v
     show ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
     rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
index 7c85fe03db9fd..b7ae7412cc9d6 100644
--- a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
+++ b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
@@ -49,7 +49,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom
   [SmoothManifoldWithCorners I M] {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
   [SmoothManifoldWithCorners I' M'] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
-variable (I)
 
 /-- Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is
   smooth on its source. -/
@@ -60,14 +59,14 @@ theorem contDiffOn_fderiv_coord_change (i j : atlas H M) :
     rw [i.1.extend_coord_change_source]; apply image_subset_range
   intro x hx
   refine (ContDiffWithinAt.fderivWithin_right ?_ I.uniqueDiffOn le_top <| h hx).mono h
-  refine (PartialHomeomorph.contDiffOn_extend_coord_change I (subset_maximalAtlas I j.2)
-    (subset_maximalAtlas I i.2) x hx).mono_of_mem ?_
-  exact i.1.extend_coord_change_source_mem_nhdsWithin j.1 I hx
+  refine (PartialHomeomorph.contDiffOn_extend_coord_change (subset_maximalAtlas j.2)
+    (subset_maximalAtlas i.2) x hx).mono_of_mem ?_
+  exact i.1.extend_coord_change_source_mem_nhdsWithin j.1 hx
 
-variable (M)
 
 open SmoothManifoldWithCorners
 
+variable (I M) in
 /-- Let `M` be a smooth manifold with corners with model `I` on `(E, H)`.
 Then `tangentBundleCore I M` is the vector bundle core for the tangent bundle over `M`.
 It is indexed by the atlas of `M`, with fiber `E` and its change of coordinates from the chart `i`
@@ -89,35 +88,33 @@ def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M) where
     simp only
     rw [Filter.EventuallyEq.fderivWithin_eq, fderivWithin_id', ContinuousLinearMap.id_apply]
     · exact I.uniqueDiffWithinAt_image
-    · filter_upwards [i.1.extend_target_mem_nhdsWithin I hx] with y hy
+    · filter_upwards [i.1.extend_target_mem_nhdsWithin hx] with y hy
       exact (i.1.extend I).right_inv hy
-    · simp_rw [Function.comp_apply, i.1.extend_left_inv I hx]
+    · simp_rw [Function.comp_apply, i.1.extend_left_inv hx]
   continuousOn_coordChange i j := by
-    refine (contDiffOn_fderiv_coord_change I i j).continuousOn.comp
-      ((i.1.continuousOn_extend I).mono ?_) ?_
+    refine (contDiffOn_fderiv_coord_change i j).continuousOn.comp
+      (i.1.continuousOn_extend.mono ?_) ?_
     · rw [i.1.extend_source]; exact inter_subset_left
     simp_rw [← i.1.extend_image_source_inter, mapsTo_image]
   coordChange_comp := by
     rintro i j k x ⟨⟨hxi, hxj⟩, hxk⟩ v
     rw [fderivWithin_fderivWithin, Filter.EventuallyEq.fderivWithin_eq]
-    · have := i.1.extend_preimage_mem_nhds I hxi (j.1.extend_source_mem_nhds I hxj)
+    · have := i.1.extend_preimage_mem_nhds (I := I) hxi (j.1.extend_source_mem_nhds (I := I) hxj)
       filter_upwards [nhdsWithin_le_nhds this] with y hy
       simp_rw [Function.comp_apply, (j.1.extend I).left_inv hy]
-    · simp_rw [Function.comp_apply, i.1.extend_left_inv I hxi, j.1.extend_left_inv I hxj]
-    · exact (contDiffWithinAt_extend_coord_change' I (subset_maximalAtlas I k.2)
-        (subset_maximalAtlas I j.2) hxk hxj).differentiableWithinAt le_top
-    · exact (contDiffWithinAt_extend_coord_change' I (subset_maximalAtlas I j.2)
-        (subset_maximalAtlas I i.2) hxj hxi).differentiableWithinAt le_top
+    · simp_rw [Function.comp_apply, i.1.extend_left_inv hxi, j.1.extend_left_inv hxj]
+    · exact (contDiffWithinAt_extend_coord_change' (subset_maximalAtlas k.2)
+        (subset_maximalAtlas j.2) hxk hxj).differentiableWithinAt le_top
+    · exact (contDiffWithinAt_extend_coord_change' (subset_maximalAtlas j.2)
+        (subset_maximalAtlas i.2) hxj hxi).differentiableWithinAt le_top
     · intro x _; exact mem_range_self _
     · exact I.uniqueDiffWithinAt_image
-    · rw [Function.comp_apply, i.1.extend_left_inv I hxi]
+    · rw [Function.comp_apply, i.1.extend_left_inv hxi]
 
 -- Porting note: moved to a separate `simp high` lemma b/c `simp` can simplify the LHS
 @[simp high]
 theorem tangentBundleCore_baseSet (i) : (tangentBundleCore I M).baseSet i = i.1.source := rfl
 
-variable {M}
-
 theorem tangentBundleCore_coordChange_achart (x x' z : M) :
     (tangentBundleCore I M).coordChange (achart H x) (achart H x') z =
       fderivWithin 𝕜 (extChartAt I x' ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) :=
@@ -125,6 +122,7 @@ theorem tangentBundleCore_coordChange_achart (x x' z : M) :
 
 section tangentCoordChange
 
+variable (I) in
 /-- In a manifold `M`, given two preferred charts indexed by `x y : M`, `tangentCoordChange I x y`
 is the family of derivatives of the corresponding change-of-coordinates map. It takes junk values
 outside the intersection of the sources of the two charts.
@@ -134,8 +132,6 @@ sets as the preferred charts of the base manifold. -/
 abbrev tangentCoordChange (x y : M) : M → E →L[𝕜] E :=
   (tangentBundleCore I M).coordChange (achart H x) (achart H y)
 
-variable {I}
-
 lemma tangentCoordChange_def {x y z : M} : tangentCoordChange I x y z =
     fderivWithin 𝕜 (extChartAt I y ∘ (extChartAt I x).symm) (range I) (extChartAt I x z) := rfl
 
@@ -159,7 +155,7 @@ lemma hasFDerivWithinAt_tangentCoordChange {x y z : M}
   have h' : extChartAt I x z ∈ ((extChartAt I x).symm ≫ (extChartAt I y)).source := by
     rw [PartialEquiv.trans_source'', PartialEquiv.symm_symm, PartialEquiv.symm_target]
     exact mem_image_of_mem _ h
-  ((contDiffWithinAt_ext_coord_change I y x h').differentiableWithinAt (by simp)).hasFDerivWithinAt
+  ((contDiffWithinAt_ext_coord_change y x h').differentiableWithinAt (by simp)).hasFDerivWithinAt
 
 lemma continuousOn_tangentCoordChange (x y : M) : ContinuousOn (tangentCoordChange I x y)
     ((extChartAt I x).source ∩ (extChartAt I y).source) := by
@@ -168,8 +164,6 @@ lemma continuousOn_tangentCoordChange (x y : M) : ContinuousOn (tangentCoordChan
 
 end tangentCoordChange
 
-variable (M)
-
 local notation "TM" => TangentBundle I M
 
 section TangentBundleInstances
@@ -292,16 +286,16 @@ end TangentBundle
 
 instance tangentBundleCore.isSmooth : (tangentBundleCore I M).IsSmooth I := by
   refine ⟨fun i j => ?_⟩
-  rw [SmoothOn, contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas I i.2),
+  rw [SmoothOn, contMDiffOn_iff_source_of_mem_maximalAtlas (subset_maximalAtlas i.2),
     contMDiffOn_iff_contDiffOn]
-  · refine ((contDiffOn_fderiv_coord_change I i j).congr fun x hx => ?_).mono ?_
+  · refine ((contDiffOn_fderiv_coord_change (I := I) i j).congr fun x hx => ?_).mono ?_
     · rw [PartialEquiv.trans_source'] at hx
       simp_rw [Function.comp_apply, tangentBundleCore_coordChange, (i.1.extend I).right_inv hx.1]
-    · exact (i.1.extend_image_source_inter j.1 I).subset
+    · exact (i.1.extend_image_source_inter j.1).subset
   · apply inter_subset_left
 
 instance TangentBundle.smoothVectorBundle : SmoothVectorBundle E (TangentSpace I : M → Type _) I :=
-  (tangentBundleCore I M).smoothVectorBundle _
+  (tangentBundleCore I M).smoothVectorBundle
 
 end TangentBundleInstances
 
@@ -341,8 +335,7 @@ theorem tangentBundleCore_coordChange_model_space (x x' z : H) :
     ContinuousLinearMap.id 𝕜 E := by
   ext v; exact (tangentBundleCore I H).coordChange_self (achart _ z) z (mem_univ _) v
 
-variable (H)
-
+variable (I) in
 /-- The canonical identification between the tangent bundle to the model space and the product,
 as a homeomorphism -/
 def tangentBundleModelSpaceHomeomorph : TangentBundle I H ≃ₜ ModelProd H E :=
@@ -364,19 +357,18 @@ def tangentBundleModelSpaceHomeomorph : TangentBundle I H ≃ₜ ModelProd H E :
 
 @[simp, mfld_simps]
 theorem tangentBundleModelSpaceHomeomorph_coe :
-    (tangentBundleModelSpaceHomeomorph H I : TangentBundle I H → ModelProd H E) =
+    (tangentBundleModelSpaceHomeomorph I : TangentBundle I H → ModelProd H E) =
       TotalSpace.toProd H E :=
   rfl
 
 @[simp, mfld_simps]
 theorem tangentBundleModelSpaceHomeomorph_coe_symm :
-    ((tangentBundleModelSpaceHomeomorph H I).symm : ModelProd H E → TangentBundle I H) =
+    ((tangentBundleModelSpaceHomeomorph I).symm : ModelProd H E → TangentBundle I H) =
       (TotalSpace.toProd H E).symm :=
   rfl
 
 section inTangentCoordinates
 
-variable (I') {M H}
 variable {N : Type*}
 
 /-- The map `in_coordinates` for the tangent bundle is trivial on the model spaces -/
@@ -386,6 +378,7 @@ theorem inCoordinates_tangent_bundle_core_model_space (x₀ x : H) (y₀ y : H')
   simp_rw [tangentBundleCore_indexAt, tangentBundleCore_coordChange_model_space,
     ContinuousLinearMap.id_comp, ContinuousLinearMap.comp_id]
 
+variable (I I') in
 /-- When `ϕ x` is a continuous linear map that changes vectors in charts around `f x` to vectors
 in charts around `g x`, `inTangentCoordinates I I' f g ϕ x₀ x` is a coordinate change of
 this continuous linear map that makes sense from charts around `f x₀` to charts around `g x₀`
diff --git a/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean b/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
index 4e56b5f717089..8106c8dd8e80c 100644
--- a/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
+++ b/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
@@ -83,7 +83,7 @@ theorem comp_embeddingPiTangent_mfderiv (x : M) (hx : x ∈ s) :
       (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))
   have := L.hasMFDerivAt.comp x f.embeddingPiTangent.smooth.mdifferentiableAt.hasMFDerivAt
   convert hasMFDerivAt_unique this _
-  refine (hasMFDerivAt_extChartAt I (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
+  refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
   refine (f.eventuallyEq_one x hx).mono fun y hy => ?_
   simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp', (· ∘ ·),
     ContinuousLinearMap.coe_fst', ContinuousLinearMap.proj_apply]
@@ -92,7 +92,7 @@ theorem comp_embeddingPiTangent_mfderiv (x : M) (hx : x ∈ s) :
 theorem embeddingPiTangent_ker_mfderiv (x : M) (hx : x ∈ s) :
     LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) f.embeddingPiTangent x) = ⊥ := by
   apply bot_unique
-  rw [← (mdifferentiable_chart I (f.c (f.ind x hx))).ker_mfderiv_eq_bot
+  rw [← (mdifferentiable_chart (f.c (f.ind x hx))).ker_mfderiv_eq_bot
       (f.mem_chartAt_ind_source x hx),
     ← comp_embeddingPiTangent_mfderiv]
   exact LinearMap.ker_le_ker_comp _ _
diff --git a/Mathlib/NumberTheory/ModularForms/Basic.lean b/Mathlib/NumberTheory/ModularForms/Basic.lean
index aca96ca362386..c0482b00817f7 100644
--- a/Mathlib/NumberTheory/ModularForms/Basic.lean
+++ b/Mathlib/NumberTheory/ModularForms/Basic.lean
@@ -152,7 +152,7 @@ theorem add_apply (f g : ModularForm Γ k) (z : ℍ) : (f + g) z = f z + g z :=
 
 instance instZero : Zero (ModularForm Γ k) :=
   ⟨ { toSlashInvariantForm := 0
-      holo' := fun _ => mdifferentiableAt_const 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ)
+      holo' := fun _ => mdifferentiableAt_const
       bdd_at_infty' := fun A => by simpa using zero_form_isBoundedAtImInfty } ⟩
 
 @[simp]
@@ -245,7 +245,7 @@ theorem mul_coe {k_1 k_2 : ℤ} {Γ : Subgroup SL(2, ℤ)} (f : ModularForm Γ k
 @[simps! (config := .asFn) toFun toSlashInvariantForm]
 def const (x : ℂ) : ModularForm Γ 0 where
   toSlashInvariantForm := .const x
-  holo' _ := mdifferentiableAt_const 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ)
+  holo' _ := mdifferentiableAt_const
   bdd_at_infty' A := by
     simpa only [SlashInvariantForm.const_toFun,
       ModularForm.is_invariant_const] using atImInfty.const_boundedAtFilter x
@@ -301,7 +301,7 @@ theorem add_apply (f g : CuspForm Γ k) (z : ℍ) : (f + g) z = f z + g z :=
 
 instance instZero : Zero (CuspForm Γ k) :=
   ⟨ { toSlashInvariantForm := 0
-      holo' := fun _ => mdifferentiableAt_const 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ)
+      holo' := fun _ => mdifferentiableAt_const
       zero_at_infty' := by simpa using Filter.zero_zeroAtFilter _ } ⟩
 
 @[simp]