diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
index 560a5447624aa..1dac252bbf591 100644
--- a/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
+++ b/Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
@@ -23,9 +23,10 @@ open FiniteDimensional
 namespace Subalgebra
 
 variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
-  (A B : Subalgebra R S) [Module.Free R A] [Module.Free R B]
-  [Module.Free A (Algebra.adjoin A (B : Set S))]
-  [Module.Free B (Algebra.adjoin B (A : Set S))]
+  (A B : Subalgebra R S)
+
+section
+variable [Module.Free R A] [Module.Free A (Algebra.adjoin A (B : Set S))]
 
 theorem rank_sup_eq_rank_left_mul_rank_of_free :
     Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank A (Algebra.adjoin A (B : Set S)) := by
@@ -40,22 +41,29 @@ theorem rank_sup_eq_rank_left_mul_rank_of_free :
   change _ = Module.rank R ((Algebra.adjoin A (B : Set S)).restrictScalars R)
   rw [Algebra.restrictScalars_adjoin]; rfl
 
-theorem rank_sup_eq_rank_right_mul_rank_of_free :
-    Module.rank R ↥(A ⊔ B) = Module.rank R B * Module.rank B (Algebra.adjoin B (A : Set S)) := by
-  rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
-
 theorem finrank_sup_eq_finrank_left_mul_finrank_of_free :
     finrank R ↥(A ⊔ B) = finrank R A * finrank A (Algebra.adjoin A (B : Set S)) := by
   simpa only [map_mul] using congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))
 
+theorem finrank_left_dvd_finrank_sup_of_free :
+    finrank R A ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_left_mul_finrank_of_free A B⟩
+
+end
+
+section
+variable [Module.Free R B] [Module.Free B (Algebra.adjoin B (A : Set S))]
+
+theorem rank_sup_eq_rank_right_mul_rank_of_free :
+    Module.rank R ↥(A ⊔ B) = Module.rank R B * Module.rank B (Algebra.adjoin B (A : Set S)) := by
+  rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
+
 theorem finrank_sup_eq_finrank_right_mul_finrank_of_free :
     finrank R ↥(A ⊔ B) = finrank R B * finrank B (Algebra.adjoin B (A : Set S)) := by
   rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]
 
-theorem finrank_left_dvd_finrank_sup_of_free :
-    finrank R A ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_left_mul_finrank_of_free A B⟩
-
 theorem finrank_right_dvd_finrank_sup_of_free :
     finrank R B ∣ finrank R ↥(A ⊔ B) := ⟨_, finrank_sup_eq_finrank_right_mul_finrank_of_free A B⟩
 
+end
+
 end Subalgebra
diff --git a/Mathlib/Algebra/Category/Grp/Injective.lean b/Mathlib/Algebra/Category/Grp/Injective.lean
index 1cc9915df9083..04d0f6d61c4a0 100644
--- a/Mathlib/Algebra/Category/Grp/Injective.lean
+++ b/Mathlib/Algebra/Category/Grp/Injective.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.EuclideanDomain.Int
 import Mathlib.Algebra.Module.Injective
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.Topology.Instances.AddCircle
-import Mathlib.Topology.Instances.Rat
 
 /-!
 # Injective objects in the category of abelian groups
diff --git a/Mathlib/Algebra/Module/CharacterModule.lean b/Mathlib/Algebra/Module/CharacterModule.lean
index 951be6418e88c..bd0b99a07a4fe 100644
--- a/Mathlib/Algebra/Module/CharacterModule.lean
+++ b/Mathlib/Algebra/Module/CharacterModule.lean
@@ -7,7 +7,6 @@ Authors: Jujian Zhang, Junyan Xu
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.Grp.Injective
 import Mathlib.Topology.Instances.AddCircle
-import Mathlib.Topology.Instances.Rat
 import Mathlib.LinearAlgebra.Isomorphisms
 
 /-!
diff --git a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
index 83a147ec797e3..ab0f694338b18 100644
--- a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
+++ b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@@ -685,7 +685,7 @@ lemma adjoin_eq_span (s : Set A) :
   rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]
 
 @[simp]
-lemma span_eq_toSubmodule (s : NonUnitalStarSubalgebra R A) :
+lemma span_eq_toSubmodule {R} [CommSemiring R] [Module R A] (s : NonUnitalStarSubalgebra R A) :
     Submodule.span R (s : Set A) = s.toSubmodule := by
   simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]
 
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
index a824595d91b6c..7defe194cdd22 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@@ -322,14 +322,16 @@ lemma cfc_cases (P : A → Prop) (a : A) (f : R → R) (h₀ : P 0)
     · rwa [cfc_apply_of_not_continuousOn _ h]
 
 variable (R) in
-lemma cfc_id : cfc (id : R → R) a = a :=
+lemma cfc_id (ha : p a := by cfc_tac) : cfc (id : R → R) a = a :=
   cfc_apply (id : R → R) a ▸ cfcHom_id (p := p) ha
 
 variable (R) in
-lemma cfc_id' : cfc (fun x : R ↦ x) a = a := cfc_id R a
+lemma cfc_id' (ha : p a := by cfc_tac) : cfc (fun x : R ↦ x) a = a := cfc_id R a
 
 /-- The **spectral mapping theorem** for the continuous functional calculus. -/
-lemma cfc_map_spectrum : spectrum R (cfc f a) = f '' spectrum R a := by
+lemma cfc_map_spectrum (ha : p a := by cfc_tac)
+    (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) :
+    spectrum R (cfc f a) = f '' spectrum R a := by
   simp [cfc_apply f a, cfcHom_map_spectrum (p := p)]
 
 lemma cfc_const (r : R) (a : A) (ha : p a := by cfc_tac) :
@@ -372,15 +374,18 @@ lemma eqOn_of_cfc_eq_cfc {f g : R → R} {a : A} (h : cfc f a = cfc g a)
   congrm($(this) ⟨x, hx⟩)
 
 variable {a f g} in
