From 21ea21123801afd7b2063f221df5dd3ba910411a Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Thu, 13 Jul 2023 15:05:14 +0200
Subject: [PATCH 1/3] chore: tidy various files

---
 Mathlib/Algebra/GCDMonoid/Finset.lean         |   4 +-
 Mathlib/Algebra/Hom/Centroid.lean             |  20 ++--
 Mathlib/Algebra/Order/Kleene.lean             |  14 +--
 Mathlib/Algebra/Ring/Prod.lean                |  49 ++++----
 .../Analysis/Convex/StrictConvexSpace.lean    |  41 +++----
 Mathlib/Analysis/Convex/Uniform.lean          |   2 +-
 Mathlib/Analysis/Normed/Field/Basic.lean      |   6 +-
 Mathlib/CategoryTheory/Groupoid.lean          |  35 +++---
 .../CategoryTheory/Groupoid/FreeGroupoid.lean |  13 ++-
 Mathlib/CategoryTheory/Opposites.lean         | 109 +++++++-----------
 Mathlib/Computability/Language.lean           |  28 ++---
 Mathlib/Data/List/Sigma.lean                  |  57 ++++-----
 Mathlib/RingTheory/Localization/AtPrime.lean  |  11 +-
 Mathlib/Topology/Algebra/MulAction.lean       |  14 +--
 14 files changed, 179 insertions(+), 224 deletions(-)

diff --git a/Mathlib/Algebra/GCDMonoid/Finset.lean b/Mathlib/Algebra/GCDMonoid/Finset.lean
index 54c67e13a2f43..79bbcdb463e9b 100644
--- a/Mathlib/Algebra/GCDMonoid/Finset.lean
+++ b/Mathlib/Algebra/GCDMonoid/Finset.lean
@@ -100,8 +100,8 @@ theorem lcm_union [DecidableEq β] : (s₁ ∪ s₂).lcm f = GCDMonoid.lcm (s₁
     fun a s _ ih ↦ by rw [insert_union, lcm_insert, lcm_insert, ih, lcm_assoc]
 #align finset.lcm_union Finset.lcm_union
 
-theorem lcm_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a)
-    : s₁.lcm f = s₂.lcm g := by
+theorem lcm_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
+    s₁.lcm f = s₂.lcm g := by
   subst hs
   exact Finset.fold_congr hfg
 #align finset.lcm_congr Finset.lcm_congr
diff --git a/Mathlib/Algebra/Hom/Centroid.lean b/Mathlib/Algebra/Hom/Centroid.lean
index 7d50ecefd9332..bdeda5c1b9169 100644
--- a/Mathlib/Algebra/Hom/Centroid.lean
+++ b/Mathlib/Algebra/Hom/Centroid.lean
@@ -88,8 +88,7 @@ section NonUnitalNonAssocSemiring
 
 variable [NonUnitalNonAssocSemiring α]
 
-instance : CentroidHomClass (CentroidHom α) α
-    where
+instance : CentroidHomClass (CentroidHom α) α where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
@@ -112,6 +111,7 @@ instance : CoeFun (CentroidHom α) fun _ ↦ α → α :=
 /- Porting note:
 `theorem to_fun_eq_coe {f : CentroidHom α} : f.toFun = (f : α → α) := rfl`
 removed because it is now a tautology -/
+#noalign centroid_hom.to_fun_eq_coe
 
 @[ext]
 theorem ext {f g : CentroidHom α} (h : ∀ a, f a = g a) : f = g :=
@@ -272,9 +272,7 @@ instance hasNsmul : SMul ℕ (CentroidHom α) :=
 
 instance hasNpowNat : Pow (CentroidHom α) ℕ :=
   ⟨fun f n ↦
