diff --git a/Mathlib/Algebra/Homology/Exact.lean b/Mathlib/Algebra/Homology/Exact.lean
index adf100f7c4e84..c99040273fea9 100644
--- a/Mathlib/Algebra/Homology/Exact.lean
+++ b/Mathlib/Algebra/Homology/Exact.lean
@@ -45,9 +45,7 @@ these results are found in `CategoryTheory/Abelian/Exact.lean`.
 
 universe v v₂ u u₂
 
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory CategoryTheory.Limits
 
 variable {V : Type u} [Category.{v} V]
 
@@ -56,8 +54,8 @@ variable [HasImages V]
 namespace CategoryTheory
 
 -- One nice feature of this definition is that we have
--- `epi f → exact g h → exact (f ≫ g) h` and `exact f g → mono h → exact f (g ≫ h)`,
--- which do not necessarily hold in a non-abelian category with the usual definition of `exact`.
+-- `Epi f → Exact g h → Exact (f ≫ g) h` and `Exact f g → Mono h → Exact f (g ≫ h)`,
+-- which do not necessarily hold in a non-abelian category with the usual definition of `Exact`.
 /-- Two morphisms `f : A ⟶ B`, `g : B ⟶ C` are called exact if `w : f ≫ g = 0` and the natural map
 `imageToKernel f g w : imageSubobject f ⟶ kernelSubobject g` is an epimorphism.
 