-lemma cfc_eq_cfc_iff_eqOn : cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
+lemma cfc_eq_cfc_iff_eqOn (ha : p a := by cfc_tac)
+    (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
+    (hg : ContinuousOn g (spectrum R a) := by cfc_cont_tac) :
+    cfc f a = cfc g a ↔ (spectrum R a).EqOn f g :=
   ⟨eqOn_of_cfc_eq_cfc, cfc_congr⟩
 
 variable (R)
 
-lemma cfc_one : cfc (1 : R → R) a = 1 :=
+lemma cfc_one (ha : p a := by cfc_tac) : cfc (1 : R → R) a = 1 :=
   cfc_apply (1 : R → R) a ▸ map_one (cfcHom (show p a from ha))
 
-lemma cfc_const_one : cfc (fun _ : R ↦ 1) a = 1 := cfc_one R a
+lemma cfc_const_one (ha : p a := by cfc_tac) : cfc (fun _ : R ↦ 1) a = 1 := cfc_one R a
 
 @[simp]
 lemma cfc_zero : cfc (0 : R → R) a = 0 := by
@@ -488,7 +493,7 @@ lemma cfc_smul_id {S : Type*} [SMul S R] [ContinuousConstSMul S R]
 lemma cfc_const_mul_id (r : R) (a : A) (ha : p a := by cfc_tac) : cfc (r * ·) a = r • a :=
   cfc_smul_id r a
 
-lemma cfc_star_id : cfc (star · : R → R) a = star a := by
+lemma cfc_star_id (ha : p a := by cfc_tac) : cfc (star · : R → R) a = star a := by
   rw [cfc_star .., cfc_id' ..]
 
 section Polynomial
@@ -518,6 +523,19 @@ lemma cfc_polynomial (q : R[X]) (a : A) (ha : p a := by cfc_tac) :
 
 end Polynomial
 
+lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
+    (ha : p a := by cfc_tac) : a = algebraMap R A r := by
+  simpa [cfc_id R a, cfc_const r a] using
+    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
+
+lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
+    a = 0 := by
+  simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
+
+lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
+    a = 1 := by
+  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
+
 variable [UniqueContinuousFunctionalCalculus R A]
 
 lemma cfc_comp (g f : R → R) (a : A) (ha : p a := by cfc_tac)
@@ -569,19 +587,6 @@ lemma cfc_comp_polynomial (q : R[X]) (f : R → R) (a : A)
     cfc (f <| q.eval ·) a = cfc f (aeval a q) := by
   rw [cfc_comp' .., cfc_polynomial ..]
 
-lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
-    (ha : p a := by cfc_tac) : a = algebraMap R A r := by
-  simpa [cfc_id R a, cfc_const r a] using
-    cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx
-
-lemma CFC.eq_zero_of_spectrum_subset_zero (h_spec : spectrum R a ⊆ {0}) (ha : p a := by cfc_tac) :
-    a = 0 := by
-  simpa using eq_algebraMap_of_spectrum_subset_singleton a 0 h_spec
-
-lemma CFC.eq_one_of_spectrum_subset_one (h_spec : spectrum R a ⊆ {1}) (ha : p a := by cfc_tac) :
-    a = 1 := by
-  simpa using eq_algebraMap_of_spectrum_subset_singleton a 1 h_spec
-
 lemma CFC.spectrum_algebraMap_subset (r : R) : spectrum R (algebraMap R A r) ⊆ {r} := by
   rw [← cfc_const r 0 (cfc_predicate_zero R),
     cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]
@@ -637,7 +642,7 @@ end Basic
 section Inv
 
 variable {R A : Type*} {p : A → Prop} [Semifield R] [StarRing R] [MetricSpace R]
-variable [TopologicalSemiring R] [ContinuousStar R] [HasContinuousInv₀ R] [TopologicalSpace A]
+variable [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A]
 variable [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p]
 variable (f : R → R) (a : A)
 
@@ -648,6 +653,8 @@ lemma isUnit_cfc_iff (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
 
 alias ⟨_, isUnit_cfc⟩ := isUnit_cfc_iff
 
+variable [HasContinuousInv₀ R]
+
 /-- Bundle `cfc f a` into a unit given a proof that `f` is nonzero on the spectrum of `a`. -/
 @[simps]
 noncomputable def cfcUnits (hf' : ∀ x ∈ spectrum R a, f x ≠ 0)
diff --git a/Mathlib/Analysis/CStarAlgebra/Unitization.lean b/Mathlib/Analysis/CStarAlgebra/Unitization.lean
index 85446f1873905..0ccc38b7262f0 100644
--- a/Mathlib/Analysis/CStarAlgebra/Unitization.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Unitization.lean
@@ -76,7 +76,7 @@ instance CStarRing.instRegularNormedAlgebra : RegularNormedAlgebra 𝕜 E where
 
 section CStarProperty
 
-variable [StarRing 𝕜] [CStarRing 𝕜] [StarModule 𝕜 E]
+variable [StarRing 𝕜] [StarModule 𝕜 E]
 variable {E}
 
 /-- This is the key lemma used to establish the instance `Unitization.instCStarRing`
@@ -122,6 +122,7 @@ theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
     simp only [smul_smul, smul_mul_assoc, ← add_assoc, ← mul_assoc, mul_smul_comm]
 
 variable {𝕜}
+variable [CStarRing 𝕜]
 
 /-- The norm on `Unitization 𝕜 E` satisfies the C⋆-property -/
 instance Unitization.instCStarRing : CStarRing (Unitization 𝕜 E) where
diff --git a/Mathlib/Analysis/Normed/Algebra/Unitization.lean b/Mathlib/Analysis/Normed/Algebra/Unitization.lean
index 68b0fbc2e2b4a..789e764e8c4e0 100644
--- a/Mathlib/Analysis/Normed/Algebra/Unitization.lean
+++ b/Mathlib/Analysis/Normed/Algebra/Unitization.lean
@@ -208,7 +208,8 @@ def uniformEquivProd : (Unitization 𝕜 A) ≃ᵤ (𝕜 × A) :=
 instance instBornology : Bornology (Unitization 𝕜 A) :=
   Bornology.induced <| addEquiv 𝕜 A
 
-theorem uniformEmbedding_addEquiv : UniformEmbedding (addEquiv 𝕜 A) where
+theorem uniformEmbedding_addEquiv {𝕜} [NontriviallyNormedField 𝕜] :
+    UniformEmbedding (addEquiv 𝕜 A) where
   comap_uniformity := rfl
   inj := (addEquiv 𝕜 A).injective
 
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
index e1c5202a1d788..c3efa1e0e4436 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -90,10 +90,9 @@ theorem ContinuousMultilinearMap.continuous_eval {𝕜 ι : Type*} {E : ι → T
 section Seminorm
 
 variable {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E₁ : ι → Type wE₁}
-  {E' : ι' → Type wE'} {G : Type wG} {G' : Type wG'} [Fintype ι]
+  {E' : ι' → Type wE'} {G : Type wG} {G' : Type wG'}
   [Fintype ι'] [NontriviallyNormedField 𝕜] [∀ i, SeminormedAddCommGroup (E i)]
   [∀ i, NormedSpace 𝕜 (E i)] [∀ i, SeminormedAddCommGroup (E₁ i)] [∀ i, NormedSpace 𝕜 (E₁ i)]
-  [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
   [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G']
 
 /-!
@@ -121,6 +120,8 @@ lemma norm_map_coord_zero (hf : Continuous f) {m : ∀ i, E i} {i : ι} (hi : 
     (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩
   simpa only [map_update_zero] using this.symm.map hf
 
+variable [Fintype ι]
+
 theorem bound_of_shell_of_norm_map_coord_zero (hf₀ : ∀ {m i}, ‖m i‖ = 0 → ‖f m‖ = 0)
     {ε : ι → ℝ} {C : ℝ} (hε : ∀ i, 0 < ε i) {c : ι → 𝕜} (hc : ∀ i, 1 < ‖c i‖)
     (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖)
@@ -297,7 +298,7 @@ defines a normed space structure on `ContinuousMultilinearMap 𝕜 E G`.
 
 namespace ContinuousMultilinearMap
 
-variable (c : 𝕜) (f g : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i)
+variable [Fintype ι] (c : 𝕜) (f g : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i)
 
 theorem bound : ∃ C : ℝ, 0 < C ∧ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
   f.toMultilinearMap.exists_bound_of_continuous f.2
@@ -687,6 +688,8 @@ theorem norm_image_sub_le (m₁ m₂ : ∀ i, E i) :
 
 end ContinuousMultilinearMap
 
+variable [Fintype ι]
+
 /-- If a continuous multilinear map is constructed from a multilinear map via the constructor
 `mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
 nonnegative. -/
@@ -990,6 +993,8 @@ theorem mkContinuousLinear_norm_le (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G')
     (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C :=
   (mkContinuousLinear_norm_le' f C H).trans_eq (max_eq_left hC)
 
+variable [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
+
 /-- Given a map `f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)` and an estimate
 `H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `MultilinearMap`s in the type to
 `ContinuousMultilinearMap`s. -/
@@ -1157,10 +1162,10 @@ noncomputable def compContinuousLinearMapContinuousMultilinear :
     ContinuousMultilinearMap 𝕜 (fun i ↦ E i →L[𝕜] E₁ i)
       ((ContinuousMultilinearMap 𝕜 E₁ G) →L[𝕜] ContinuousMultilinearMap 𝕜 E G) :=
   @MultilinearMap.mkContinuous 𝕜 ι (fun i ↦ E i →L[𝕜] E₁ i)
-    ((ContinuousMultilinearMap 𝕜 E₁ G) →L[𝕜] ContinuousMultilinearMap 𝕜 E G) _ _
+    ((ContinuousMultilinearMap 𝕜 E₁ G) →L[𝕜] ContinuousMultilinearMap 𝕜 E G) _
     (fun _ ↦ ContinuousLinearMap.toSeminormedAddCommGroup)
     (fun _ ↦ ContinuousLinearMap.toNormedSpace) _ _
-    (compContinuousLinearMapMultilinear 𝕜 E E₁ G) 1
+    (compContinuousLinearMapMultilinear 𝕜 E E₁ G) _ 1
     fun f ↦ by simpa using norm_compContinuousLinearMapL_le G f
 
 variable {𝕜 E E₁}
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
index 8be1705a830fc..07c05d0a62e73 100644
--- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
+++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
@@ -84,14 +84,14 @@ end ContinuousLinearMap
 
 namespace LinearMap
 
-variable [RingHomIsometric σ₂₃]
-
 lemma norm_mkContinuous₂_aux (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ)
     (h : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E) :
     ‖(f x).mkContinuous (C * ‖x‖) (h x)‖ ≤ max C 0 * ‖x‖ :=
   (mkContinuous_norm_le' (f x) (h x)).trans_eq <| by
     rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
 
+variable [RingHomIsometric σ₂₃]
+
 /-- Create a bilinear map (represented as a map `E →L[𝕜] F →L[𝕜] G`) from the corresponding linear
 map and existence of a bound on the norm of the image. The linear map can be constructed using
 `LinearMap.mk₂`.
diff --git a/Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean b/Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
index 74ef28683a937..ec8cbeca4457f 100644
--- a/Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
+++ b/Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
@@ -39,7 +39,7 @@ universe uι u𝕜 uE uF
 
 variable {ι : Type uι} [Fintype ι]
 variable {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜]
-variable {E : ι → Type uE} [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
+variable {E : ι → Type uE} [∀ i, SeminormedAddCommGroup (E i)]
 variable {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 open scoped TensorProduct
@@ -81,6 +81,8 @@ theorem projectiveSeminormAux_smul (p : FreeAddMonoid (𝕜 × Π i, E i)) (a :
   simp only [Function.comp_apply, norm_mul, smul_eq_mul]
   rw [mul_assoc]
 
+variable [∀ i, NormedSpace 𝕜 (E i)]
+
 theorem bddBelow_projectiveSemiNormAux (x : ⨂[𝕜] i, E i) :
     BddBelow (Set.range (fun (p : lifts x) ↦ projectiveSeminormAux p.1)) := by
   existsi 0
diff --git a/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean
index f5e91a85cbb1e..e66a91cfd4c63 100644
--- a/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean
@@ -22,19 +22,18 @@ open GrothendieckTopology
 namespace Equivalence
 
 variable {D : Type*} [Category D]
-variable (e : C ≌ D)
 
 section Coherent
 
 variable [Precoherent C]
 
 /-- `Precoherent` is preserved by equivalence of categories. -/
-theorem precoherent : Precoherent D := e.inverse.reflects_precoherent
+theorem precoherent (e : C ≌ D) : Precoherent D := e.inverse.reflects_precoherent
 
 instance [EssentiallySmall C] :
     Precoherent (SmallModel C) := (equivSmallModel C).precoherent
 
-instance : haveI := precoherent e
+instance (e : C ≌ D) : haveI := precoherent e
     e.inverse.IsDenseSubsite (coherentTopology D) (coherentTopology C) where
   functorPushforward_mem_iff := by
     rw [coherentTopology.eq_induced e.inverse]
@@ -46,7 +45,7 @@ variable (A : Type*) [Category A]
 Equivalent precoherent categories give equivalent coherent toposes.
 -/
 @[simps!]
-def sheafCongrPrecoherent : haveI := e.precoherent
+def sheafCongrPrecoherent (e : C ≌ D) : haveI := e.precoherent
     Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A := e.sheafCongr _ _ _
 
 open Presheaf
@@ -54,7 +53,7 @@ open Presheaf
 /--
 The coherent sheaf condition can be checked after precomposing with the equivalence.
 -/
-theorem precoherent_isSheaf_iff (F : Cᵒᵖ ⥤ A) : haveI := e.precoherent
+theorem precoherent_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) : haveI := e.precoherent
     IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F) := by
   refine ⟨fun hF ↦ ((e.sheafCongrPrecoherent A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩
   rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
@@ -77,12 +76,12 @@ section Regular
 variable [Preregular C]
 
 /-- `Preregular` is preserved by equivalence of categories. -/
-theorem preregular : Preregular D := e.inverse.reflects_preregular
+theorem preregular (e : C ≌ D) : Preregular D := e.inverse.reflects_preregular
 
 instance [EssentiallySmall C] :
     Preregular (SmallModel C) := (equivSmallModel C).preregular
 
-instance : haveI := preregular e
+instance (e : C ≌ D) : haveI := preregular e
     e.inverse.IsDenseSubsite (regularTopology D) (regularTopology C) where
   functorPushforward_mem_iff := by
     rw [regularTopology.eq_induced e.inverse]
@@ -94,7 +93,7 @@ variable (A : Type*) [Category A]
 Equivalent preregular categories give equivalent regular toposes.
 -/
 @[simps!]
-def sheafCongrPreregular : haveI := e.preregular
+def sheafCongrPreregular (e : C ≌ D) : haveI := e.preregular
     Sheaf (regularTopology C) A ≌ Sheaf (regularTopology D) A := e.sheafCongr _ _ _
 
 open Presheaf
@@ -102,7 +101,7 @@ open Presheaf
 /--
 The regular sheaf condition can be checked after precomposing with the equivalence.
 -/
-theorem preregular_isSheaf_iff (F : Cᵒᵖ ⥤ A) : haveI := e.preregular
+theorem preregular_isSheaf_iff (e : C ≌ D) (F : Cᵒᵖ ⥤ A) : haveI := e.preregular
     IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F) := by
   refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).cond, fun hF ↦ ?_⟩
   rw [isSheaf_of_iso_iff (P' := e.functor.op ⋙ e.inverse.op ⋙ F)]
diff --git a/Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean b/Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
index ab0bbf619ae27..0360e2114a8d9 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
@@ -49,8 +49,8 @@ variable {k P₁ P₂ P₃ P₄ V₁ V₂ V₃ V₄ : Type*} [Ring k]
   [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂]
   [AddCommGroup V₃] [Module k V₃] [AddTorsor V₃ P₃]
   [AddCommGroup V₄] [Module k V₄] [AddTorsor V₄ P₄]
-  [TopologicalSpace P₁] [AddCommMonoid P₁] [Module k P₁]
-  [TopologicalSpace P₂] [AddCommMonoid P₂] [Module k P₂]
+  [TopologicalSpace P₁]
+  [TopologicalSpace P₂]
   [TopologicalSpace P₃] [TopologicalSpace P₄]
 
 namespace ContinuousAffineEquiv
diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
index f1fb7c9f708a9..ed9305efcd20a 100644
--- a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
+++ b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
@@ -473,17 +473,19 @@ theorem eq_of_le_of_finrank_eq {S₁ S₂ : Submodule K V} [FiniteDimensional K
 section Subalgebra
 
 variable {K L : Type*} [Field K] [Ring L] [Algebra K L] {F E : Subalgebra K L}
-  [hfin : FiniteDimensional K E] (h_le : F ≤ E)
+  [hfin : FiniteDimensional K E]
 
 /-- If a subalgebra is contained in a finite-dimensional
 subalgebra with the same or smaller dimension, they are equal. -/
-theorem _root_.Subalgebra.eq_of_le_of_finrank_le (h_finrank : finrank K E ≤ finrank K F) : F = E :=
+theorem _root_.Subalgebra.eq_of_le_of_finrank_le (h_le : F ≤ E)
+    (h_finrank : finrank K E ≤ finrank K F) : F = E :=
   haveI : Module.Finite K (Subalgebra.toSubmodule E) := hfin
   Subalgebra.toSubmodule_injective <| FiniteDimensional.eq_of_le_of_finrank_le h_le h_finrank
 
 /-- If a subalgebra is contained in a finite-dimensional
 subalgebra with the same dimension, they are equal. -/
-theorem _root_.Subalgebra.eq_of_le_of_finrank_eq (h_finrank : finrank K F = finrank K E) : F = E :=
+theorem _root_.Subalgebra.eq_of_le_of_finrank_eq (h_le : F ≤ E)
+    (h_finrank : finrank K F = finrank K E) : F = E :=
   Subalgebra.eq_of_le_of_finrank_le h_le h_finrank.ge
 
 end Subalgebra
diff --git a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
index cbe6c2575aaa0..8455083320dad 100644
--- a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
+++ b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
@@ -140,7 +140,7 @@ theorem map_val_apply (f : M →ₗ[R] N) {n : ℕ} (x : AdicCompletion I M) :
   rfl
 
 /-- Equality of maps out of an adic completion can be checked on Cauchy sequences. -/
-theorem map_ext {f g : AdicCompletion I M → N}
+theorem map_ext {N} {f g : AdicCompletion I M → N}
     (h : ∀ (a : AdicCauchySequence I M),
       f (AdicCompletion.mk I M a) = g (AdicCompletion.mk I M a)) :
     f = g := by
diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
index 1676d72c3620b..6836737387416 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -38,12 +38,12 @@ namespace FractionalIdeal
 open Set Submodule
 
 variable {R : Type*} [CommRing R] {S : Submonoid R} {P : Type*} [CommRing P]
-variable [Algebra R P] [loc : IsLocalization S P]
+variable [Algebra R P]
 
 section
 
-variable {P' : Type*} [CommRing P'] [Algebra R P'] [loc' : IsLocalization S P']
-variable {P'' : Type*} [CommRing P''] [Algebra R P''] [loc'' : IsLocalization S P'']
+variable {P' : Type*} [CommRing P'] [Algebra R P']
+variable {P'' : Type*} [CommRing P''] [Algebra R P'']
 
 theorem _root_.IsFractional.map (g : P →ₐ[R] P') {I : Submodule R P} :
     IsFractional S I → IsFractional S (Submodule.map g.toLinearMap I)
@@ -165,7 +165,8 @@ theorem isFractional_span_iff {s : Set P} :
         rw [smul_comm]
         exact isInteger_smul hx⟩⟩
 
-theorem isFractional_of_fg {I : Submodule R P} (hI : I.FG) : IsFractional S I := by
+theorem isFractional_of_fg [IsLocalization S P] {I : Submodule R P} (hI : I.FG) :
+    IsFractional S I := by
   rcases hI with ⟨I, rfl⟩
   rcases exist_integer_multiples_of_finset S I with ⟨⟨s, hs1⟩, hs⟩
   rw [isFractional_span_iff]
@@ -196,6 +197,8 @@ theorem _root_.Ideal.fg_of_isUnit (inj : Function.Injective (algebraMap R P)) (I
 
 variable (S P P')
 
+variable [IsLocalization S P] [IsLocalization S P']
+
 /-- `canonicalEquiv f f'` is the canonical equivalence between the fractional
 ideals in `P` and in `P'`, which are both localizations of `R` at `S`. -/
 noncomputable irreducible_def canonicalEquiv : FractionalIdeal S P ≃+* FractionalIdeal S P' :=
@@ -329,7 +332,7 @@ is a field because `R` is a domain.
 -/
 
 variable {R₁ : Type*} [CommRing R₁] {K : Type*} [Field K]
-variable [Algebra R₁ K] [frac : IsFractionRing R₁ K]
+variable [Algebra R₁ K]
 
 instance : Nontrivial (FractionalIdeal R₁⁰ K) :=
   ⟨⟨0, 1, fun h =>
@@ -344,7 +347,7 @@ theorem ne_zero_of_mul_eq_one (I J : FractionalIdeal R₁⁰ K) (h : I * J = 1)
       convert h
       simp [hI])
 
-variable [IsDomain R₁]
+variable [IsFractionRing R₁ K] [IsDomain R₁]
 
 theorem _root_.IsFractional.div_of_nonzero {I J : Submodule R₁ K} :
     IsFractional R₁⁰ I → IsFractional R₁⁰ J → J ≠ 0 → IsFractional R₁⁰ (I / J)
@@ -541,6 +544,8 @@ theorem spanFinset_ne_zero {ι : Type*} {s : Finset ι} {f : ι → K} :
 
 open Submodule.IsPrincipal
 
+variable [IsLocalization S P]
+
 theorem isFractional_span_singleton (x : P) : IsFractional S (span R {x} : Submodule R P) :=
   let ⟨a, ha⟩ := exists_integer_multiple S x
   isFractional_span_iff.mpr ⟨a, a.2, fun _ hx' => (Set.mem_singleton_iff.mp hx').symm ▸ ha⟩
@@ -814,7 +819,7 @@ theorem num_le (I : FractionalIdeal S P) :
 end PrincipalIdeal
 
 variable {R₁ : Type*} [CommRing R₁]
-variable {K : Type*} [Field K] [Algebra R₁ K] [frac : IsFractionRing R₁ K]
+variable {K : Type*} [Field K] [Algebra R₁ K]
 
 attribute [local instance] Classical.propDecidable
 
@@ -835,7 +840,7 @@ theorem isNoetherian_coeIdeal [IsNoetherianRing R₁] (I : Ideal R₁) :
   obtain ⟨J, rfl⟩ := le_one_iff_exists_coeIdeal.mp (le_trans hJ coeIdeal_le_one)
   exact (IsNoetherian.noetherian J).map _
 
-variable [IsDomain R₁]
+variable [IsFractionRing R₁ K] [IsDomain R₁]
 
 theorem isNoetherian_spanSingleton_inv_to_map_mul (x : R₁) {I : FractionalIdeal R₁⁰ K}
     (hI : IsNoetherian R₁ I) :
@@ -864,10 +869,10 @@ theorem isNoetherian [IsNoetherianRing R₁] (I : FractionalIdeal R₁⁰ K) : I
 section Adjoin
 
 variable (S)
-variable (x : P) (hx : IsIntegral R x)
+variable [IsLocalization S P] (x : P)
 
 /-- `A[x]` is a fractional ideal for every integral `x`. -/
-theorem isFractional_adjoin_integral :
+theorem isFractional_adjoin_integral (hx : IsIntegral R x) :
     IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R ({x} : Set P))) :=
   isFractional_of_fg hx.fg_adjoin_singleton
 
@@ -875,16 +880,16 @@ theorem isFractional_adjoin_integral :
 where `hx` is a proof that `x : P` is integral over `R`. -/
 -- Porting note: `@[simps]` generated a `Subtype.val` coercion instead of a
 -- `FractionalIdeal.coeToSubmodule` coercion
-def adjoinIntegral : FractionalIdeal S P :=
+def adjoinIntegral (hx : IsIntegral R x) : FractionalIdeal S P :=
   ⟨_, isFractional_adjoin_integral S x hx⟩
 
 @[simp]
-theorem adjoinIntegral_coe :
+theorem adjoinIntegral_coe (hx : IsIntegral R x) :
     (adjoinIntegral S x hx : Submodule R P) =
       (Subalgebra.toSubmodule (Algebra.adjoin R ({x} : Set P))) :=
   rfl
 
-theorem mem_adjoinIntegral_self : x ∈ adjoinIntegral S x hx :=
+theorem mem_adjoinIntegral_self (hx : IsIntegral R x) : x ∈ adjoinIntegral S x hx :=
   Algebra.subset_adjoin (Set.mem_singleton x)
 
 end Adjoin
diff --git a/Mathlib/Topology/Algebra/Algebra.lean b/Mathlib/Topology/Algebra/Algebra.lean
index 5870483dbea15..b4367b4042dc1 100644
--- a/Mathlib/Topology/Algebra/Algebra.lean
+++ b/Mathlib/Topology/Algebra/Algebra.lean
@@ -78,8 +78,8 @@ section TopologicalAlgebra
 
 section
 
-variable (R : Type*) [CommSemiring R] [TopologicalSpace R] [TopologicalSemiring R]
-  (A : Type*) [Semiring A] [TopologicalSpace A] [TopologicalSemiring A]
+variable (R : Type*) [CommSemiring R]
+  (A : Type*) [Semiring A]
 
 /-- Continuous algebra homomorphisms between algebras. We only put the type classes that are
 necessary for the definition, although in applications `M` and `B` will be topological algebras
@@ -98,7 +98,7 @@ namespace ContinuousAlgHom
 section Semiring
 
 variable {R} {A}
-variable [TopologicalSpace R] [TopologicalSemiring R]
+variable [TopologicalSpace A]
 
 variable {B : Type*} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B]
 
@@ -207,6 +207,8 @@ theorem ext_on [T2Space B] {s : Set A} (hs : Dense (Algebra.adjoin R s : Set A))
     {f g : A →A[R] B} (h : Set.EqOn f g s) : f = g :=
   ext fun x => eqOn_closure_adjoin h (hs x)
 
+variable [TopologicalSemiring A]
+
 /-- The topological closure of a subalgebra -/
 def _root_.Subalgebra.topologicalClosure (s : Subalgebra R A) : Subalgebra R A where
   toSubsemiring := s.toSubsemiring.topologicalClosure
@@ -244,6 +246,7 @@ end Semiring
 
 section id
 
+variable [TopologicalSpace A]
 variable [Algebra R A]
 
 /-- The identity map as a continuous algebra homomorphism. -/
@@ -274,6 +277,7 @@ end id
 section comp
 
 variable {R} {A}
+variable [TopologicalSpace A]
 variable {B : Type*} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B]
   {C : Type*} [Semiring C] [Algebra R C] [TopologicalSpace C]
 
@@ -331,6 +335,7 @@ end comp
 section prod
 
 variable {R} {A}
+variable [TopologicalSpace A]
 variable {B : Type*} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B]
   {C : Type*} [Semiring C] [Algebra R C] [TopologicalSpace C]
 
@@ -431,6 +436,7 @@ end prod
 section subalgebra
 
 variable {R A}
+variable [TopologicalSpace A]
 variable {B : Type*} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B]
 
 /-- Restrict codomain of a continuous algebra morphism. -/
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
index be2896bac4115..09d1d25020184 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
@@ -108,7 +108,7 @@ end Multipliable
 
 section tprod
 
-variable [T2Space M] {α β γ : Type*}
+variable {α β γ : Type*}
 
 section Encodable
 
@@ -175,7 +175,7 @@ end Countable
 
 section ContinuousMul
 
-variable [ContinuousMul M]
+variable [T2Space M] [ContinuousMul M]
 
 @[to_additive]
 theorem prod_mul_tprod_nat_mul'
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Real.lean b/Mathlib/Topology/Algebra/InfiniteSum/Real.lean
index 12800c8af15fb..1ba9e35f1b1fc 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Real.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Real.lean
@@ -64,7 +64,7 @@ theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀
     Summable f ↔ ¬Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop := by
   rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]
 
-theorem summable_sigma_of_nonneg {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
+theorem summable_sigma_of_nonneg {α} {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
     Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩ := by
   lift f to (Σx, β x) → ℝ≥0 using hf
   exact mod_cast NNReal.summable_sigma
@@ -74,7 +74,7 @@ lemma summable_partition {α β : Type*} {f : β → ℝ} (hf : 0 ≤ f) {s : α
       (∀ j, Summable fun i : s j ↦ f i) ∧ Summable fun j ↦ ∑' i : s j, f i := by
   simpa only [← (Set.sigmaEquiv s hs).summable_iff] using summable_sigma_of_nonneg (fun _ ↦ hf _)
 
-theorem summable_prod_of_nonneg {f : (α × β) → ℝ} (hf : 0 ≤ f) :
+theorem summable_prod_of_nonneg {α β} {f : (α × β) → ℝ} (hf : 0 ≤ f) :
     Summable f ↔ (∀ x, Summable fun y ↦ f (x, y)) ∧ Summable fun x ↦ ∑' y, f (x, y) :=
   (Equiv.sigmaEquivProd _ _).summable_iff.symm.trans <| summable_sigma_of_nonneg fun _ ↦ hf _
 
diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean
index e50b1de578992..f4ca295850c70 100644
--- a/Mathlib/Topology/Algebra/Module/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Basic.lean
@@ -2076,9 +2076,6 @@ section
 /-! The next theorems cover the identification between `M ≃L[𝕜] M`and the group of units of the ring
 `M →L[R] M`. -/
 
-
-variable [TopologicalAddGroup M]
-
 /-- An invertible continuous linear map `f` determines a continuous equivalence from `M` to itself.
 -/
 def ofUnit (f : (M →L[R] M)ˣ) : M ≃L[R] M where
@@ -2273,7 +2270,7 @@ end
 section
 
 variable [Ring R]
-variable [AddCommGroup M] [TopologicalAddGroup M] [Module R M]
+variable [AddCommGroup M] [Module R M]
 variable [AddCommGroup M₂] [Module R M₂]
 
 @[simp]
diff --git a/Mathlib/Topology/ContinuousFunction/Compact.lean b/Mathlib/Topology/ContinuousFunction/Compact.lean
index 24fddb06c48a9..5257cc87a452a 100644
--- a/Mathlib/Topology/ContinuousFunction/Compact.lean
+++ b/Mathlib/Topology/ContinuousFunction/Compact.lean
@@ -429,7 +429,7 @@ of `C(X, E)` (i.e. locally uniform convergence). -/
 
 open TopologicalSpace
 
-variable {X : Type*} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X]
+variable {X : Type*} [TopologicalSpace X] [LocallyCompactSpace X]
 variable {E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
 
 theorem summable_of_locally_summable_norm {ι : Type*} {F : ι → C(X, E)}
diff --git a/Mathlib/Topology/ContinuousFunction/CompactlySupported.lean b/Mathlib/Topology/ContinuousFunction/CompactlySupported.lean
index a5e36fed1b6b0..d8d72123235af 100644
--- a/Mathlib/Topology/ContinuousFunction/CompactlySupported.lean
+++ b/Mathlib/Topology/ContinuousFunction/CompactlySupported.lean
@@ -437,8 +437,6 @@ theorem coe_comp_to_continuous_fun (f : C_c(γ, δ)) (g : β →co γ) : ((f.com
 theorem comp_id (f : C_c(γ, δ)) : f.comp (CocompactMap.id γ) = f :=
   ext fun _ => rfl
 
-variable [T2Space β]
-
 @[simp]
 theorem comp_assoc (f : C_c(γ, δ)) (g : β →co γ) (h : α →co β) :
     (f.comp g).comp h = f.comp (g.comp h) :=
diff --git a/Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean b/Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean
index c34d6f692c3d4..f02fe2b8cc5f7 100644
--- a/Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean
+++ b/Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean
@@ -57,7 +57,7 @@ lemma ext {f g : C(X, R)₀} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g
 @[simp]
 lemma coe_mk {f : C(X, R)} {h0 : f 0 = 0} : ⇑(mk f h0) = f := rfl
 
-lemma toContinuousMap_injective [Zero R] : Injective ((↑) : C(X, R)₀ → C(X, R)) :=
+lemma toContinuousMap_injective : Injective ((↑) : C(X, R)₀ → C(X, R)) :=
   fun _ _ h ↦ congr(.mk $(h) _)
 
 lemma range_toContinuousMap : range ((↑) : C(X, R)₀ → C(X, R)) = {f : C(X, R) | f 0 = 0} :=
diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean
index 9f33cbe774d18..21303dc60bf02 100644
--- a/Mathlib/Topology/Instances/AddCircle.lean
+++ b/Mathlib/Topology/Instances/AddCircle.lean
@@ -85,23 +85,24 @@ theorem continuous_left_toIocMod : ContinuousWithinAt (toIocMod hp a) (Iic x) x
     (continuous_sub_left _).continuousAt.comp_continuousWithinAt <|
       (continuous_right_toIcoMod _ _ _).comp continuous_neg.continuousWithinAt fun y => neg_le_neg
 
-variable {x} (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a)
+variable {x}
 
-theorem toIcoMod_eventuallyEq_toIocMod : toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a :=
+theorem toIcoMod_eventuallyEq_toIocMod (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a) :
+    toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a :=
   IsOpen.mem_nhds
       (by
         rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
         exact isOpen_iUnion fun i => isOpen_Ioo) <|
     (not_modEq_iff_toIcoMod_eq_toIocMod hp).1 <| not_modEq_iff_ne_mod_zmultiples.2 hx
 
-theorem continuousAt_toIcoMod : ContinuousAt (toIcoMod hp a) x :=
+theorem continuousAt_toIcoMod (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a) : ContinuousAt (toIcoMod hp a) x :=
   let h := toIcoMod_eventuallyEq_toIocMod hp a hx
   continuousAt_iff_continuous_left_right.2 <|
     ⟨(continuous_left_toIocMod hp a x).congr_of_eventuallyEq (h.filter_mono nhdsWithin_le_nhds)
         h.eq_of_nhds,
       continuous_right_toIcoMod hp a x⟩
 
-theorem continuousAt_toIocMod : ContinuousAt (toIocMod hp a) x :=
+theorem continuousAt_toIocMod (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a) : ContinuousAt (toIocMod hp a) x :=
   let h := toIcoMod_eventuallyEq_toIocMod hp a hx
   continuousAt_iff_continuous_left_right.2 <|
     ⟨continuous_left_toIocMod hp a x,
@@ -112,14 +113,14 @@ end Continuity
 
 /-- The "additive circle": `𝕜 ⧸ (ℤ ∙ p)`. See also `Circle` and `Real.angle`. -/
 @[nolint unusedArguments]
-abbrev AddCircle [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜) :=
+abbrev AddCircle [LinearOrderedAddCommGroup 𝕜] (p : 𝕜) :=
   𝕜 ⧸ zmultiples p
 
 namespace AddCircle
 
 section LinearOrderedAddCommGroup
 
-variable [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p : 𝕜)
+variable [LinearOrderedAddCommGroup 𝕜] (p : 𝕜)
 
 theorem coe_nsmul {n : ℕ} {x : 𝕜} : (↑(n • x) : AddCircle p) = n • (x : AddCircle p) :=
   rfl
@@ -160,7 +161,7 @@ theorem coe_add_period (x : 𝕜) : ((x + p : 𝕜) : AddCircle p) = x := by
   rw [coe_add, ← eq_sub_iff_add_eq', sub_self, coe_period]
 
 @[continuity, nolint unusedArguments]
-protected theorem continuous_mk' :
+protected theorem continuous_mk' [TopologicalSpace 𝕜] :
     Continuous (QuotientAddGroup.mk' (zmultiples p) : 𝕜 → AddCircle p) :=
   continuous_coinduced_rng
 
@@ -227,6 +228,8 @@ variable (p a)
 
 section Continuity
 
+variable [TopologicalSpace 𝕜]
+
 @[continuity]
 theorem continuous_equivIco_symm : Continuous (equivIco p a).symm :=
   continuous_quotient_mk'.comp continuous_subtype_val
@@ -235,14 +238,14 @@ theorem continuous_equivIco_symm : Continuous (equivIco p a).symm :=
 theorem continuous_equivIoc_symm : Continuous (equivIoc p a).symm :=
   continuous_quotient_mk'.comp continuous_subtype_val
 
-variable {x : AddCircle p} (hx : x ≠ a)
+variable [OrderTopology 𝕜] {x : AddCircle p}
 
-theorem continuousAt_equivIco : ContinuousAt (equivIco p a) x := by
+theorem continuousAt_equivIco (hx : x ≠ a) : ContinuousAt (equivIco p a) x := by
   induction x using QuotientAddGroup.induction_on
   rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
   exact (continuousAt_toIcoMod hp.out a hx).codRestrict _
 
-theorem continuousAt_equivIoc : ContinuousAt (equivIoc p a) x := by
+theorem continuousAt_equivIoc (hx : x ≠ a) : ContinuousAt (equivIoc p a) x := by
   induction x using QuotientAddGroup.induction_on
   rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]
   exact (continuousAt_toIocMod hp.out a hx).codRestrict _
@@ -304,7 +307,7 @@ end LinearOrderedAddCommGroup
 
 section LinearOrderedField
 
-variable [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p q : 𝕜)
+variable [LinearOrderedField 𝕜] (p q : 𝕜)
 
 /-- The rescaling equivalence between additive circles with different periods. -/
 def equivAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃+ AddCircle q :=
@@ -322,6 +325,9 @@ theorem equivAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
     (equivAddCircle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) :=
   rfl
 
+section
+variable [TopologicalSpace 𝕜] [OrderTopology 𝕜]
+
 /-- The rescaling homeomorphism between additive circles with different periods. -/
 def homeomorphAddCircle (hp : p ≠ 0) (hq : q ≠ 0) : AddCircle p ≃ₜ AddCircle q :=
   ⟨equivAddCircle p q hp hq,
@@ -337,6 +343,7 @@ theorem homeomorphAddCircle_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
 theorem homeomorphAddCircle_symm_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
     (homeomorphAddCircle p q hp hq).symm (x : 𝕜) = (x * (q⁻¹ * p) : 𝕜) :=
   rfl
+end
 
 variable [hp : Fact (0 < p)]
 
@@ -526,7 +533,7 @@ by the equivalence relation identifying the endpoints. -/
 
 namespace AddCircle
 
-variable [LinearOrderedAddCommGroup 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (p a : 𝕜)
+variable [LinearOrderedAddCommGroup 𝕜] (p a : 𝕜)
   [hp : Fact (0 < p)]
 
 local notation "𝕋" => AddCircle p
@@ -582,7 +589,7 @@ theorem equivIccQuot_comp_mk_eq_toIocMod :
 
 /-- The natural map from `[a, a + p] ⊂ 𝕜` with endpoints identified to `𝕜 / ℤ • p`, as a
 homeomorphism of topological spaces. -/
-def homeoIccQuot : 𝕋 ≃ₜ Quot (EndpointIdent p a) where
+def homeoIccQuot [TopologicalSpace 𝕜] [OrderTopology 𝕜] : 𝕋 ≃ₜ Quot (EndpointIdent p a) where
   toEquiv := equivIccQuot p a
   continuous_toFun := by
     -- Porting note: was `simp_rw`
@@ -615,23 +622,21 @@ theorem liftIco_eq_lift_Icc {f : 𝕜 → B} (h : f a = f (a + p)) :
         equivIccQuot p a :=
   rfl
 
+theorem liftIco_zero_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ico 0 p) : liftIco p 0 f ↑x = f x :=
+  liftIco_coe_apply (by rwa [zero_add])
+
+variable [TopologicalSpace 𝕜] [OrderTopology 𝕜]
+
 theorem liftIco_continuous [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p))
     (hc : ContinuousOn f <| Icc a (a + p)) : Continuous (liftIco p a f) := by
   rw [liftIco_eq_lift_Icc hf]
   refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun
   exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_restrict.mp hc)
 
-section ZeroBased
-
-theorem liftIco_zero_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ico 0 p) : liftIco p 0 f ↑x = f x :=
-  liftIco_coe_apply (by rwa [zero_add])
-
 theorem liftIco_zero_continuous [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p)
     (hc : ContinuousOn f <| Icc 0 p) : Continuous (liftIco p 0 f) :=
   liftIco_continuous (by rwa [zero_add] : f 0 = f (0 + p)) (by rwa [zero_add])
 
-end ZeroBased
-
 end AddCircle
 
 end IdentifyIccEnds
diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean
index 338cc5c4ba0ef..7d4f1adcd31f9 100644
--- a/Mathlib/Topology/Instances/ENNReal.lean
+++ b/Mathlib/Topology/Instances/ENNReal.lean
@@ -1290,7 +1290,7 @@ theorem Filter.Tendsto.edist {f g : β → α} {x : Filter β} {a b : α} (hf :
 
 /-- If the extended distance between consecutive points of a sequence is estimated
 by a summable series of `NNReal`s, then the original sequence is a Cauchy sequence. -/
-theorem cauchySeq_of_edist_le_of_summable [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ≥0)
+theorem cauchySeq_of_edist_le_of_summable {f : ℕ → α} (d : ℕ → ℝ≥0)
     (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : Summable d) : CauchySeq f := by
   refine EMetric.cauchySeq_iff_NNReal.2 fun ε εpos ↦ ?_
   -- Actually we need partial sums of `d` to be a Cauchy sequence.
diff --git a/Mathlib/Topology/MetricSpace/Gluing.lean b/Mathlib/Topology/MetricSpace/Gluing.lean
index 3c2c725c49738..41444fef866b6 100644
--- a/Mathlib/Topology/MetricSpace/Gluing.lean
+++ b/Mathlib/Topology/MetricSpace/Gluing.lean
@@ -103,6 +103,7 @@ theorem le_glueDist_inr_inl (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (x y) :
     ε ≤ glueDist Φ Ψ ε (.inr x) (.inl y) := by
   rw [glueDist_comm]; apply le_glueDist_inl_inr
 
+section
 variable [Nonempty Z]
 
 private theorem glueDist_triangle_inl_inr_inr (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (x : X) (y z : Y) :
@@ -145,6 +146,8 @@ private theorem glueDist_triangle (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
     apply glueDist_triangle_inl_inr_inl
     simpa only [abs_sub_comm]
 
+end
+
 private theorem eq_of_glueDist_eq_zero (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (ε0 : 0 < ε) :
     ∀ p q : X ⊕ Y, glueDist Φ Ψ ε p q = 0 → p = q
   | .inl x, .inl y, h => by rw [eq_of_dist_eq_zero h]
@@ -170,7 +173,7 @@ theorem Sum.mem_uniformity_iff_glueDist (hε : 0 < ε) (s : Set ((X ⊕ Y) × (X
 `Φ p` and `Φ q`, and between `Ψ p` and `Ψ q`, coincide up to `2 ε` where `ε > 0`, one can almost
 glue the two spaces `X` and `Y` along the images of `Φ` and `Ψ`, so that `Φ p` and `Ψ p` are
 at distance `ε`. -/
-def glueMetricApprox (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (ε0 : 0 < ε)
+def glueMetricApprox [Nonempty Z] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (ε0 : 0 < ε)
     (H : ∀ p q, |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε) : MetricSpace (X ⊕ Y) where
   dist := glueDist Φ Ψ ε
   dist_self := glueDist_self Φ Ψ ε