-    { (f.toEnd ^ n :
-        AddMonoid.End
-          α) with
+    { (f.toEnd ^ n : AddMonoid.End α) with
       map_mul_left' := fun a b ↦ by
         induction' n with n ih
         · exact rfl
@@ -431,10 +429,7 @@ instance : Sub (CentroidHom α) :=
 
 instance hasZsmul : SMul ℤ (CentroidHom α) :=
   ⟨fun n f ↦
-    {
-      (SMul.smul n f :
-        α →+
-          α) with
+    { (SMul.smul n f : α →+ α) with
       map_mul_left' := fun a b ↦ by
         change n • f (a * b) = a * n • f b
         rw [map_mul_left f, ← mul_smul_comm]
@@ -470,8 +465,7 @@ theorem toEnd_zsmul (x : CentroidHom α) (n : ℤ) : (n • x).toEnd = n • x.t
 #align centroid_hom.to_End_zsmul CentroidHom.toEnd_zsmul
 
 instance : AddCommGroup (CentroidHom α) :=
-  toEnd_injective.addCommGroup _ toEnd_zero toEnd_add toEnd_neg toEnd_sub toEnd_nsmul
-    toEnd_zsmul
+  toEnd_injective.addCommGroup _ toEnd_zero toEnd_add toEnd_neg toEnd_sub toEnd_nsmul toEnd_zsmul
 
 @[simp, norm_cast]
 theorem coe_neg (f : CentroidHom α) : ⇑(-f) = -f :=
@@ -498,7 +492,7 @@ theorem toEnd_int_cast (z : ℤ) : (z : CentroidHom α).toEnd = ↑z :=
   rfl
 #align centroid_hom.to_End_int_cast CentroidHom.toEnd_int_cast
 
-instance : Ring (CentroidHom α) :=
+instance ring : Ring (CentroidHom α) :=
   toEnd_injective.ring _ toEnd_zero toEnd_one toEnd_add toEnd_mul toEnd_neg toEnd_sub
     toEnd_nsmul toEnd_zsmul toEnd_pow toEnd_nat_cast toEnd_int_cast
 
@@ -513,7 +507,7 @@ variable [NonUnitalRing α]
 /-- A prime associative ring has commutative centroid. -/
 @[reducible]
 def commRing (h : ∀ a b : α, (∀ r : α, a * r * b = 0) → a = 0 ∨ b = 0) : CommRing (CentroidHom α) :=
-  { CentroidHom.instRingCentroidHomToNonUnitalNonAssocSemiring with
+  { CentroidHom.ring with
     mul_comm := fun f g ↦ by
       ext
       refine' sub_eq_zero.1 ((or_self_iff _).1 <| (h _ _) fun r ↦ _)
diff --git a/Mathlib/Algebra/Order/Kleene.lean b/Mathlib/Algebra/Order/Kleene.lean
index 7d67ea01879c6..d41328b175f7d 100644
--- a/Mathlib/Algebra/Order/Kleene.lean
+++ b/Mathlib/Algebra/Order/Kleene.lean
@@ -290,17 +290,17 @@ end KleeneAlgebra
 
 namespace Prod
 
-instance [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β) :=
-  { Prod.instSemiringProd, Prod.semilatticeSup _ _, Prod.orderBot _ _ with
+instance instIdemSemiring [IdemSemiring α] [IdemSemiring β] : IdemSemiring (α × β) :=
+  { Prod.instSemiring, Prod.semilatticeSup _ _, Prod.orderBot _ _ with
     add_eq_sup := fun _ _ ↦ ext (add_eq_sup _ _) (add_eq_sup _ _) }
 
 instance [IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β) :=
-  { Prod.instCommSemiringProd, Prod.instIdemSemiringProd with }
+  { Prod.instCommSemiring, Prod.instIdemSemiring with }
 
 variable [KleeneAlgebra α] [KleeneAlgebra β]
 
 instance : KleeneAlgebra (α × β) :=
-  { Prod.instIdemSemiringProd with
+  { Prod.instIdemSemiring with
     kstar := fun a ↦ (a.1∗, a.2∗)
     one_le_kstar := fun _ ↦ ⟨one_le_kstar, one_le_kstar⟩
     mul_kstar_le_kstar := fun _ ↦ ⟨mul_kstar_le_kstar, mul_kstar_le_kstar⟩
@@ -326,17 +326,17 @@ end Prod
 
 namespace Pi
 
-instance [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
+instance instIdemSemiring [∀ i, IdemSemiring (π i)] : IdemSemiring (∀ i, π i) :=
   { Pi.semiring, Pi.semilatticeSup, Pi.orderBot with
     add_eq_sup := fun _ _ ↦ funext fun _ ↦ add_eq_sup _ _ }
 
 instance [∀ i, IdemCommSemiring (π i)] : IdemCommSemiring (∀ i, π i) :=
-  { Pi.commSemiring, Pi.instIdemSemiringForAll with }
+  { Pi.commSemiring, Pi.instIdemSemiring with }
 
 variable [∀ i, KleeneAlgebra (π i)]
 
 instance : KleeneAlgebra (∀ i, π i) :=
-  { Pi.instIdemSemiringForAll with
+  { Pi.instIdemSemiring with
     kstar := fun a i ↦ (a i)∗
     one_le_kstar := fun _ _ ↦ one_le_kstar
     mul_kstar_le_kstar := fun _ _ ↦ mul_kstar_le_kstar
diff --git a/Mathlib/Algebra/Ring/Prod.lean b/Mathlib/Algebra/Ring/Prod.lean
index 61434281a3774..5570df0e83a63 100644
--- a/Mathlib/Algebra/Ring/Prod.lean
+++ b/Mathlib/Algebra/Ring/Prod.lean
@@ -33,67 +33,72 @@ variable {α β R R' S S' T T' : Type _}
 namespace Prod
 
 /-- Product of two distributive types is distributive. -/
-instance [Distrib R] [Distrib S] : Distrib (R × S) :=
+instance instDistrib [Distrib R] [Distrib S] : Distrib (R × S) :=
   { left_distrib := fun _ _ _ => mk.inj_iff.mpr ⟨left_distrib _ _ _, left_distrib _ _ _⟩
     right_distrib := fun _ _ _ => mk.inj_iff.mpr ⟨right_distrib _ _ _, right_distrib _ _ _⟩ }
 
 /-- Product of two `NonUnitalNonAssocSemiring`s is a `NonUnitalNonAssocSemiring`. -/
-instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
+instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
     NonUnitalNonAssocSemiring (R × S) :=
   { inferInstanceAs (AddCommMonoid (R × S)),
     inferInstanceAs (Distrib (R × S)),
     inferInstanceAs (MulZeroClass (R × S)) with }
 
 /-- Product of two `NonUnitalSemiring`s is a `NonUnitalSemiring`. -/
-instance [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S) :=
+instance instNonUnitalSemiring [NonUnitalSemiring R] [NonUnitalSemiring S] :
+    NonUnitalSemiring (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
     inferInstanceAs (SemigroupWithZero (R × S)) with }
 
 /-- Product of two `NonAssocSemiring`s is a `NonAssocSemiring`. -/
-instance [NonAssocSemiring R] [NonAssocSemiring S] : NonAssocSemiring (R × S) :=
+instance instNonAssocSemiring [NonAssocSemiring R] [NonAssocSemiring S] :
+    NonAssocSemiring (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
     inferInstanceAs (MulZeroOneClass (R × S)),
     inferInstanceAs (AddMonoidWithOne (R × S)) with }
 
 /-- Product of two semirings is a semiring. -/
-instance [Semiring R] [Semiring S] : Semiring (R × S) :=
+instance instSemiring [Semiring R] [Semiring S] : Semiring (R × S) :=
   { inferInstanceAs (NonUnitalSemiring (R × S)),
     inferInstanceAs (NonAssocSemiring (R × S)),
     inferInstanceAs (MonoidWithZero (R × S)) with }
 
 /-- Product of two `NonUnitalCommSemiring`s is a `NonUnitalCommSemiring`. -/
-instance [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] : NonUnitalCommSemiring (R × S) :=
+instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] :
+    NonUnitalCommSemiring (R × S) :=
   { inferInstanceAs (NonUnitalSemiring (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
 
 /-- Product of two commutative semirings is a commutative semiring. -/
-instance [CommSemiring R] [CommSemiring S] : CommSemiring (R × S) :=
+instance instCommSemiring [CommSemiring R] [CommSemiring S] : CommSemiring (R × S) :=
   { inferInstanceAs (Semiring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }
 
-instance [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] : NonUnitalNonAssocRing (R × S) :=
+instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] :
+    NonUnitalNonAssocRing (R × S) :=
   { inferInstanceAs (AddCommGroup (R × S)),
     inferInstanceAs (NonUnitalNonAssocSemiring (R × S)) with }
 
-instance [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S) :=
+instance instNonUnitalRing [NonUnitalRing R] [NonUnitalRing S] : NonUnitalRing (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocRing (R × S)),
     inferInstanceAs (NonUnitalSemiring (R × S)) with }
 
-instance [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S) :=
+instance instNonAssocRing [NonAssocRing R] [NonAssocRing S] : NonAssocRing (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocRing (R × S)),
     inferInstanceAs (NonAssocSemiring (R × S)),
     inferInstanceAs (AddGroupWithOne (R × S)) with }
 
 /-- Product of two rings is a ring. -/
-instance [Ring R] [Ring S] : Ring (R × S) :=
+instance instRing [Ring R] [Ring S] : Ring (R × S) :=
   { inferInstanceAs (Semiring (R × S)),
     inferInstanceAs (AddCommGroup (R × S)),
     inferInstanceAs (AddGroupWithOne (R × S)) with }
 
 /-- Product of two `NonUnitalCommRing`s is a `NonUnitalCommRing`. -/
-instance [NonUnitalCommRing R] [NonUnitalCommRing S] : NonUnitalCommRing (R × S) :=
+instance instNonUnitalCommRing [NonUnitalCommRing R] [NonUnitalCommRing S] :
+    NonUnitalCommRing (R × S) :=
   { inferInstanceAs (NonUnitalRing (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
 
 /-- Product of two commutative rings is a commutative ring. -/
-instance [CommRing R] [CommRing S] : CommRing (R × S) :=
+instance instCommRing [CommRing R] [CommRing S] : CommRing (R × S) :=
   { inferInstanceAs (Ring (R × S)), inferInstanceAs (CommMonoid (R × S)) with }
 
 end Prod
@@ -162,7 +167,7 @@ variable [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnita
 
 variable (f : R →ₙ+* R') (g : S →ₙ+* S')
 
-/-- `prod.map` as a `NonUnitalRingHom`. -/
+/-- `Prod.map` as a `NonUnitalRingHom`. -/
 def prodMap : R × S →ₙ+* R' × S' :=
   (f.comp (fst R S)).prod (g.comp (snd R S))
 #align non_unital_ring_hom.prod_map NonUnitalRingHom.prodMap
@@ -282,26 +287,26 @@ def prodComm : R × S ≃+* S × R :=
 #align ring_equiv.prod_comm RingEquiv.prodComm
 
 @[simp]
-theorem coe_prod_comm : ⇑(prodComm : R × S ≃+* S × R) = Prod.swap :=
+theorem coe_prodComm : ⇑(prodComm : R × S ≃+* S × R) = Prod.swap :=
   rfl
-#align ring_equiv.coe_prod_comm RingEquiv.coe_prod_comm
+#align ring_equiv.coe_prod_comm RingEquiv.coe_prodComm
 
 @[simp]
-theorem coe_prod_comm_symm : ⇑(prodComm : R × S ≃+* S × R).symm = Prod.swap :=
+theorem coe_prodComm_symm : ⇑(prodComm : R × S ≃+* S × R).symm = Prod.swap :=
   rfl
-#align ring_equiv.coe_prod_comm_symm RingEquiv.coe_prod_comm_symm
+#align ring_equiv.coe_prod_comm_symm RingEquiv.coe_prodComm_symm
 
 @[simp]
-theorem fst_comp_coe_prod_comm :
+theorem fst_comp_coe_prodComm :
     (RingHom.fst S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.snd R S :=
   RingHom.ext fun _ => rfl
-#align ring_equiv.fst_comp_coe_prod_comm RingEquiv.fst_comp_coe_prod_comm
+#align ring_equiv.fst_comp_coe_prod_comm RingEquiv.fst_comp_coe_prodComm
 
 @[simp]
-theorem snd_comp_coe_prod_comm :
+theorem snd_comp_coe_prodComm :
     (RingHom.snd S R).comp ↑(prodComm : R × S ≃+* S × R) = RingHom.fst R S :=
   RingHom.ext fun _ => rfl
-#align ring_equiv.snd_comp_coe_prod_comm RingEquiv.snd_comp_coe_prod_comm
+#align ring_equiv.snd_comp_coe_prod_comm RingEquiv.snd_comp_coe_prodComm
 
 section
 
diff --git a/Mathlib/Analysis/Convex/StrictConvexSpace.lean b/Mathlib/Analysis/Convex/StrictConvexSpace.lean
index a68ac7f76f193..90913dfd91e12 100644
--- a/Mathlib/Analysis/Convex/StrictConvexSpace.lean
+++ b/Mathlib/Analysis/Convex/StrictConvexSpace.lean
@@ -44,10 +44,10 @@ In a strictly convex space, we prove
 
 We also provide several lemmas that can be used as alternative constructors for `StrictConvex ℝ E`:
 
-- `StrictConvexSpace.ofStrictConvexClosedUnitBall`: if `closed_ball (0 : E) 1` is strictly
+- `StrictConvexSpace.of_strictConvex_closed_unit_ball`: if `closed_ball (0 : E) 1` is strictly
   convex, then `E` is a strictly convex space;
 
-- `StrictConvexSpace.ofNormAdd`: if `‖x + y‖ = ‖x‖ + ‖y‖` implies `SameRay ℝ x y` for all
+- `StrictConvexSpace.of_norm_add`: if `‖x + y‖ = ‖x‖ + ‖y‖` implies `SameRay ℝ x y` for all
   nonzero `x y : E`, then `E` is a strictly convex space.
 
 ## Implementation notes
@@ -69,7 +69,7 @@ open Convex Pointwise
 require balls of positive radius with center at the origin to be strictly convex in the definition,
 then prove that any closed ball is strictly convex in `strictConvex_closedBall` below.
 
-See also `StrictConvexSpace.ofStrictConvexClosedUnitBall`. -/
+See also `StrictConvexSpace.of_strictConvex_closed_unit_ball`. -/
 class StrictConvexSpace (𝕜 E : Type _) [NormedLinearOrderedField 𝕜] [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] : Prop where
   strictConvex_closedBall : ∀ r : ℝ, 0 < r → StrictConvex 𝕜 (closedBall (0 : E) r)
@@ -90,19 +90,19 @@ theorem strictConvex_closedBall [StrictConvexSpace 𝕜 E] (x : E) (r : ℝ) :
 variable [NormedSpace ℝ E]
 
 /-- A real normed vector space is strictly convex provided that the unit ball is strictly convex. -/
-theorem StrictConvexSpace.ofStrictConvexClosedUnitBall [LinearMap.CompatibleSMul E E 𝕜 ℝ]
+theorem StrictConvexSpace.of_strictConvex_closed_unit_ball [LinearMap.CompatibleSMul E E 𝕜 ℝ]
     (h : StrictConvex 𝕜 (closedBall (0 : E) 1)) : StrictConvexSpace 𝕜 E :=
   ⟨fun r hr => by simpa only [smul_closedUnitBall_of_nonneg hr.le] using h.smul r⟩
-#align strict_convex_space.of_strict_convex_closed_unit_ball StrictConvexSpace.ofStrictConvexClosedUnitBall
+#align strict_convex_space.of_strict_convex_closed_unit_ball StrictConvexSpace.of_strictConvex_closed_unit_ball
 
 /-- Strict convexity is equivalent to `‖a • x + b • y‖ < 1` for all `x` and `y` of norm at most `1`
 and all strictly positive `a` and `b` such that `a + b = 1`. This lemma shows that it suffices to
 check this for points of norm one and some `a`, `b` such that `a + b = 1`. -/
-theorem StrictConvexSpace.ofNormComboLtOne
+theorem StrictConvexSpace.of_norm_combo_lt_one
     (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, a + b = 1 ∧ ‖a • x + b • y‖ < 1) :
     StrictConvexSpace ℝ E := by
   refine'
-    StrictConvexSpace.ofStrictConvexClosedUnitBall ℝ
+    StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ
       ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => _)
   rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball,
     mem_sphere_zero_iff_norm] at hx hy
@@ -110,45 +110,46 @@ theorem StrictConvexSpace.ofNormComboLtOne
   use b
   rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
     sub_eq_iff_eq_add.2 hab.symm]
-#align strict_convex_space.of_norm_combo_lt_one StrictConvexSpace.ofNormComboLtOne
+#align strict_convex_space.of_norm_combo_lt_one StrictConvexSpace.of_norm_combo_lt_one
 
-theorem StrictConvexSpace.ofNormComboNeOne
+theorem StrictConvexSpace.of_norm_combo_ne_one
     (h :
       ∀ x y : E,
         ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) :
     StrictConvexSpace ℝ E := by
-  refine' StrictConvexSpace.ofStrictConvexClosedUnitBall ℝ ((convex_closedBall _ _).strictConvex _)
+  refine' StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ
+    ((convex_closedBall _ _).strictConvex _)
   simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise,
     frontier_closedBall _ one_ne_zero, mem_sphere_zero_iff_norm]
   intro x hx y hy hne
   rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩
   exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩
-#align strict_convex_space.of_norm_combo_ne_one StrictConvexSpace.ofNormComboNeOne
+#align strict_convex_space.of_norm_combo_ne_one StrictConvexSpace.of_norm_combo_ne_one
 
-theorem StrictConvexSpace.ofNormAddNeTwo
+theorem StrictConvexSpace.of_norm_add_ne_two
     (h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E := by
   refine'
-    StrictConvexSpace.ofNormComboNeOne fun x y hx hy hne =>
+    StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
       ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, _⟩
   rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne.def,
     div_eq_one_iff_eq (two_ne_zero' ℝ)]
   exact h hx hy hne
-#align strict_convex_space.of_norm_add_ne_two StrictConvexSpace.ofNormAddNeTwo
+#align strict_convex_space.of_norm_add_ne_two StrictConvexSpace.of_norm_add_ne_two
 
-theorem StrictConvexSpace.ofPairwiseSphereNormNeTwo
+theorem StrictConvexSpace.of_pairwise_sphere_norm_ne_two
     (h : (sphere (0 : E) 1).Pairwise fun x y => ‖x + y‖ ≠ 2) : StrictConvexSpace ℝ E :=
-  StrictConvexSpace.ofNormAddNeTwo fun _ _ hx hy =>
+  StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy =>
     h (mem_sphere_zero_iff_norm.2 hx) (mem_sphere_zero_iff_norm.2 hy)
-#align strict_convex_space.of_pairwise_sphere_norm_ne_two StrictConvexSpace.ofPairwiseSphereNormNeTwo
+#align strict_convex_space.of_pairwise_sphere_norm_ne_two StrictConvexSpace.of_pairwise_sphere_norm_ne_two
 
 /-- If `‖x + y‖ = ‖x‖ + ‖y‖` implies that `x y : E` are in the same ray, then `E` is a strictly
 convex space. See also a more -/
-theorem StrictConvexSpace.ofNormAdd
+theorem StrictConvexSpace.of_norm_add
     (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) : StrictConvexSpace ℝ E := by
-  refine' StrictConvexSpace.ofPairwiseSphereNormNeTwo fun x hx y hy => mt fun h₂ => _
+  refine' StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => _
   rw [mem_sphere_zero_iff_norm] at hx hy
   exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)
-#align strict_convex_space.of_norm_add StrictConvexSpace.ofNormAdd
+#align strict_convex_space.of_norm_add StrictConvexSpace.of_norm_add
 
 variable [StrictConvexSpace ℝ E] {x y z : E} {a b r : ℝ}
 
diff --git a/Mathlib/Analysis/Convex/Uniform.lean b/Mathlib/Analysis/Convex/Uniform.lean
index 29eda3c9d3609..dbae43c6ed628 100644
--- a/Mathlib/Analysis/Convex/Uniform.lean
+++ b/Mathlib/Analysis/Convex/Uniform.lean
@@ -134,7 +134,7 @@ variable [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E]
 
 -- See note [lower instance priority]
 instance (priority := 100) UniformConvexSpace.toStrictConvexSpace : StrictConvexSpace ℝ E :=
-  StrictConvexSpace.ofNormAddNeTwo fun _ _ hx hy hxy =>
+  StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy hxy =>
     let ⟨_, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy)
     ((h hx.le hy.le le_rfl).trans_lt <| sub_lt_self _ hδ).ne
 #align uniform_convex_space.to_strict_convex_space UniformConvexSpace.toStrictConvexSpace
diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean
index 2898ed0af2385..768e752db4452 100644
--- a/Mathlib/Analysis/Normed/Field/Basic.lean
+++ b/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -242,7 +242,7 @@ instance ULift.nonUnitalSeminormedRing : NonUnitalSeminormedRing (ULift α) :=
   using the sup norm. -/
 instance Prod.nonUnitalSeminormedRing [NonUnitalSeminormedRing β] :
     NonUnitalSeminormedRing (α × β) :=
-  { Prod.seminormedAddCommGroup, instNonUnitalRingProd with
+  { seminormedAddCommGroup, instNonUnitalRing with
     norm_mul := fun x y =>
       calc
         ‖x * y‖ = ‖(x.1 * y.1, x.2 * y.2)‖ := rfl
@@ -393,7 +393,7 @@ instance ULift.seminormedRing : SeminormedRing (ULift α) :=
 /-- Seminormed ring structure on the product of two seminormed rings,
   using the sup norm. -/
 instance Prod.seminormedRing [SeminormedRing β] : SeminormedRing (α × β) :=
-  { Prod.nonUnitalSeminormedRing, instRingProd with }
+  { nonUnitalSeminormedRing, instRing with }
 #align prod.semi_normed_ring Prod.seminormedRing
 
 /-- Seminormed ring structure on the product of finitely many seminormed rings,
@@ -452,7 +452,7 @@ instance ULift.normedRing : NormedRing (ULift α) :=
 
 /-- Normed ring structure on the product of two normed rings, using the sup norm. -/
 instance Prod.normedRing [NormedRing β] : NormedRing (α × β) :=
-  { Prod.nonUnitalNormedRing, instRingProd with }
+  { nonUnitalNormedRing, instRing with }
 #align prod.normed_ring Prod.normedRing
 
 /-- Normed ring structure on the product of finitely many normed rings, using the sup norm. -/
diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean
index e165c8344f1b4..29b23b9e8548d 100644
--- a/Mathlib/CategoryTheory/Groupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid.lean
@@ -86,8 +86,7 @@ def Groupoid.invEquiv : (X ⟶ Y) ≃ (Y ⟶ X) :=
   ⟨Groupoid.inv, Groupoid.inv, fun f => by simp, fun f => by simp⟩
 #align category_theory.groupoid.inv_equiv CategoryTheory.Groupoid.invEquiv
 
-instance (priority := 100) groupoidHasInvolutiveReverse : Quiver.HasInvolutiveReverse C
-    where
+instance (priority := 100) groupoidHasInvolutiveReverse : Quiver.HasInvolutiveReverse C where
   reverse' f := Groupoid.inv f
   inv' f := by
     dsimp [Quiver.reverse]
@@ -99,18 +98,16 @@ theorem Groupoid.reverse_eq_inv (f : X ⟶ Y) : Quiver.reverse f = Groupoid.inv
   rfl
 #align category_theory.groupoid.reverse_eq_inv CategoryTheory.Groupoid.reverse_eq_inv
 
-instance functorMapReverse {D : Type _} [Groupoid D] (F : C ⥤ D) : F.toPrefunctor.MapReverse
-    where
-      map_reverse' f := by
-        simp only [Quiver.reverse, Quiver.HasReverse.reverse', Groupoid.inv_eq_inv,
-          Functor.map_inv]
+instance functorMapReverse {D : Type _} [Groupoid D] (F : C ⥤ D) : F.toPrefunctor.MapReverse where
+  map_reverse' f := by
+    simp only [Quiver.reverse, Quiver.HasReverse.reverse', Groupoid.inv_eq_inv,
+      Functor.map_inv]
 #align category_theory.functor_map_reverse CategoryTheory.functorMapReverse
 
 variable (X Y)
 
 /-- In a groupoid, isomorphisms are equivalent to morphisms. -/
-def Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y)
-    where
+def Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y) where
   toFun := Iso.hom
   invFun f := ⟨f, Groupoid.inv f, (by aesop_cat), (by aesop_cat)⟩
   left_inv i := Iso.ext rfl
@@ -121,8 +118,7 @@ variable (C)
 
 /-- The functor from a groupoid `C` to its opposite sending every morphism to its inverse. -/
 @[simps]
-noncomputable def Groupoid.invFunctor : C ⥤ Cᵒᵖ
-    where
+noncomputable def Groupoid.invFunctor : C ⥤ Cᵒᵖ where
   obj := Opposite.op
   map {X Y} f := (inv f).op
 #align category_theory.groupoid.inv_functor CategoryTheory.Groupoid.invFunctor
@@ -141,8 +137,8 @@ noncomputable def Groupoid.ofIsIso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), Is
 #align category_theory.groupoid.of_is_iso CategoryTheory.Groupoid.ofIsIso
 
 /-- A category with a unique morphism between any two objects is a groupoid -/
-def Groupoid.ofHomUnique (all_unique : ∀ {X Y : C}, Unique (X ⟶ Y)) : Groupoid.{v} C
-    where inv _ := all_unique.default
+def Groupoid.ofHomUnique (all_unique : ∀ {X Y : C}, Unique (X ⟶ Y)) : Groupoid.{v} C where
+  inv _ := all_unique.default
 #align category_theory.groupoid.of_hom_unique CategoryTheory.Groupoid.ofHomUnique
 
 end
@@ -158,16 +154,15 @@ instance InducedCategory.groupoid {C : Type u} (D : Type u₂) [Groupoid.{v} D]
 section
 
 instance groupoidPi {I : Type u} {J : I → Type u₂} [∀ i, Groupoid.{v} (J i)] :
-    Groupoid.{max u v} (∀ i : I, J i)
-    where
-      inv f := fun i : I => Groupoid.inv (f i)
-      comp_inv := fun f => by funext i; apply Groupoid.comp_inv
-      inv_comp := fun f => by funext i; apply Groupoid.inv_comp
+    Groupoid.{max u v} (∀ i : I, J i) where
+  inv f := fun i : I => Groupoid.inv (f i)
+  comp_inv := fun f => by funext i; apply Groupoid.comp_inv
+  inv_comp := fun f => by funext i; apply Groupoid.inv_comp
 #align category_theory.groupoid_pi CategoryTheory.groupoidPi
 
 instance groupoidProd {α : Type u} {β : Type v} [Groupoid.{u₂} α] [Groupoid.{v₂} β] :
-    Groupoid.{max u₂ v₂} (α × β)
-    where inv f := (Groupoid.inv f.1, Groupoid.inv f.2)
+    Groupoid.{max u₂ v₂} (α × β) where
+  inv f := (Groupoid.inv f.1, Groupoid.inv f.2)
 #align category_theory.groupoid_prod CategoryTheory.groupoidProd
 
 end
diff --git a/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean b/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
index b2f86293a3ad4..ac5a7a3b46a0a 100644
--- a/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
@@ -26,10 +26,10 @@ extension as a functor from the free groupoid, and proves uniqueness of this ext
 
 Given the type `V` and a quiver instance on `V`:
 
-- `free_groupoid V`: a type synonym for `V`.
-- `free_groupoid_groupoid`: the `groupoid` instance on `free_groupoid V`.
+- `FreeGroupoid V`: a type synonym for `V`.
+- `FreeGroupoid.instGroupoid`: the `Groupoid` instance on `FreeGroupoid V`.
 - `lift`: the lifting of a prefunctor from `V` to `V'` where `V'` is a groupoid, to a functor.
-  `free_groupoid V ⥤ V'`.
+  `FreeGroupoid V ⥤ V'`.
 - `lift_spec` and `lift_unique`: the proofs that, respectively, `lift` indeed is a lifting
   and is the unique one.
 
@@ -136,12 +136,13 @@ def quotInv {X Y : FreeGroupoid V} (f : X ⟶ Y) : Y ⟶ X :=
     Quot.sound <| congr_reverse pp qq con
 #align category_theory.groupoid.free.quot_inv CategoryTheory.Groupoid.Free.quotInv
 
-instance : Groupoid (FreeGroupoid V) where
+instance _root_.CategoryTheory.FreeGroupoid.instGroupoid : Groupoid (FreeGroupoid V) where
   inv := quotInv
   inv_comp p := Quot.inductionOn p fun pp => congr_reverse_comp pp
   comp_inv p := Quot.inductionOn p fun pp => congr_comp_reverse pp
+#align category_theory.groupoid.free.category_theory.free_groupoid.category_theory.groupoid CategoryTheory.FreeGroupoid.instGroupoid
 
-/-- The inclusion of the quiver on `V` to the underlying quiver on `free_groupoid V`-/
+/-- The inclusion of the quiver on `V` to the underlying quiver on `FreeGroupoid V`-/
 def of (V) [Quiver V] : V ⥤q FreeGroupoid V where
   obj X := ⟨X⟩
   map f := Quot.mk _ f.toPosPath
@@ -156,7 +157,7 @@ section UniversalProperty
 
 variable {V' : Type u'} [Groupoid V'] (φ : V ⥤q V')
 
-/-- The lift of a prefunctor to a groupoid, to a functor from `free_groupoid V` -/
+/-- The lift of a prefunctor to a groupoid, to a functor from `FreeGroupoid V` -/
 def lift (φ : V ⥤q V') : FreeGroupoid V ⥤ V' :=
   Quotient.lift _ (Paths.lift <| Quiver.Symmetrify.lift φ) <| by
     rintro _ _ _ _ ⟨X, Y, f⟩
diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean
index 3fb8bf7503428..0151b7a395397 100644
--- a/Mathlib/CategoryTheory/Opposites.lean
+++ b/Mathlib/CategoryTheory/Opposites.lean
@@ -26,8 +26,6 @@ Unfortunately, because we do not have a definitional equality `op (op X) = X`,
 there are quite a few variations that are needed in practice.
 -/
 
-set_option autoImplicit false
-
 universe v₁ v₂ u₁ u₂
 
 -- morphism levels before object levels. See note [CategoryTheory universes].
@@ -46,8 +44,7 @@ theorem Quiver.Hom.op_inj {X Y : C} :
 
 theorem Quiver.Hom.unop_inj {X Y : Cᵒᵖ} :
     Function.Injective (Quiver.Hom.unop : (X ⟶ Y) → (Opposite.unop Y ⟶ Opposite.unop X)) :=
-    fun _ _ H =>
-  congr_arg Quiver.Hom.op H
+  fun _ _ H => congr_arg Quiver.Hom.op H
 #align quiver.hom.unop_inj Quiver.Hom.unop_inj
 
 @[simp]
@@ -70,9 +67,8 @@ variable [Category.{v₁} C]
 
 See <https://stacks.math.columbia.edu/tag/001M>.
 -/
-instance Category.opposite : Category.{v₁} Cᵒᵖ
-    where
-  comp := @fun _ _ _ f g => (g.unop ≫ f.unop).op
+instance Category.opposite : Category.{v₁} Cᵒᵖ where
+  comp f g := (g.unop ≫ f.unop).op
   id X := (𝟙 (unop X)).op
 #align category_theory.category.opposite CategoryTheory.Category.opposite
 
@@ -114,14 +110,14 @@ variable (C)
 @[simps]
 def opOp : Cᵒᵖᵒᵖ ⥤ C where
   obj X := unop (unop X)
-  map := @fun X Y f => f.unop.unop
+  map f := f.unop.unop
 #align category_theory.op_op CategoryTheory.opOp
 
 /-- The functor from a category to its double-opposite.  -/
 @[simps]
 def unopUnop : C ⥤ Cᵒᵖᵒᵖ where
   obj X := op (op X)
-  map := @fun X Y f => f.op.op
+  map f := f.op.op
 #align category_theory.unop_unop CategoryTheory.unopUnop
 
 /-- The double opposite category is equivalent to the original. -/
@@ -177,26 +173,21 @@ section
 
 variable {D : Type u₂} [Category.{v₂} D]
 
--- porting note: commenting out redundant binder annotation update
--- variable {C D}
-
 /-- The opposite of a functor, i.e. considering a functor `F : C ⥤ D` as a functor `Cᵒᵖ ⥤ Dᵒᵖ`.
 In informal mathematics no distinction is made between these. -/
 @[simps, pp_dot]
-protected def op (F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ
-    where
+protected def op (F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ where
   obj X := op (F.obj (unop X))
-  map := @fun X Y f => (F.map f.unop).op
+  map f := (F.map f.unop).op
 #align category_theory.functor.op CategoryTheory.Functor.op
 
 /-- Given a functor `F : Cᵒᵖ ⥤ Dᵒᵖ` we can take the "unopposite" functor `F : C ⥤ D`.
 In informal mathematics no distinction is made between these.
 -/
 @[simps]
-protected def unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D
-    where
+protected def unop (F : Cᵒᵖ ⥤ Dᵒᵖ) : C ⥤ D where
   obj X := unop (F.obj (op X))
-  map := @fun X Y f => (F.map f.op).unop
+  map f := (F.map f.op).unop
 #align category_theory.functor.unop CategoryTheory.Functor.unop
 
 /-- The isomorphism between `F.op.unop` and `F`. -/
@@ -218,7 +209,7 @@ variable (C D)
 @[simps]
 def opHom : (C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ where
   obj F := (unop F).op
-  map := @fun F G α =>
+  map α :=
     { app := fun X => (α.unop.app (unop X)).op
       naturality := fun X Y f => Quiver.Hom.unop_inj (α.unop.naturality f.unop).symm }
 #align category_theory.functor.op_hom CategoryTheory.Functor.opHom
@@ -228,7 +219,7 @@ def opHom : (C ⥤ D)ᵒᵖ ⥤ Cᵒᵖ ⥤ Dᵒᵖ where
 @[simps]
 def opInv : (Cᵒᵖ ⥤ Dᵒᵖ) ⥤ (C ⥤ D)ᵒᵖ where
   obj F := op F.unop
-  map := @fun F G α =>
+  map α :=
     Quiver.Hom.op
       { app := fun X => (α.app (op X)).unop
         naturality := fun X Y f => Quiver.Hom.op_inj <| (α.naturality f.op).symm }
@@ -241,10 +232,9 @@ Another variant of the opposite of functor, turning a functor `C ⥤ Dᵒᵖ` in
 In informal mathematics no distinction is made.
 -/
 @[simps, pp_dot]
-protected def leftOp (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D
-    where
+protected def leftOp (F : C ⥤ Dᵒᵖ) : Cᵒᵖ ⥤ D where
   obj X := unop (F.obj (unop X))
-  map := @fun X Y f => (F.map f.unop).unop
+  map f := (F.map f.unop).unop
 #align category_theory.functor.left_op CategoryTheory.Functor.leftOp
 
 /--
@@ -252,28 +242,24 @@ Another variant of the opposite of functor, turning a functor `Cᵒᵖ ⥤ D` in
 In informal mathematics no distinction is made.
 -/
 @[simps, pp_dot]
-protected def rightOp (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ
-    where
+protected def rightOp (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ where
   obj X := op (F.obj (op X))
-  map := @fun X Y f => (F.map f.op).op
+  map f := (F.map f.op).op
 #align category_theory.functor.right_op CategoryTheory.Functor.rightOp
 
 instance {F : C ⥤ D} [Full F] : Full F.op where preimage := @fun X Y f => (F.preimage f.unop).op
 
-instance {F : C ⥤ D} [Faithful F] : Faithful F.op
-    where map_injective := @fun X Y f g h =>
-    Quiver.Hom.unop_inj <| by simpa using map_injective F (Quiver.Hom.op_inj h)
+instance {F : C ⥤ D} [Faithful F] : Faithful F.op where
+  map_injective h := Quiver.Hom.unop_inj <| by simpa using map_injective F (Quiver.Hom.op_inj h)
 
 /-- If F is faithful then the right_op of F is also faithful. -/
-instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp
-    where map_injective := @fun _ _ _ _ h =>
-        Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h))
+instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp where
+  map_injective h := Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h))
 #align category_theory.functor.right_op_faithful CategoryTheory.Functor.rightOp_faithful
 
 /-- If F is faithful then the left_op of F is also faithful. -/
-instance leftOp_faithful {F : C ⥤ Dᵒᵖ} [Faithful F] : Faithful F.leftOp
-    where map_injective := @fun _ _ _ _ h =>
-        Quiver.Hom.unop_inj (map_injective F (Quiver.Hom.unop_inj h))
+instance leftOp_faithful {F : C ⥤ Dᵒᵖ} [Faithful F] : Faithful F.leftOp where
+  map_injective h := Quiver.Hom.unop_inj (map_injective F (Quiver.Hom.unop_inj h))
 #align category_theory.functor.left_op_faithful CategoryTheory.Functor.leftOp_faithful
 
 /-- The isomorphism between `F.leftOp.rightOp` and `F`. -/
@@ -309,8 +295,7 @@ variable {F G : C ⥤ D}
 
 /-- The opposite of a natural transformation. -/
 @[simps]
-protected def op (α : F ⟶ G) : G.op ⟶ F.op
-    where
+protected def op (α : F ⟶ G) : G.op ⟶ F.op where
   app X := (α.app (unop X)).op
   naturality X Y f := Quiver.Hom.unop_inj (by simp)
 #align category_theory.nat_trans.op CategoryTheory.NatTrans.op
@@ -322,8 +307,7 @@ theorem op_id (F : C ⥤ D) : NatTrans.op (𝟙 F) = 𝟙 F.op :=
 
 /-- The "unopposite" of a natural transformation. -/
 @[simps]
-protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop
-    where
+protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ⟶ G) : G.unop ⟶ F.unop where
   app X := (α.app (op X)).unop
   naturality X Y f := Quiver.Hom.op_inj (by simp)
 #align category_theory.nat_trans.unop CategoryTheory.NatTrans.unop
@@ -337,8 +321,7 @@ theorem unop_id (F : Cᵒᵖ ⥤ Dᵒᵖ) : NatTrans.unop (𝟙 F) = 𝟙 F.unop
 we can take the "unopposite" of each component obtaining a natural transformation `G ⟶ F`.
 -/
 @[simps]
-protected def removeOp (α : F.op ⟶ G.op) : G ⟶ F
-    where
+protected def removeOp (α : F.op ⟶ G.op) : G ⟶ F where
   app X := (α.app (op X)).unop
   naturality X Y f :=
     Quiver.Hom.op_inj <| by simpa only [Functor.op_map] using (α.naturality f.op).symm
@@ -352,8 +335,7 @@ theorem removeOp_id (F : C ⥤ D) : NatTrans.removeOp (𝟙 F.op) = 𝟙 F :=
 /-- Given a natural transformation `α : F.unop ⟶ G.unop`, we can take the opposite of each
 component obtaining a natural transformation `G ⟶ F`. -/
 @[simps]
-protected def removeUnop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) : G ⟶ F
-    where
+protected def removeUnop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F.unop ⟶ G.unop) : G ⟶ F where
   app X := (α.app (unop X)).op
   naturality X Y f :=
     Quiver.Hom.unop_inj <| by simpa only [Functor.unop_map] using (α.naturality f.unop).symm
@@ -371,11 +353,10 @@ section
 variable {F G H : C ⥤ Dᵒᵖ}
 
 /-- Given a natural transformation `α : F ⟶ G`, for `F G : C ⥤ Dᵒᵖ`,
-taking `unop` of each component gives a natural transformation `G.left_op ⟶ F.left_op`.
+taking `unop` of each component gives a natural transformation `G.leftOp ⟶ F.leftOp`.
 -/
 @[simps]
-protected def leftOp (α : F ⟶ G) : G.leftOp ⟶ F.leftOp
-    where
+protected def leftOp (α : F ⟶ G) : G.leftOp ⟶ F.leftOp where
   app X := (α.app (unop X)).unop
   naturality X Y f := Quiver.Hom.op_inj (by simp)
 #align category_theory.nat_trans.left_op CategoryTheory.NatTrans.leftOp
@@ -395,8 +376,7 @@ theorem leftOp_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.leftOp (α ≫ β)
 taking `op` of each component gives a natural transformation `G ⟶ F`.
 -/
 @[simps]
-protected def removeLeftOp (α : F.leftOp ⟶ G.leftOp) : G ⟶ F
-    where
+protected def removeLeftOp (α : F.leftOp ⟶ G.leftOp) : G ⟶ F where
   app X := (α.app (op X)).op
   naturality X Y f :=
     Quiver.Hom.unop_inj <| by simpa only [Functor.leftOp_map] using (α.naturality f.op).symm
@@ -417,8 +397,7 @@ variable {F G H : Cᵒᵖ ⥤ D}
 taking `op` of each component gives a natural transformation `G.rightOp ⟶ F.rightOp`.
 -/
 @[simps]
-protected def rightOp (α : F ⟶ G) : G.rightOp ⟶ F.rightOp
-    where
+protected def rightOp (α : F ⟶ G) : G.rightOp ⟶ F.rightOp where
   app X := (α.app _).op
   naturality X Y f := Quiver.Hom.unop_inj (by simp)
 #align category_theory.nat_trans.right_op CategoryTheory.NatTrans.rightOp
@@ -438,8 +417,7 @@ theorem rightOp_comp (α : F ⟶ G) (β : G ⟶ H) : NatTrans.rightOp (α ≫ β
 taking `unop` of each component gives a natural transformation `G ⟶ F`.
 -/
 @[simps]
-protected def removeRightOp (α : F.rightOp ⟶ G.rightOp) : G ⟶ F
-    where
+protected def removeRightOp (α : F.rightOp ⟶ G.rightOp) : G ⟶ F where
   app X := (α.app X.unop).unop
   naturality X Y f :=
     Quiver.Hom.op_inj <| by simpa only [Functor.rightOp_map] using (α.naturality f.unop).symm
@@ -461,8 +439,7 @@ variable {X Y : C}
 /-- The opposite isomorphism.
 -/
 @[simps]
-protected def op (α : X ≅ Y) : op Y ≅ op X
-    where
+protected def op (α : X ≅ Y) : op Y ≅ op X where
   hom := α.hom.op
   inv := α.inv.op
   hom_inv_id := Quiver.Hom.unop_inj α.inv_hom_id
@@ -471,8 +448,7 @@ protected def op (α : X ≅ Y) : op Y ≅ op X
 
 /-- The isomorphism obtained from an isomorphism in the opposite category. -/
 @[simps]
-def unop {X Y : Cᵒᵖ} (f : X ≅ Y) : Y.unop ≅ X.unop
-    where
+def unop {X Y : Cᵒᵖ} (f : X ≅ Y) : Y.unop ≅ X.unop where
   hom := f.hom.unop
   inv := f.inv.unop
   hom_inv_id := by simp only [← unop_comp, f.inv_hom_id, unop_id]
@@ -498,8 +474,7 @@ variable {F G : C ⥤ D}
 /-- The natural isomorphism between opposite functors `G.op ≅ F.op` induced by a natural
 isomorphism between the original functors `F ≅ G`. -/
 @[simps]
-protected def op (α : F ≅ G) : G.op ≅ F.op
-    where
+protected def op (α : F ≅ G) : G.op ≅ F.op where
   hom := NatTrans.op α.hom
   inv := NatTrans.op α.inv
   hom_inv_id := by ext; dsimp; rw [← op_comp]; rw [α.inv_hom_id_app]; rfl
@@ -509,8 +484,7 @@ protected def op (α : F ≅ G) : G.op ≅ F.op
 /-- The natural isomorphism between functors `G ≅ F` induced by a natural isomorphism
 between the opposite functors `F.op ≅ G.op`. -/
 @[simps]
-protected def removeOp (α : F.op ≅ G.op) : G ≅ F
-    where
+protected def removeOp (α : F.op ≅ G.op) : G ≅ F where
   hom := NatTrans.removeOp α.hom
   inv := NatTrans.removeOp α.inv
   hom_inv_id := by ext; dsimp; rw [← unop_comp]; rw [α.inv_hom_id_app]; rfl
@@ -520,8 +494,7 @@ protected def removeOp (α : F.op ≅ G.op) : G ≅ F
 /-- The natural isomorphism between functors `G.unop ≅ F.unop` induced by a natural isomorphism
 between the original functors `F ≅ G`. -/
 @[simps]
-protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : G.unop ≅ F.unop
-    where
+protected def unop {F G : Cᵒᵖ ⥤ Dᵒᵖ} (α : F ≅ G) : G.unop ≅ F.unop where
   hom := NatTrans.unop α.hom
   inv := NatTrans.unop α.inv
   hom_inv_id := by ext; dsimp; rw [← unop_comp]; rw [α.inv_hom_id_app]; rfl
@@ -579,8 +552,7 @@ def opEquiv''' (A B : C) : (Opposite.op A ⟶ Opposite.op B) ≃ (B ⟶ A) :=
 ```
 -/
 @[simps]
-def opEquiv (A B : Cᵒᵖ) : (A ⟶ B) ≃ (B.unop ⟶ A.unop)
-    where
+def opEquiv (A B : Cᵒᵖ) : (A ⟶ B) ≃ (B.unop ⟶ A.unop) where
   toFun f := f.unop
   invFun g := g.op
   left_inv _ := rfl
@@ -603,8 +575,7 @@ Note this is definitionally the same as the other three variants:
 * `(Opposite.op A ≅ Opposite.op B) ≃ (B ≅ A)`
 -/
 @[simps]
-def isoOpEquiv (A B : Cᵒᵖ) : (A ≅ B) ≃ (B.unop ≅ A.unop)
-    where
+def isoOpEquiv (A B : Cᵒᵖ) : (A ≅ B) ≃ (B.unop ≅ A.unop) where
   toFun f := f.unop
   invFun g := g.op
   left_inv _ := by
@@ -624,8 +595,7 @@ variable (D : Type u₂) [Category.{v₂} D]
 /-- The equivalence of functor categories induced by `op` and `unop`.
 -/
 @[simps]
-def opUnopEquiv : (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ
-    where
+def opUnopEquiv : (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ where
   functor := opHom _ _
   inverse := opInv _ _
   unitIso :=
@@ -642,8 +612,7 @@ def opUnopEquiv : (C ⥤ D)ᵒᵖ ≌ Cᵒᵖ ⥤ Dᵒᵖ
 /-- The equivalence of functor categories induced by `leftOp` and `rightOp`.
 -/
 @[simps!]
-def leftOpRightOpEquiv : (Cᵒᵖ ⥤ D)ᵒᵖ ≌ C ⥤ Dᵒᵖ
-    where
+def leftOpRightOpEquiv : (Cᵒᵖ ⥤ D)ᵒᵖ ≌ C ⥤ Dᵒᵖ where
   functor :=
     { obj := fun F => F.unop.rightOp
       map := fun η => NatTrans.rightOp η.unop  }
diff --git a/Mathlib/Computability/Language.lean b/Mathlib/Computability/Language.lean
index f6b6f67ff89d4..a6a326c438206 100644
--- a/Mathlib/Computability/Language.lean
+++ b/Mathlib/Computability/Language.lean
@@ -133,7 +133,7 @@ theorem nil_mem_kstar (l : Language α) : [] ∈ l∗ :=
   ⟨[], rfl, fun _ h ↦ by contradiction⟩
 #align language.nil_mem_kstar Language.nil_mem_kstar
 
-instance : Semiring (Language α) where
+instance instSemiring : Semiring (Language α) where
   add := (· + ·)
   add_assoc := union_assoc
   zero := 0
@@ -182,16 +182,11 @@ theorem kstar_def_nonempty (l : Language α) :
   constructor
   · rintro ⟨S, rfl, h⟩
     refine' ⟨S.filter fun l ↦ ¬List.isEmpty l, by simp, fun y hy ↦ _⟩
-    simp [mem_filter, List.isEmpty_iff_eq_nil] at hy
     -- Porting note: The previous code was:
-    -- exact ⟨h y hy.1, hy.2⟩
-    --
-    -- The goal `y ≠ []` for the second argument cannot be resolved
-    -- by `hy.2 : isEmpty y = False`.
-    let ⟨hyl, hyr⟩ := hy
-    apply And.intro (h y hyl)
-    cases y <;> simp only [ne_eq, not_true, not_false_iff]
-    contradiction
+    -- rw [mem_filter, empty_iff_eq_nil] at hy
+    rw [mem_filter, decide_not, Bool.decide_coe, Bool.not_eq_true', ← Bool.bool_iff_false,
+      isEmpty_iff_eq_nil] at hy
+    exact ⟨h y hy.1, hy.2⟩
   · rintro ⟨S, hx, h⟩
     exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩
 #align language.kstar_def_nonempty Language.kstar_def_nonempty
@@ -241,15 +236,8 @@ theorem mem_pow {l : Language α} {x : List α} {n : ℕ} :
     constructor
     · rintro rfl
       exact ⟨[], rfl, rfl, fun _ h ↦ by contradiction⟩
-    · -- Porting note: The previous code was:
-      -- rintro ⟨_, rfl, rfl, _⟩
-      -- rfl
-      --
-      -- The code reports an error for the second `rfl`.
-      rintro ⟨_, rfl, h₀, _⟩
-      simp; intros _ h₁
-      rw [h₀] at h₁
-      contradiction
+    · rintro ⟨_, rfl, rfl, _⟩
+      rfl
   · simp only [pow_succ, mem_mul, ihn]
     constructor
     · rintro ⟨a, b, ha, ⟨S, rfl, rfl, hS⟩, rfl⟩
@@ -292,7 +280,7 @@ theorem one_add_kstar_mul_self_eq_kstar (l : Language α) : 1 + l∗ * l = l∗
 #align language.one_add_kstar_mul_self_eq_kstar Language.one_add_kstar_mul_self_eq_kstar
 
 instance : KleeneAlgebra (Language α) :=
-  { Language.instSemiringLanguage, Set.completeAtomicBooleanAlgebra with
+  { Language.instSemiring, Set.completeAtomicBooleanAlgebra with
     kstar := fun L ↦ L∗,
     one_le_kstar := fun a l hl ↦ ⟨[], hl, by simp⟩,
     mul_kstar_le_kstar := fun a ↦ (one_add_self_mul_kstar_eq_kstar a).le.trans' le_sup_right,
diff --git a/Mathlib/Data/List/Sigma.lean b/Mathlib/Data/List/Sigma.lean
index 5c893bd68ce8e..50ce9b78dca09 100644
--- a/Mathlib/Data/List/Sigma.lean
+++ b/Mathlib/Data/List/Sigma.lean
@@ -247,7 +247,7 @@ theorem lookup_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁
     rw [← mem_dlookup_iff, ← mem_dlookup_iff, h] <;> assumption
 #align list.lookup_ext List.lookup_ext
 
-/-! ### `lookup_all` -/
+/-! ### `lookupAll` -/
 
 
 /-- `lookup_all a l` is the list of all values in `l` corresponding to the key `a`. -/
@@ -431,9 +431,9 @@ theorem mem_keys_of_mem_keys_kerase {a₁ a₂} {l : List (Sigma β)} :
 theorem exists_of_kerase {a : α} {l : List (Sigma β)} (h : a ∈ l.keys) :
     ∃ (b : β a) (l₁ l₂ : List (Sigma β)),
       a ∉ l₁.keys ∧ l = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a l = l₁ ++ l₂ := by
-  induction l
-  case nil => cases h
-  case cons hd tl ih =>
+  induction l with
+  | nil => cases h
+  | cons hd tl ih =>
     by_cases e : a = hd.1
     · subst e
       exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
@@ -463,7 +463,8 @@ theorem kerase_kerase {a a'} {l : List (Sigma β)} :
     (kerase a' l).kerase a = (kerase a l).kerase a' := by
   by_cases h : a = a'
   · subst a'; rfl
-  induction' l with x xs; · rfl
+  induction' l with x xs
+  · rfl
   · by_cases a' = x.1
     · subst a'
       simp [kerase_cons_ne h, kerase_cons_eq rfl]
@@ -485,9 +486,9 @@ theorem Perm.kerase {a : α} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys)
 @[simp]
 theorem not_mem_keys_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) :
     a ∉ (kerase a l).keys := by
-  induction l
-  case nil => simp
-  case cons hd tl ih =>
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
     simp at nd
     by_cases h : a = hd.1
     · subst h
@@ -504,9 +505,9 @@ theorem dlookup_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) :
 @[simp]
 theorem dlookup_kerase_ne {a a'} {l : List (Sigma β)} (h : a ≠ a') :
     dlookup a (kerase a' l) = dlookup a l := by
-  induction l
-  case nil => rfl
-  case cons hd tl ih =>
+  induction l with
+  | nil => rfl
+  | cons hd tl ih =>
     cases' hd with ah bh
     by_cases h₁ : a = ah <;> by_cases h₂ : a' = ah
     · substs h₁ h₂
@@ -701,9 +702,9 @@ theorem kunion_cons {s} {l₁ l₂ : List (Sigma β)} :
 @[simp]
 theorem mem_keys_kunion {a} {l₁ l₂ : List (Sigma β)} :
     a ∈ (kunion l₁ l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys := by
-  induction l₁ generalizing l₂
-  case nil => simp
-  case cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]
+  induction l₁ generalizing l₂ with
+  | nil => simp
+  | cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]
 #align list.mem_keys_kunion List.mem_keys_kunion
 
 @[simp]
@@ -714,21 +715,21 @@ theorem kunion_kerase {a} :
 #align list.kunion_kerase List.kunion_kerase
 
 theorem NodupKeys.kunion (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) : (kunion l₁ l₂).NodupKeys := by
-  induction l₁ generalizing l₂
-  case nil => simp only [nil_kunion, nd₂]
-  case cons s l₁ ih =>
+  induction l₁ generalizing l₂ with
+  | nil => simp only [nil_kunion, nd₂]
+  | cons s l₁ ih =>
     simp at nd₁
     simp [not_or, nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]
 #align list.nodupkeys.kunion List.NodupKeys.kunion
 
 theorem Perm.kunion_right {l₁ l₂ : List (Sigma β)} (p : l₁ ~ l₂) (l) :
     kunion l₁ l ~ kunion l₂ l := by
-  induction p generalizing l
-  case nil => rfl
-  case cons hd tl₁ tl₂ _ ih =>
+  induction p generalizing l with
+  | nil => rfl
+  | cons hd _ ih =>
     simp [ih (List.kerase _ _), Perm.cons]
-  case swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
-  case trans l₁ l₂ l₃ _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)
+  | swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
+  | trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)
 #align list.perm.kunion_right List.Perm.kunion_right
 
 theorem Perm.kunion_left :
@@ -758,17 +759,17 @@ theorem dlookup_kunion_left {a} {l₁ l₂ : List (Sigma β)} (h : a ∈ l₁.ke
 @[simp]
 theorem dlookup_kunion_right {a} {l₁ l₂ : List (Sigma β)} (h : a ∉ l₁.keys) :
     dlookup a (kunion l₁ l₂) = dlookup a l₂ := by
-  induction l₁ generalizing l₂
-  case nil => simp
-  case cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]
+  induction l₁ generalizing l₂ with
+  | nil => simp
+  | cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]
 #align list.lookup_kunion_right List.dlookup_kunion_right
 
 --Porting note: removing simp, LHS not in normal form, added new version
 theorem mem_dlookup_kunion {a} {b : β a} {l₁ l₂ : List (Sigma β)} :
     b ∈ dlookup a (kunion l₁ l₂) ↔ b ∈ dlookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ dlookup a l₂ := by
-  induction l₁ generalizing l₂
-  case nil => simp
-  case cons s _ ih =>
+  induction l₁ generalizing l₂ with
+  | nil => simp
+  | cons s _ ih =>
     cases' s with a'
     by_cases h₁ : a = a'
     · subst h₁
diff --git a/Mathlib/RingTheory/Localization/AtPrime.lean b/Mathlib/RingTheory/Localization/AtPrime.lean
index c68a035933b09..b839362180d11 100644
--- a/Mathlib/RingTheory/Localization/AtPrime.lean
+++ b/Mathlib/RingTheory/Localization/AtPrime.lean
@@ -16,7 +16,7 @@ import Mathlib.RingTheory.Localization.Ideal
 
 ## Main definitions
 
- * `IsLocalization.AtPrime (I : Ideal R) [IsPrime I] (S : Type*)` expresses that `S` is a
+ * `IsLocalization.AtPrime (I : Ideal R) [IsPrime I] (S : Type _)` expresses that `S` is a
    localization at (the complement of) a prime ideal `I`, as an abbreviation of
    `IsLocalization I.prime_compl S`
 
@@ -183,7 +183,7 @@ variable (I : Ideal R) [hI : I.IsPrime]
 
 variable {I}
 
-/-- The unique maximal ideal of the localization at `I.prime_compl` lies over the ideal `I`. -/
+/-- The unique maximal ideal of the localization at `I.primeCompl` lies over the ideal `I`. -/
 theorem AtPrime.comap_maximalIdeal :
     Ideal.comap (algebraMap R (Localization.AtPrime I))
         (LocalRing.maximalIdeal (Localization I.primeCompl)) =
@@ -192,8 +192,8 @@ theorem AtPrime.comap_maximalIdeal :
   IsLocalization.AtPrime.comap_maximalIdeal _ _
 #align localization.at_prime.comap_maximal_ideal Localization.AtPrime.comap_maximalIdeal
 
-/-- The image of `I` in the localization at `I.prime_compl` is a maximal ideal, and in particular
-it is the unique maximal ideal given by the local ring structure `at_prime.local_ring` -/
+/-- The image of `I` in the localization at `I.primeCompl` is a maximal ideal, and in particular
+it is the unique maximal ideal given by the local ring structure `AtPrime.localRing` -/
 theorem AtPrime.map_eq_maximalIdeal :
     Ideal.map (algebraMap R (Localization.AtPrime I)) I =
       LocalRing.maximalIdeal (Localization I.primeCompl) := by
@@ -208,7 +208,8 @@ theorem le_comap_primeCompl_iff {J : Ideal P} [hJ : J.IsPrime] {f : R →+* P} :
     I.primeCompl ≤ J.primeCompl.comap f ↔ J.comap f ≤ I :=
   ⟨fun h x hx => by
     contrapose! hx
-    exact h hx, fun h x hx hfxJ => hx (h hfxJ)⟩
+    exact h hx,
+   fun h x hx hfxJ => hx (h hfxJ)⟩
 #align localization.le_comap_prime_compl_iff Localization.le_comap_primeCompl_iff
 
 variable (I)
diff --git a/Mathlib/Topology/Algebra/MulAction.lean b/Mathlib/Topology/Algebra/MulAction.lean
index 078d444d948d8..809a9d0a0e69c 100644
--- a/Mathlib/Topology/Algebra/MulAction.lean
+++ b/Mathlib/Topology/Algebra/MulAction.lean
@@ -48,7 +48,7 @@ open Filter
 is continuous in both arguments. We use the same class for all kinds of multiplicative actions,
 including (semi)modules and algebras. -/
 class ContinuousSMul (M X : Type _) [SMul M X] [TopologicalSpace M] [TopologicalSpace X] :
-  Prop where
+    Prop where
   /-- The scalar multiplication `(•)` is continuous. -/
   continuous_smul : Continuous fun p : M × X => p.1 • p.2
 #align has_continuous_smul ContinuousSMul
@@ -59,7 +59,7 @@ export ContinuousSMul (continuous_smul)
 is continuous in both arguments. We use the same class for all kinds of additive actions,
 including (semi)modules and algebras. -/
 class ContinuousVAdd (M X : Type _) [VAdd M X] [TopologicalSpace M] [TopologicalSpace X] :
-  Prop where
+    Prop where
   /-- The additive action `(+ᵥ)` is continuous. -/
   continuous_vadd : Continuous fun p : M × X => p.1 +ᵥ p.2
 #align has_continuous_vadd ContinuousVAdd
@@ -77,8 +77,8 @@ section SMul
 variable [SMul M X] [ContinuousSMul M X]
 
 @[to_additive]
-instance (priority := 100) ContinuousSMul.continuousConstSMul : ContinuousConstSMul M X
-    where continuous_const_smul _ := continuous_smul.comp (continuous_const.prod_mk continuous_id)
+instance (priority := 100) ContinuousSMul.continuousConstSMul : ContinuousConstSMul M X where
+  continuous_const_smul _ := continuous_smul.comp (continuous_const.prod_mk continuous_id)
 #align has_continuous_smul.has_continuous_const_smul ContinuousSMul.continuousConstSMul
 #align has_continuous_vadd.has_continuous_const_vadd ContinuousVAdd.continuousConstVAdd
 
@@ -126,7 +126,7 @@ theorem Continuous.smul (hf : Continuous f) (hg : Continuous g) : Continuous fun
 #align continuous.vadd Continuous.vadd
 
 /-- If a scalar action is central, then its right action is continuous when its left action is. -/
-@[to_additive "If an additive action is central, then its right action is continuous when its left\n
+@[to_additive "If an additive action is central, then its right action is continuous when its left
 action is."]
 instance ContinuousSMul.op [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : ContinuousSMul Mᵐᵒᵖ X :=
   ⟨by
@@ -150,8 +150,8 @@ section Monoid
 variable [Monoid M] [MulAction M X] [ContinuousSMul M X]
 
 @[to_additive]
-instance Units.continuousSMul : ContinuousSMul Mˣ X
-    where continuous_smul :=
+instance Units.continuousSMul : ContinuousSMul Mˣ X where
+  continuous_smul :=
     show Continuous ((fun p : M × X => p.fst • p.snd) ∘ fun p : Mˣ × X => (p.1, p.2)) from
       continuous_smul.comp ((Units.continuous_val.comp continuous_fst).prod_mk continuous_snd)
 #align units.has_continuous_smul Units.continuousSMul

From 436223a1ca56fbc80f4b4f7bae4b86d1d52b7257 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sat, 22 Jul 2023 22:04:17 +0200
Subject: [PATCH 2/3] Review

---
 Mathlib/Algebra/Hom/Centroid.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Algebra/Hom/Centroid.lean b/Mathlib/Algebra/Hom/Centroid.lean
index bdeda5c1b9169..d2cc3c6601137 100644
--- a/Mathlib/Algebra/Hom/Centroid.lean
+++ b/Mathlib/Algebra/Hom/Centroid.lean
@@ -108,10 +108,10 @@ mismatch, so I used `library_search`. -/
 instance : CoeFun (CentroidHom α) fun _ ↦ α → α :=
   inferInstanceAs (CoeFun (CentroidHom α) fun _ ↦ α → α)
 
-/- Porting note:
-`theorem to_fun_eq_coe {f : CentroidHom α} : f.toFun = (f : α → α) := rfl`
-removed because it is now a tautology -/
-#noalign centroid_hom.to_fun_eq_coe
+-- Porting note: removed @[simp]; not in normal form. (`toAddMonoidHom_eq_coe` below ensures that
+-- the LHS simplifies to the RHS anyway.)
+theorem toFun_eq_coe {f : CentroidHom α} : f.toFun = f := rfl
+#align centroid_hom.to_fun_eq_coe CentroidHom.toFun_eq_coe
 
 @[ext]
 theorem ext {f g : CentroidHom α} (h : ∀ a, f a = g a) : f = g :=

From 36c4202efb3ac4e1e8fb91d207c8dcbc178f5024 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Wed, 26 Jul 2023 18:00:07 +0200
Subject: [PATCH 3/3] Review

---
 Mathlib/Algebra/Hom/Centroid.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Hom/Centroid.lean b/Mathlib/Algebra/Hom/Centroid.lean
index d2cc3c6601137..d057811d95ef0 100644
--- a/Mathlib/Algebra/Hom/Centroid.lean
+++ b/Mathlib/Algebra/Hom/Centroid.lean
@@ -492,7 +492,7 @@ theorem toEnd_int_cast (z : ℤ) : (z : CentroidHom α).toEnd = ↑z :=
   rfl
 #align centroid_hom.to_End_int_cast CentroidHom.toEnd_int_cast
 
-instance ring : Ring (CentroidHom α) :=
+instance instRing : Ring (CentroidHom α) :=
   toEnd_injective.ring _ toEnd_zero toEnd_one toEnd_add toEnd_mul toEnd_neg toEnd_sub
     toEnd_nsmul toEnd_zsmul toEnd_pow toEnd_nat_cast toEnd_int_cast
 
@@ -507,7 +507,7 @@ variable [NonUnitalRing α]
 /-- A prime associative ring has commutative centroid. -/
 @[reducible]
 def commRing (h : ∀ a b : α, (∀ r : α, a * r * b = 0) → a = 0 ∨ b = 0) : CommRing (CentroidHom α) :=
-  { CentroidHom.ring with
+  { CentroidHom.instRing with
     mul_comm := fun f g ↦ by
       ext
       refine' sub_eq_zero.1 ((or_self_iff _).1 <| (h _ _) fun r ↦ _)