@@ -93,7 +91,8 @@ theorem Preadditive.exact_iff_homology_zero {A B C : V} (f : A ⟶ B) (g : B ⟶
     Exact f g ↔ ∃ w : f ≫ g = 0, Nonempty (homology f g w ≅ 0) :=
   ⟨fun h => ⟨h.w, ⟨by
     haveI := h.epi
-    exact cokernel.ofEpi _⟩⟩, fun h => by
+    exact cokernel.ofEpi _⟩⟩,
+   fun h => by
     obtain ⟨w, ⟨i⟩⟩ := h
     exact ⟨w, Preadditive.epi_of_cokernel_zero ((cancel_mono i.hom).mp (by ext))⟩⟩
 #align category_theory.preadditive.exact_iff_homology_zero CategoryTheory.Preadditive.exact_iff_homology_zero
diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean
index d8463fcefd30e..52203b09b27a1 100644
--- a/Mathlib/Algebra/Order/ToIntervalMod.lean
+++ b/Mathlib/Algebra/Order/ToIntervalMod.lean
@@ -515,7 +515,7 @@ def MemIooMod (b x : α) : Prop :=
 #align mem_Ioo_mod MemIooMod
 
 open List in
-theorem tFAE_memIooMod :
+theorem tfae_memIooMod :
     TFAE
       [MemIooMod a b x,
       toIcoMod a hb x = toIocMod a hb x,
@@ -538,21 +538,21 @@ theorem tFAE_memIooMod :
     conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul a hb x, h]
   · have h' := toIcoMod_mem_Ico a hb x
     exact fun h => ⟨_, h'.1.lt_of_ne' h, h'.2⟩
-#align tfae_mem_Ioo_mod tFAE_memIooMod
+#align tfae_mem_Ioo_mod tfae_memIooMod
 
 variable {a x}
 
 theorem memIooMod_iff_toIcoMod_eq_toIocMod : MemIooMod a b x ↔ toIcoMod a hb x = toIocMod a hb x :=
-  (tFAE_memIooMod a hb x).out 0 1
+  (tfae_memIooMod a hb x).out 0 1
 #align mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod memIooMod_iff_toIcoMod_eq_toIocMod
 
 theorem memIooMod_iff_toIcoMod_add_period_ne_toIocMod :
     MemIooMod a b x ↔ toIcoMod a hb x + b ≠ toIocMod a hb x :=
-  (tFAE_memIooMod a hb x).out 0 2
+  (tfae_memIooMod a hb x).out 0 2
 #align mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod memIooMod_iff_toIcoMod_add_period_ne_toIocMod
 
 theorem memIooMod_iff_toIcoMod_ne_left : MemIooMod a b x ↔ toIcoMod a hb x ≠ a :=
-  (tFAE_memIooMod a hb x).out 0 3
+  (tfae_memIooMod a hb x).out 0 3
 #align mem_Ioo_mod_iff_to_Ico_mod_ne_left memIooMod_iff_toIcoMod_ne_left
 
 theorem not_memIooMod_iff_toIcoMod_add_period_eq_toIocMod :
diff --git a/Mathlib/Analysis/Normed/Group/AddTorsor.lean b/Mathlib/Analysis/Normed/Group/AddTorsor.lean
index f7e947aebc7cd..f8dd4d4044e65 100644
--- a/Mathlib/Analysis/Normed/Group/AddTorsor.lean
+++ b/Mathlib/Analysis/Normed/Group/AddTorsor.lean
@@ -58,7 +58,7 @@ instance (priority := 100) SeminormedAddCommGroup.toNormedAddTorsor : NormedAddT
     where dist_eq_norm' := dist_eq_norm
 #align seminormed_add_comm_group.to_normed_add_torsor SeminormedAddCommGroup.toNormedAddTorsor
 
--- Because of the add_torsor.nonempty instance.
+-- Because of the AddTorsor.nonempty instance.
 /-- A nonempty affine subspace of a `NormedAddTorsor` is itself a `NormedAddTorsor`. -/
 instance AffineSubspace.toNormedAddTorsor {R : Type _} [Ring R] [Module R V]
     (s : AffineSubspace R P) [Nonempty s] : NormedAddTorsor s.direction s :=
@@ -176,11 +176,10 @@ def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [SeminormedA
     [AddTorsor V P] : PseudoMetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
   -- porting note: `edist_dist` is no longer an `autoParam`
-  edist_dist := fun p p' => by simp only [←ENNReal.ofReal_eq_coe_nnreal]
+  edist_dist _ _ := by simp only [←ENNReal.ofReal_eq_coe_nnreal]
   dist_self x := by simp
   dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
-  dist_triangle := by
-    intro x y z
+  dist_triangle x y z := by
     change ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
     rw [← vsub_add_vsub_cancel]
     apply norm_add_le
@@ -192,12 +191,11 @@ P`. -/
 def metricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [NormedAddCommGroup V]
     [AddTorsor V P] : MetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
-  edist_dist := fun p p' => by simp only; rw [ENNReal.ofReal_eq_coe_nnreal]
+  edist_dist _ _ := by simp only; rw [ENNReal.ofReal_eq_coe_nnreal]
   dist_self x := by simp
   eq_of_dist_eq_zero h := by simpa using h
   dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
-  dist_triangle := by
-    intro x y z
+  dist_triangle x y z := by
     change ‖x -ᵥ z‖ ≤ ‖x -ᵥ y‖ + ‖y -ᵥ z‖
     rw [← vsub_add_vsub_cancel]
     apply norm_add_le
@@ -231,8 +229,8 @@ theorem uniformContinuous_vsub : UniformContinuous fun x : P × P => x.1 -ᵥ x.
   (LipschitzWith.prod_fst.vsub LipschitzWith.prod_snd).uniformContinuous
 #align uniform_continuous_vsub uniformContinuous_vsub
 
-instance (priority := 100) NormedAddTorsor.to_continuousVAdd : ContinuousVAdd V P
-    where continuous_vadd := uniformContinuous_vadd.continuous
+instance (priority := 100) NormedAddTorsor.to_continuousVAdd : ContinuousVAdd V P where
+  continuous_vadd := uniformContinuous_vadd.continuous
 #align normed_add_torsor.to_has_continuous_vadd NormedAddTorsor.to_continuousVAdd
 
 theorem continuous_vsub : Continuous fun x : P × P => x.1 -ᵥ x.2 :=
diff --git a/Mathlib/CategoryTheory/Sites/Sheafification.lean b/Mathlib/CategoryTheory/Sites/Sheafification.lean
index 816a38e17af94..71363922c07bc 100644
--- a/Mathlib/CategoryTheory/Sites/Sheafification.lean
+++ b/Mathlib/CategoryTheory/Sites/Sheafification.lean
@@ -403,7 +403,6 @@ theorem exists_of_sep (P : Cᵒᵖ ⥤ D)
           exact hf)
   use e0, 𝟙 _
   ext IV
-  --dsimp only [Meq.refine_apply, Meq.pullback_apply, w]
   let IA : B.Arrow := ⟨_, (IV.f ≫ II.f) ≫ I.f,
     ⟨I.Y, _, _, I.hf, Sieve.downward_closed _ II.hf _, rfl⟩⟩
   let IB : S.Arrow := IA.fromMiddle
diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
index 8e7aa2a0b7fcd..2f74e3b1e96af 100644
--- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
+++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
@@ -25,8 +25,8 @@ $$
 exists and does not depend on `x`. This number is called the *translation number* of `f`.
 Different authors use different notation for this number: `τ`, `ρ`, `rot`, etc
 
-In this file we define a structure `circle_deg1_lift` for bundled maps with these properties, define
-translation number of `f : circle_deg1_lift`, prove some estimates relating `f^n(x)-x` to `τ(f)`. In
+In this file we define a structure `CircleDeg1Lift` for bundled maps with these properties, define
+translation number of `f : CircleDeg1Lift`, prove some estimates relating `f^n(x)-x` to `τ(f)`. In
 case of a continuous map `f` we also prove that `f` admits a point `x` such that `f^n(x)=x+m` if and
 only if `τ(f)=m/n`.
 
@@ -41,50 +41,50 @@ It does not depend on the choice of `a`.
 
 ## Main definitions
 
-* `circle_deg1_lift`: a monotone map `f : ℝ → ℝ` such that `f (x + 1) = f x + 1` for all `x`;
-  the type `circle_deg1_lift` is equipped with `lattice` and `monoid` structures; the
+* `CircleDeg1Lift`: a monotone map `f : ℝ → ℝ` such that `f (x + 1) = f x + 1` for all `x`;
+  the type `CircleDeg1Lift` is equipped with `Lattice` and `Monoid` structures; the
   multiplication is given by composition: `(f * g) x = f (g x)`.
-* `circle_deg1_lift.translation_number`: translation number of `f : circle_deg1_lift`.
+* `CircleDeg1Lift.translationNumber`: translation number of `f : CircleDeg1Lift`.
 
 ## Main statements
 
-We prove the following properties of `circle_deg1_lift.translation_number`.
+We prove the following properties of `CircleDeg1Lift.translationNumber`.
 
-* `circle_deg1_lift.translation_number_eq_of_dist_bounded`: if the distance between `(f^n) 0`
+* `CircleDeg1Lift.translationNumber_eq_of_dist_bounded`: if the distance between `(f^n) 0`
   and `(g^n) 0` is bounded from above uniformly in `n : ℕ`, then `f` and `g` have equal
   translation numbers.
 
-* `circle_deg1_lift.translation_number_eq_of_semiconj_by`: if two `circle_deg1_lift` maps `f`, `g`
-  are semiconjugate by a `circle_deg1_lift` map, then `τ f = τ g`.
+* `CircleDeg1Lift.translationNumber_eq_of_semiconjBy`: if two `CircleDeg1Lift` maps `f`, `g`
+  are semiconjugate by a `CircleDeg1Lift` map, then `τ f = τ g`.
 
-* `circle_deg1_lift.translation_number_units_inv`: if `f` is an invertible `circle_deg1_lift` map
+* `CircleDeg1Lift.translationNumber_units_inv`: if `f` is an invertible `CircleDeg1Lift` map
   (equivalently, `f` is a lift of an orientation-preserving circle homeomorphism), then
   the translation number of `f⁻¹` is the negative of the translation number of `f`.
 
-* `circle_deg1_lift.translation_number_mul_of_commute`: if `f` and `g` commute, then
+* `CircleDeg1Lift.translationNumber_mul_of_commute`: if `f` and `g` commute, then
   `τ (f * g) = τ f + τ g`.
 
-* `circle_deg1_lift.translation_number_eq_rat_iff`: the translation number of `f` is equal to
+* `CircleDeg1Lift.translationNumber_eq_rat_iff`: the translation number of `f` is equal to
   a rational number `m / n` if and only if `(f^n) x = x + m` for some `x`.
 
-* `circle_deg1_lift.semiconj_of_bijective_of_translation_number_eq`: if `f` and `g` are two
-  bijective `circle_deg1_lift` maps and their translation numbers are equal, then these
+* `CircleDeg1Lift.semiconj_of_bijective_of_translationNumber_eq`: if `f` and `g` are two
+  bijective `CircleDeg1Lift` maps and their translation numbers are equal, then these
   maps are semiconjugate to each other.
 
-* `circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq`: let `f₁` and `f₂` be
+* `CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq`: let `f₁` and `f₂` be
   two actions of a group `G` on the circle by degree 1 maps (formally, `f₁` and `f₂` are two
-  homomorphisms from `G →* circle_deg1_lift`). If the translation numbers of `f₁ g` and `f₂ g` are
+  homomorphisms from `G →* CircleDeg1Lift`). If the translation numbers of `f₁ g` and `f₂ g` are
   equal to each other for all `g : G`, then these two actions are semiconjugate by some `F :
-  circle_deg1_lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
+  CircleDeg1Lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
   d'homeomorphismes du cercle et cohomologie bornee][ghys87:groupes].
 
 ## Notation
 
-We use a local notation `τ` for the translation number of `f : circle_deg1_lift`.
+We use a local notation `τ` for the translation number of `f : CircleDeg1Lift`.
 
 ## Implementation notes
 
-We define the translation number of `f : circle_deg1_lift` to be the limit of the sequence
+We define the translation number of `f : CircleDeg1Lift` to be the limit of the sequence
 `(f ^ (2 ^ n)) 0 / (2 ^ n)`, then prove that `((f ^ n) x - x) / n` tends to this number for any `x`.
 This way it is much easier to prove that the limit exists and basic properties of the limit.
 
@@ -104,17 +104,17 @@ preserving circle homeomorphisms for two reasons:
 
 Here are some short-term goals.
 
-* Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use `units
-  circle_deg1_lift` for now, but it's better to have a dedicated type (or a typeclass?).
+* Introduce a structure or a typeclass for lifts of circle homeomorphisms. We use `Units
+  CircleDeg1Lift` for now, but it's better to have a dedicated type (or a typeclass?).
 
-* Prove that the `semiconj_by` relation on circle homeomorphisms is an equivalence relation.
+* Prove that the `SemiconjBy` relation on circle homeomorphisms is an equivalence relation.
 
-* Introduce `conditionally_complete_lattice` structure, use it in the proof of
-  `circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq`.
+* Introduce `ConditionallyCompleteLattice` structure, use it in the proof of
+  `CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq`.
 
 * Prove that the orbits of the irrational rotation are dense in the circle. Deduce that a
   homeomorphism with an irrational rotation is semiconjugate to the corresponding irrational
-  translation by a continuous `circle_deg1_lift`.
+  translation by a continuous `CircleDeg1Lift`.
 
 ## Tags
 
@@ -283,9 +283,9 @@ theorem commute_iff_commute {f g : CircleDeg1Lift} : Commute f g ↔ Function.Co
 -/
 
 
-/-- The map `y ↦ x + y` as a `circle_deg1_lift`. More precisely, we define a homomorphism from
-`multiplicative ℝ` to `circle_deg1_liftˣ`, so the translation by `x` is
-`translation (multiplicative.of_add x)`. -/
+/-- The map `y ↦ x + y` as a `CircleDeg1Lift`. More precisely, we define a homomorphism from
+`Multiplicative ℝ` to `CircleDeg1Liftˣ`, so the translation by `x` is
+`translation (Multiplicative.ofAdd x)`. -/
 def translate : Multiplicative ℝ →* CircleDeg1Liftˣ := MonoidHom.toHomUnits <|
   { toFun := fun x =>
       ⟨⟨fun y => Multiplicative.toAdd x + y, fun _ _ h => add_le_add_left h _⟩, fun _ =>
@@ -327,7 +327,7 @@ theorem translate_iterate (x : ℝ) (n : ℕ) :
 
 In this section we prove that `f` commutes with translations by an integer number.
 First we formulate these statements (for a natural or an integer number,
-addition on the left or on the right, addition or subtraction) using `function.commute`,
+addition on the left or on the right, addition or subtraction) using `Function.Commute`,
 then reformulate as `simp` lemmas `map_int_add` etc.
 -/
 
@@ -406,7 +406,7 @@ noncomputable instance : Lattice CircleDeg1Lift where
   sup f g :=
     { toFun := fun x => max (f x) (g x)
       monotone' := fun x y h => max_le_max (f.mono h) (g.mono h)
-      -- TODO: generalize to `monotone.max`
+      -- TODO: generalize to `Monotone.max`
       map_add_one' := fun x => by simp [max_add_add_right] }
   le f g := ∀ x, f x ≤ g x
   le_refl f x := le_refl (f x)
@@ -630,7 +630,7 @@ def transnumAuxSeq (n : ℕ) : ℝ :=
   (f ^ (2 ^ n : ℕ)) 0 / 2 ^ n
 #align circle_deg1_lift.transnum_aux_seq CircleDeg1Lift.transnumAuxSeq
 
-/-- The translation number of a `circle_deg1_lift`, $τ(f)=\lim_{n→∞}\frac{f^n(x)-x}{n}$. We use
+/-- The translation number of a `CircleDeg1Lift`, $τ(f)=\lim_{n→∞}\frac{f^n(x)-x}{n}$. We use
 an auxiliary sequence `\frac{f^{2^n}(0)}{2^n}` to define `τ(f)` because some proofs are simpler
 this way. -/
 def translationNumber : ℝ :=
@@ -640,7 +640,7 @@ def translationNumber : ℝ :=
 end
 
 -- mathport name: exprτ
--- TODO: choose two different symbols for `circle_deg1_lift.translation_number` and the future
+-- TODO: choose two different symbols for `CircleDeg1Lift.translationNumber` and the future
 -- `circle_mono_homeo.rotation_number`, then make them `localized notation`s
 local notation "τ" => translationNumber
 
@@ -960,9 +960,9 @@ theorem translationNumber_eq_rat_iff (hf : Continuous f) {m : ℤ} {n : ℕ} (hn
   exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)
 #align circle_deg1_lift.translation_number_eq_rat_iff CircleDeg1Lift.translationNumber_eq_rat_iff
 
-/-- Consider two actions `f₁ f₂ : G →* circle_deg1_lift` of a group on the real line by lifts of
+/-- Consider two actions `f₁ f₂ : G →* CircleDeg1Lift` of a group on the real line by lifts of
 orientation preserving circle homeomorphisms. Suppose that for each `g : G` the homeomorphisms
-`f₁ g` and `f₂ g` have equal rotation numbers. Then there exists `F : circle_deg1_lift`  such that
+`f₁ g` and `f₂ g` have equal rotation numbers. Then there exists `F : CircleDeg1Lift`  such that
 `F * f₁ g = f₂ g * F` for all `g : G`.
 
 This is a version of Proposition 5.4 from [Étienne Ghys, Groupes d'homeomorphismes du cercle et
@@ -985,7 +985,7 @@ theorem semiconj_of_group_action_of_forall_translationNumber_eq {G : Type _} [Gr
       _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 :=
         add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _
       _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]
-  -- We have a theorem about actions by `order_iso`, so we introduce auxiliary maps
+  -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
   -- to `ℝ ≃o ℝ`.
   set F₁ := toOrderIso.comp f₁.toHomUnits
   set F₂ := toOrderIso.comp f₂.toHomUnits
@@ -1002,7 +1002,7 @@ theorem semiconj_of_group_action_of_forall_translationNumber_eq {G : Type _} [Gr
 #align circle_deg1_lift.semiconj_of_group_action_of_forall_translation_number_eq CircleDeg1Lift.semiconj_of_group_action_of_forall_translationNumber_eq
 
 /-- If two lifts of circle homeomorphisms have the same translation number, then they are
-semiconjugate by a `circle_deg1_lift`. This version uses arguments `f₁ f₂ : circle_deg1_liftˣ`
+semiconjugate by a `CircleDeg1Lift`. This version uses arguments `f₁ f₂ : CircleDeg1Liftˣ`
 to assume that `f₁` and `f₂` are homeomorphisms. -/
 theorem units_semiconj_of_translationNumber_eq {f₁ f₂ : CircleDeg1Liftˣ} (h : τ f₁ = τ f₂) :
     ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
@@ -1015,7 +1015,7 @@ theorem units_semiconj_of_translationNumber_eq {f₁ f₂ : CircleDeg1Liftˣ} (h
 #align circle_deg1_lift.units_semiconj_of_translation_number_eq CircleDeg1Lift.units_semiconj_of_translationNumber_eq
 
 /-- If two lifts of circle homeomorphisms have the same translation number, then they are
-semiconjugate by a `circle_deg1_lift`. This version uses assumptions `is_unit f₁` and `is_unit f₂`
+semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `IsUnit f₁` and `IsUnit f₂`
 to assume that `f₁` and `f₂` are homeomorphisms. -/
 theorem semiconj_of_isUnit_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : IsUnit f₁)
     (h₂ : IsUnit f₂) (h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ := by
@@ -1024,7 +1024,7 @@ theorem semiconj_of_isUnit_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift}
 #align circle_deg1_lift.semiconj_of_is_unit_of_translation_number_eq CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq
 
 /-- If two lifts of circle homeomorphisms have the same translation number, then they are
-semiconjugate by a `circle_deg1_lift`. This version uses assumptions `bijective f₁` and
+semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `bijective f₁` and
 `bijective f₂` to assume that `f₁` and `f₂` are homeomorphisms. -/
 theorem semiconj_of_bijective_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : Bijective f₁)
     (h₂ : Bijective f₂) (h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
index 0b8d8bd4d2c34..2dca3174a995d 100644
--- a/Mathlib/Geometry/Manifold/ChartedSpace.lean
+++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -115,9 +115,7 @@ composition of local equivs with `≫`.
 
 noncomputable section
 
-open Classical Topology
-
-open Filter
+open Classical Topology Filter
 
 universe u
 
@@ -402,10 +400,10 @@ class ClosedUnderRestriction (G : StructureGroupoid H) : Prop where
     ∀ {e : LocalHomeomorph H H}, e ∈ G → ∀ s : Set H, IsOpen s → e.restr s ∈ G
 #align closed_under_restriction ClosedUnderRestriction
 
-theorem closed_under_restriction' {G : StructureGroupoid H} [ClosedUnderRestriction G]
+theorem closedUnderRestriction' {G : StructureGroupoid H} [ClosedUnderRestriction G]
     {e : LocalHomeomorph H H} (he : e ∈ G) {s : Set H} (hs : IsOpen s) : e.restr s ∈ G :=
   ClosedUnderRestriction.closedUnderRestriction he s hs
-#align closed_under_restriction' closed_under_restriction'
+#align closed_under_restriction' closedUnderRestriction'
 
 /-- The trivial restriction-closed groupoid, containing only local homeomorphisms equivalent to the
 restriction of the identity to the various open subsets. -/
@@ -460,7 +458,7 @@ theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) :
     apply StructureGroupoid.le_iff.mpr
     rintro e ⟨s, hs, hes⟩
     refine' G.eq_on_source _ hes
-    convert closed_under_restriction' G.id_mem hs
+    convert closedUnderRestriction' G.id_mem hs
     -- Porting note: was
     -- change s = _ ∩ _
     -- rw [hs.interior_eq]
@@ -1073,7 +1071,7 @@ instance [ClosedUnderRestriction G] : HasGroupoid s G where
     rw [hc'.symm, mem_singleton_iff] at he'
     rw [he, he']
     refine' G.eq_on_source _ (subtypeRestr_symm_trans_subtypeRestr s (chartAt x) (chartAt x'))
-    apply closed_under_restriction'
+    apply closedUnderRestriction'
     · exact G.compatible (chart_mem_atlas _) (chart_mem_atlas _)
     · exact preimage_open_of_open_symm (chartAt _) s.2
 
diff --git a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
index f7499b74d2bd2..00374fe1bcd51 100644
--- a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
+++ b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
@@ -574,7 +574,7 @@ theorem isLocalStructomorphWithinAt_localInvariantProp [ClosedUnderRestriction G
       · rintro h hx
         rcases h ⟨hx, hux⟩ with ⟨e, heG, hef, hex⟩
         refine' ⟨e.restr (interior u), _, _, _⟩
-        · exact closed_under_restriction' heG isOpen_interior
+        · exact closedUnderRestriction' heG isOpen_interior
         · have : s ∩ u ∩ e.source = s ∩ (e.source ∩ u) := by mfld_set_tac
           simpa only [this, interior_interior, hu.interior_eq, mfld_simps] using hef
         · simp only [*, interior_interior, hu.interior_eq, mfld_simps]
@@ -614,7 +614,7 @@ theorem _root_.LocalHomeomorph.isLocalStructomorphWithinAt_iff {G : StructureGro
   constructor
   · intro hf h2x
     obtain ⟨e, he, hfe, hxe⟩ := hf h2x
-    refine' ⟨e.restr f.source, closed_under_restriction' he f.open_source, _, _, hxe, _⟩
+    refine' ⟨e.restr f.source, closedUnderRestriction' he f.open_source, _, _, hxe, _⟩
     · simp_rw [LocalHomeomorph.restr_source]
       refine' (inter_subset_right _ _).trans interior_subset
     · intro x' hx'
@@ -676,7 +676,7 @@ theorem HasGroupoid.comp
         (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').open_source
       refine' ⟨_, hs.inter φ.open_source, _, _⟩
       · simp only [hx, hφ_dom, mfld_simps]
-      · refine' G₁.eq_on_source (closed_under_restriction' hφG₁ hs) _
+      · refine' G₁.eq_on_source (closedUnderRestriction' hφG₁ hs) _
         rw [LocalHomeomorph.restr_source_inter]
         refine' LocalHomeomorph.Set.EqOn.restr_eqOn_source (hφ.mono _)
         mfld_set_tac }
diff --git a/Mathlib/Logic/Equiv/TransferInstance.lean b/Mathlib/Logic/Equiv/TransferInstance.lean
index cd55018fc8b58..7aa3371bf9f95 100644
--- a/Mathlib/Logic/Equiv/TransferInstance.lean
+++ b/Mathlib/Logic/Equiv/TransferInstance.lean
@@ -334,7 +334,7 @@ protected def nonAssocSemiring [NonAssocSemiring β] : NonAssocSemiring α := by
   apply e.injective.nonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _
 #align equiv.non_assoc_semiring Equiv.nonAssocSemiring
 
-/-- Transfer `semiring` across an `Equiv` -/
+/-- Transfer `Semiring` across an `Equiv` -/
 @[reducible]
 protected def semiring [Semiring β] : Semiring α := by
   let mul := e.Mul
diff --git a/Mathlib/RingTheory/Valuation/Basic.lean b/Mathlib/RingTheory/Valuation/Basic.lean
index 938c6a5e10964..7bea0e5bb8228 100644
--- a/Mathlib/RingTheory/Valuation/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/Basic.lean
@@ -64,12 +64,10 @@ boilerplate lemmas to `ValuationClass`.
 -/
 
 
-open Classical BigOperators
+open Classical BigOperators Function Ideal
 
 noncomputable section
 
-open Function Ideal
-
 variable {K F R : Type _} [DivisionRing K]
 
 section
@@ -358,14 +356,9 @@ theorem one_lt_val_iff (v : Valuation K Γ₀) {x : K} (h : x ≠ 0) : 1 < v x 
 /-- The subgroup of elements whose valuation is less than a certain unit.-/
 def ltAddSubgroup (v : Valuation R Γ₀) (γ : Γ₀ˣ) : AddSubgroup R where
   carrier := { x | v x < γ }
-  zero_mem' := by
-    have h := Units.ne_zero γ
-    contrapose! h
-    simp at h
-  add_mem' := by
-    intros x y x_in y_in
-    exact lt_of_le_of_lt (v.map_add x y) (max_lt x_in y_in)
-  neg_mem' := by intros x x_in; rwa [Set.mem_setOf_eq, map_neg]
+  zero_mem' := by simp
+  add_mem' {x y} x_in y_in := lt_of_le_of_lt (v.map_add x y) (max_lt x_in y_in)
+  neg_mem' x_in := by rwa [Set.mem_setOf, map_neg]
 #align valuation.lt_add_subgroup Valuation.ltAddSubgroup
 
 end Group
@@ -423,13 +416,13 @@ end IsEquiv
 -- end of namespace
 section
 
-theorem IsEquiv_of_map_strictMono [LinearOrderedCommMonoidWithZero Γ₀]
+theorem isEquiv_of_map_strictMono [LinearOrderedCommMonoidWithZero Γ₀]
     [LinearOrderedCommMonoidWithZero Γ'₀] [Ring R] {v : Valuation R Γ₀} (f : Γ₀ →*₀ Γ'₀)
     (H : StrictMono f) : IsEquiv (v.map f H.monotone) v := fun _x _y =>
   ⟨H.le_iff_le.mp, fun h => H.monotone h⟩
-#align valuation.is_equiv_of_map_strict_mono Valuation.IsEquiv_of_map_strictMono
+#align valuation.is_equiv_of_map_strict_mono Valuation.isEquiv_of_map_strictMono
 
-theorem IsEquiv_of_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
+theorem isEquiv_of_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
     [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀)
     (h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1) : v.IsEquiv v' := by
   intro x y
@@ -447,22 +440,22 @@ theorem IsEquiv_of_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
     replace hy := v'.ne_zero_iff.mpr hy
     replace H := le_of_le_mul_right hy H
     rwa [h]
-#align valuation.is_equiv_of_val_le_one Valuation.IsEquiv_of_val_le_one
+#align valuation.is_equiv_of_val_le_one Valuation.isEquiv_of_val_le_one
 
-theorem IsEquiv_iff_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
+theorem isEquiv_iff_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
     [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
     v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1 :=
-  ⟨fun h x => by simpa using h x 1, IsEquiv_of_val_le_one _ _⟩
-#align valuation.is_equiv_iff_val_le_one Valuation.IsEquiv_iff_val_le_one
+  ⟨fun h x => by simpa using h x 1, isEquiv_of_val_le_one _ _⟩
+#align valuation.is_equiv_iff_val_le_one Valuation.isEquiv_iff_val_le_one
 
-theorem IsEquiv_iff_val_eq_one [LinearOrderedCommGroupWithZero Γ₀]
+theorem isEquiv_iff_val_eq_one [LinearOrderedCommGroupWithZero Γ₀]
     [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
     v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1 := by
   constructor
   · intro h x
     simpa using @IsEquiv.val_eq _ _ _ _ _ _ v v' h x 1
   · intro h
-    apply IsEquiv_of_val_le_one
+    apply isEquiv_of_val_le_one
     intro x
     constructor
     · intro hx
@@ -489,16 +482,16 @@ theorem IsEquiv_iff_val_eq_one [LinearOrderedCommGroupWithZero Γ₀]
         simp [this]
       · rw [← h] at hx'
         exact le_of_eq hx'
-#align valuation.is_equiv_iff_val_eq_one Valuation.IsEquiv_iff_val_eq_one
+#align valuation.is_equiv_iff_val_eq_one Valuation.isEquiv_iff_val_eq_one
 
-theorem IsEquiv_iff_val_lt_one [LinearOrderedCommGroupWithZero Γ₀]
+theorem isEquiv_iff_val_lt_one [LinearOrderedCommGroupWithZero Γ₀]
     [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
     v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1 := by
   constructor
   · intro h x
     simp only [lt_iff_le_and_ne,
-      and_congr ((IsEquiv_iff_val_le_one _ _).1 h) ((IsEquiv_iff_val_eq_one _ _).1 h).not]
-  · rw [IsEquiv_iff_val_eq_one]
+      and_congr ((isEquiv_iff_val_le_one _ _).1 h) ((isEquiv_iff_val_eq_one _ _).1 h).not]
+  · rw [isEquiv_iff_val_eq_one]
     intro h x
     by_cases hx : x = 0
     · -- porting note: this proof was `simp only [(zero_iff _).2 hx, zero_ne_one]`
@@ -519,25 +512,25 @@ theorem IsEquiv_iff_val_lt_one [LinearOrderedCommGroupWithZero Γ₀]
       | inr h_2 =>
         rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
         exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
-#align valuation.is_equiv_iff_val_lt_one Valuation.IsEquiv_iff_val_lt_one
+#align valuation.is_equiv_iff_val_lt_one Valuation.isEquiv_iff_val_lt_one
 
-theorem IsEquiv_iff_val_sub_one_lt_one [LinearOrderedCommGroupWithZero Γ₀]
+theorem isEquiv_iff_val_sub_one_lt_one [LinearOrderedCommGroupWithZero Γ₀]
     [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
     v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1 := by
-  rw [IsEquiv_iff_val_lt_one]
+  rw [isEquiv_iff_val_lt_one]
   exact (Equiv.subRight 1).surjective.forall
-#align valuation.is_equiv_iff_val_sub_one_lt_one Valuation.IsEquiv_iff_val_sub_one_lt_one
+#align valuation.is_equiv_iff_val_sub_one_lt_one Valuation.isEquiv_iff_val_sub_one_lt_one
 
-theorem IsEquiv_tFAE [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
+theorem isEquiv_tfae [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
     (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) :
     [v.IsEquiv v', ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x}, v x = 1 ↔ v' x = 1, ∀ {x}, v x < 1 ↔ v' x < 1,
         ∀ {x}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE := by
-  tfae_have 1 ↔ 2; · apply IsEquiv_iff_val_le_one
-  tfae_have 1 ↔ 3; · apply IsEquiv_iff_val_eq_one
-  tfae_have 1 ↔ 4; · apply IsEquiv_iff_val_lt_one
-  tfae_have 1 ↔ 5; · apply IsEquiv_iff_val_sub_one_lt_one
+  tfae_have 1 ↔ 2; · apply isEquiv_iff_val_le_one
+  tfae_have 1 ↔ 3; · apply isEquiv_iff_val_eq_one
+  tfae_have 1 ↔ 4; · apply isEquiv_iff_val_lt_one
+  tfae_have 1 ↔ 5; · apply isEquiv_iff_val_sub_one_lt_one
   tfae_finish
-#align valuation.is_equiv_tfae Valuation.IsEquiv_tFAE
+#align valuation.is_equiv_tfae Valuation.isEquiv_tfae
 
 end
 
@@ -553,12 +546,10 @@ variable (v : Valuation R Γ₀)
 def supp : Ideal R where
   carrier := { x | v x = 0 }
   zero_mem' := map_zero v
-  add_mem' := by
-    intros x y hx hy
-    exact le_zero_iff.mp <|
-      calc
-        v (x + y) ≤ max (v x) (v y) := v.map_add x y
-        _ ≤ 0 := max_le (le_zero_iff.mpr hx) (le_zero_iff.mpr hy)
+  add_mem' {x y} hx hy := le_zero_iff.mp <|
+    calc
+      v (x + y) ≤ max (v x) (v y) := v.map_add x y
+      _ ≤ 0 := max_le (le_zero_iff.mpr hx) (le_zero_iff.mpr hy)
   smul_mem' c x hx :=
     calc
       v (c * x) = v c * v x := map_mul v c x
@@ -573,24 +564,18 @@ theorem mem_supp_iff (x : R) : x ∈ supp v ↔ v x = 0 :=
 
 /-- The support of a valuation is a prime ideal. -/
 instance [Nontrivial Γ₀] [NoZeroDivisors Γ₀] : Ideal.IsPrime (supp v) :=
-  ⟨fun h : v.supp = ⊤ =>
-    one_ne_zero <|
-      show (1 : Γ₀) = 0 from
-        calc
-          1 = v 1 := v.map_one.symm
-          _ = 0 :=
-            show (1 : R) ∈ supp v by
-              rw [h]
-              trivial, by
-    intros x y hxy
-    show v x = 0 ∨ v y = 0
-    have hxy' : v (x * y) = 0 := hxy
-    rw [v.map_mul x y] at hxy'
-    exact eq_zero_or_eq_zero_of_mul_eq_zero hxy'⟩
+  ⟨fun h =>
+    one_ne_zero (α := Γ₀) <|
+      calc
+        1 = v 1 := v.map_one.symm
+        _ = 0 := by rw [←mem_supp_iff, h]; exact Submodule.mem_top,
+   fun {x y} hxy => by
+    simp only [mem_supp_iff] at hxy ⊢
+    rw [v.map_mul x y] at hxy
+    exact eq_zero_or_eq_zero_of_mul_eq_zero hxy⟩
 
 theorem map_add_supp (a : R) {s : R} (h : s ∈ supp v) : v (a + s) = v a := by
-  have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a :=
-    by
+  have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a := by
     intro a' s' h'
     refine' le_trans (v.map_add a' s') (max_le le_rfl _)
     simp [h']
@@ -600,13 +585,10 @@ theorem map_add_supp (a : R) {s : R} (h : s ∈ supp v) : v (a + s) = v a := by
     _ ≤ v (a + s) := aux (a + s) (-s) (by rwa [← Ideal.neg_mem_iff] at h)
 #align valuation.map_add_supp Valuation.map_add_supp
 
+set_option synthInstance.etaExperiment true in
 theorem comap_supp {S : Type _} [CommRing S] (f : S →+* R) :
-    -- Porting note: telling Lean where this instance is
-    supp (v.comap f) =
-      (@Ideal.comap S R (S →+* R) _ _ RingHom.instRingHomClassRingHom f v.supp : Ideal S) :=
-  Ideal.ext fun x => by
-    simp only [mem_supp_iff, Ideal.mem_comap, mem_supp_iff]
-    rfl
+    supp (v.comap f) = Ideal.comap f v.supp :=
+  Ideal.ext fun x => by rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]
 #align valuation.comap_supp Valuation.comap_supp
 
 end Supp
@@ -647,7 +629,7 @@ variable (f : R → Γ₀) (h0 : f 0 = ⊤) (h1 : f 1 = 0)
 
 variable (hadd : ∀ x y, min (f x) (f y) ≤ f (x + y)) (hmul : ∀ x y, f (x * y) = f x + f y)
 
-/-- An alternate constructor of `AddValuation`, that doesn't reference `multiplicative Γ₀ᵒᵈ` -/
+/-- An alternate constructor of `AddValuation`, that doesn't reference `Multiplicative Γ₀ᵒᵈ` -/
 def of : AddValuation R Γ₀ where
   toFun := f
   map_one' := h1
@@ -703,7 +685,7 @@ theorem map_add : ∀ (x y : R), min (v.asFun x) (v.asFun y) ≤ v.asFun (x + y)
 @[simp]
 theorem map_add' : ∀ (x y : R), v.asFun x ≤ v.asFun (x + y) ∨ v.asFun y ≤ v.asFun (x + y) := by
   intro x y
-  rw [←@min_le_iff _ _ (v.asFun x) (v.asFun y) (v.asFun (x+y)),←ge_iff_le]
+  rw [← @min_le_iff _ _ (v.asFun x) (v.asFun y) (v.asFun (x+y)), ← ge_iff_le]
   apply map_add
 
 theorem map_le_add {x y : R} {g : Γ₀} (hx : g ≤ v x) (hy : g ≤ v y) : g ≤ v (x + y) :=
diff --git a/Mathlib/Topology/MetricSpace/Closeds.lean b/Mathlib/Topology/MetricSpace/Closeds.lean
index e4b90c029d154..472078ba4fc11 100644
--- a/Mathlib/Topology/MetricSpace/Closeds.lean
+++ b/Mathlib/Topology/MetricSpace/Closeds.lean
@@ -75,13 +75,13 @@ set_option linter.uppercaseLean3 false in
 theorem isClosed_subsets_of_isClosed (hs : IsClosed s) :
     IsClosed { t : Closeds α | (t : Set α) ⊆ s } := by
   refine' isClosed_of_closure_subset fun t ht x hx => _
-  -- t : closeds α,  ht : t ∈ closure {t : closeds α | t ⊆ s},
+  -- t : Closeds α,  ht : t ∈ closure {t : Closeds α | t ⊆ s},
   -- x : α,  hx : x ∈ t
   -- goal : x ∈ s
   have : x ∈ closure s := by
     refine' mem_closure_iff.2 fun ε εpos => _
     rcases mem_closure_iff.1 ht ε εpos with ⟨u, hu, Dtu⟩
-    -- u : closeds α,  hu : u ∈ {t : closeds α | t ⊆ s},  hu' : edist t u < ε
+    -- u : Closeds α,  hu : u ∈ {t : Closeds α | t ⊆ s},  hu' : edist t u < ε
     rcases exists_edist_lt_of_hausdorffEdist_lt hx Dtu with ⟨y, hy, Dxy⟩
     -- y : α,  hy : y ∈ u, Dxy : edist x y < ε
     exact ⟨y, hu hy, Dxy⟩
@@ -189,8 +189,8 @@ instance Closeds.completeSpace [CompleteSpace α] : CompleteSpace (Closeds α) :
     ENNReal.Tendsto.const_mul
       (ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 <| by simp [ENNReal.one_lt_two]) (Or.inr <| by simp)
   rw [MulZeroClass.mul_zero] at this
-  obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b
-  exact ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop
+  obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b :=
+    ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop
   exact ⟨N, fun n hn => lt_of_le_of_lt (main n) (hN n hn)⟩
 #align emetric.closeds.complete_space EMetric.Closeds.completeSpace
 
@@ -208,7 +208,7 @@ instance Closeds.compactSpace [CompactSpace α] : CompactSpace (Closeds α) :=
     rcases EMetric.totallyBounded_iff.1
         (isCompact_iff_totallyBounded_isComplete.1 (@isCompact_univ α _ _)).1 δ δpos with
       ⟨s, fs, hs⟩
-    -- s : set α,  fs : s.finite,  hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ
+    -- s : Set α,  fs : s.Finite,  hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ
     -- we first show that any set is well approximated by a subset of `s`.
     have main : ∀ u : Set α, ∃ (v : _)(_ : v ⊆ s), hausdorffEdist u v ≤ δ := by
       intro u
@@ -431,7 +431,7 @@ theorem lipschitz_infDist : LipschitzWith 2 fun p : α × NonemptyCompacts α =>
   convert @LipschitzWith.uncurry α (NonemptyCompacts α) ℝ _ _ _
     (fun (x : α) (s : NonemptyCompacts α) => infDist x s) 1 1
     (fun s => lipschitz_infDist_pt ↑s) lipschitz_infDist_set
-  norm_cast
+  norm_num
 #align metric.lipschitz_inf_dist Metric.lipschitz_infDist
 
 theorem uniformContinuous_infDist_Hausdorff_dist :