chore: tidy various files (#5971)

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -49,14 +49,14 @@ abbrev Two :=
   WithZero Unit
 #align counterexample.counterexample_not_prime_but_homogeneous_prime.two Counterexample.CounterexampleNotPrimeButHomogeneousPrime.Two
 
-instance Two.LinearOrder : LinearOrder Two :=
+instance Two.instLinearOrder : LinearOrder Two :=
   inferInstance
 
-instance Two.AddCommMonoid : AddCommMonoid Two :=
+instance Two.instAddCommMonoid : AddCommMonoid Two :=
   inferInstance
 
 instance : LinearOrderedAddCommMonoid Two :=
-  { Two.LinearOrder, Two.AddCommMonoid with
+  { Two.instLinearOrder, Two.instAddCommMonoid with
     add_le_add_left := by
       delta Two WithZero; decide }
 section

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -16,9 +16,9 @@ import Mathlib.Algebra.Category.ModuleCat.Basic
 /-!
 # Category instance for algebras over a commutative ring
 
-We introduce the bundled category `Algebra` of algebras over a fixed commutative ring `R ` along
-with the forgetful functors to `Ring` and `Module`. We furthermore show that the functor associating
-to a type the free `R`-algebra on that type is left adjoint to the forgetful functor.
+We introduce the bundled category `AlgebraCat` of algebras over a fixed commutative ring `R ` along
+with the forgetful functors to `RingCat` and `ModuleCat`. We furthermore show that the functor
+associating to a type the free `R`-algebra on that type is left adjoint to the forgetful functor.
 -/
 
 set_option linter.uppercaseLean3 false
@@ -93,7 +93,7 @@ def of (X : Type v) [Ring X] [Algebra R X] : AlgebraCat.{v} R :=
   ⟨X⟩
 #align Algebra.of AlgebraCat.of
 
-/-- Typecheck a `alg_hom` as a morphism in `Algebra R`. -/
+/-- Typecheck a `AlgHom` as a morphism in `AlgebraCat R`. -/
 def ofHom {R : Type u} [CommRing R] {X Y : Type v} [Ring X] [Algebra R X] [Ring Y] [Algebra R Y]
     (f : X →ₐ[R] Y) : of R X ⟶ of R Y :=
   f
@@ -189,7 +189,7 @@ variable {R}
 
 variable {X₁ X₂ : Type u}
 
-/-- Build an isomorphism in the category `Algebra R` from a `alg_equiv` between `algebra`s. -/
+/-- Build an isomorphism in the category `AlgebraCat R` from a `AlgEquiv` between `Algebra`s. -/
 @[simps]
 def AlgEquiv.toAlgebraIso {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂}
     (e : X₁ ≃ₐ[R] X₂) : AlgebraCat.of R X₁ ≅ AlgebraCat.of R X₂ where
@@ -201,7 +201,7 @@ def AlgEquiv.toAlgebraIso {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra
 
 namespace CategoryTheory.Iso
 
-/-- Build a `alg_equiv` from an isomorphism in the category `Algebra R`. -/
+/-- Build a `AlgEquiv` from an isomorphism in the category `AlgebraCat R`. -/
 @[simps]
 def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y where
   toFun := i.hom
@@ -223,8 +223,8 @@ def toAlgEquiv {X Y : AlgebraCat R} (i : X ≅ Y) : X ≃ₐ[R] Y where
 
 end CategoryTheory.Iso
 
-/-- Algebra equivalences between `algebras`s are the same as (isomorphic to) isomorphisms in
-`Algebra`. -/
+/-- Algebra equivalences between `Algebra`s are the same as (isomorphic to) isomorphisms in
+`AlgebraCat`. -/
 @[simps]
 def algEquivIsoAlgebraIso {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] :
     (X ≃ₐ[R] Y) ≅ AlgebraCat.of R X ≅ AlgebraCat.of R Y where
@@ -238,7 +238,7 @@ instance (X : Type u) [Ring X] [Algebra R X] : CoeOut (Subalgebra R X) (AlgebraC
 
 instance AlgebraCat.forget_reflects_isos : ReflectsIsomorphisms (forget (AlgebraCat.{u} R)) where
   reflects {X Y} f _ := by
-    { let i := asIso ((forget (AlgebraCat.{u} R)).map f)
-      let e : X ≃ₐ[R] Y := { f, i.toEquiv with }
-      exact ⟨(IsIso.of_iso e.toAlgebraIso).1⟩ }
+    let i := asIso ((forget (AlgebraCat.{u} R)).map f)
+    let e : X ≃ₐ[R] Y := { f, i.toEquiv with }
+    exact ⟨(IsIso.of_iso e.toAlgebraIso).1⟩
 #align Algebra.forget_reflects_isos AlgebraCat.forget_reflects_isos

Mathlib/Algebra/Category/MonCat/Adjunctions.lean

@@ -51,8 +51,8 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align has_forget_to_AddSemigroup hasForgetToAddSemigroup
 
-/-- The adjoin_one-forgetful adjunction from `SemigroupCat` to `MonCat`.-/
-@[to_additive "The adjoin_one-forgetful adjunction from `AddSemigroupCat` to `AddMonCat`"]
+/-- The `adjoinOne`-forgetful adjunction from `SemigroupCat` to `MonCat`.-/
+@[to_additive "The `adjoinZero`-forgetful adjunction from `AddSemigroupCat` to `AddMonCat`"]
 def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} SemigroupCat.{u} :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun S M => WithOne.lift.symm

Mathlib/Algebra/Star/Basic.lean

@@ -178,9 +178,7 @@ theorem star_mul' [CommSemigroup R] [StarSemigroup R] (x y : R) : star (x * y) =
 /-- `star` as a `MulEquiv` from `R` to `Rᵐᵒᵖ` -/
 @[simps apply]
 def starMulEquiv [Semigroup R] [StarSemigroup R] : R ≃* Rᵐᵒᵖ :=
-  {
-    (InvolutiveStar.star_involutive.toPerm star).trans
-      opEquiv with
+  { (InvolutiveStar.star_involutive.toPerm star).trans opEquiv with
     toFun := fun x => MulOpposite.op (star x)
     map_mul' := fun x y => by simp only [star_mul, op_mul] }
 #align star_mul_equiv starMulEquiv
@@ -189,9 +187,7 @@ def starMulEquiv [Semigroup R] [StarSemigroup R] : R ≃* Rᵐᵒᵖ :=
 /-- `star` as a `MulAut` for commutative `R`. -/
 @[simps apply]
 def starMulAut [CommSemigroup R] [StarSemigroup R] : MulAut R :=
-  {
-    InvolutiveStar.star_involutive.toPerm
-      star with
+  { InvolutiveStar.star_involutive.toPerm star with
     toFun := star
     map_mul' := star_mul' }
 #align star_mul_aut starMulAut
@@ -265,9 +261,7 @@ attribute [simp] star_add
 /-- `star` as an `AddEquiv` -/
 @[simps apply]
 def starAddEquiv [AddMonoid R] [StarAddMonoid R] : R ≃+ R :=
-  {
-    InvolutiveStar.star_involutive.toPerm
-      star with
+  { InvolutiveStar.star_involutive.toPerm star with
     toFun := star
     map_add' := star_add }
 #align star_add_equiv starAddEquiv
@@ -320,7 +314,8 @@ class StarRing (R : Type u) [NonUnitalSemiring R] extends StarSemigroup R where
 #align star_ring StarRing
 
 instance (priority := 100) StarRing.toStarAddMonoid [NonUnitalSemiring R] [StarRing R] :
-    StarAddMonoid R where star_add := StarRing.star_add
+    StarAddMonoid R where
+  star_add := StarRing.star_add
 #align star_ring.to_star_add_monoid StarRing.toStarAddMonoid
 
 /-- `star` as a `RingEquiv` from `R` to `Rᵐᵒᵖ` -/
@@ -378,7 +373,6 @@ def starRingEnd [CommSemiring R] [StarRing R] : R →+* R :=
 
 variable {R}
 
--- mathport name: star_ring_end
 @[inherit_doc]
 scoped[ComplexConjugate] notation "conj" => starRingEnd _
 
@@ -403,8 +397,7 @@ theorem starRingEnd_self_apply [CommSemiring R] [StarRing R] (x : R) :
 #align star_ring_end_self_apply starRingEnd_self_apply
 
 instance RingHom.involutiveStar {S : Type _} [NonAssocSemiring S] [CommSemiring R] [StarRing R] :
-    InvolutiveStar (S →+* R)
-    where
+    InvolutiveStar (S →+* R) where
   toStar := { star := fun f => RingHom.comp (starRingEnd R) f }
   star_involutive := by
     intro
@@ -529,8 +522,7 @@ namespace Units
 
 variable [Monoid R] [StarSemigroup R]
 
-instance : StarSemigroup Rˣ
-    where
+instance : StarSemigroup Rˣ where
   star u :=
     { val := star u
       inv := star ↑u⁻¹
@@ -602,17 +594,17 @@ theorem op_star [Star R] (r : R) : op (star r) = star (op r) :=
   rfl
 #align mul_opposite.op_star MulOpposite.op_star
 
-instance [InvolutiveStar R] : InvolutiveStar Rᵐᵒᵖ
-    where star_involutive r := unop_injective (star_star r.unop)
+instance [InvolutiveStar R] : InvolutiveStar Rᵐᵒᵖ where
+  star_involutive r := unop_injective (star_star r.unop)
 
-instance [Monoid R] [StarSemigroup R] : StarSemigroup Rᵐᵒᵖ
-    where star_mul x y := unop_injective (star_mul y.unop x.unop)
+instance [Monoid R] [StarSemigroup R] : StarSemigroup Rᵐᵒᵖ where
+  star_mul x y := unop_injective (star_mul y.unop x.unop)
 
-instance [AddMonoid R] [StarAddMonoid R] : StarAddMonoid Rᵐᵒᵖ
-    where star_add x y := unop_injective (star_add x.unop y.unop)
+instance [AddMonoid R] [StarAddMonoid R] : StarAddMonoid Rᵐᵒᵖ where
+  star_add x y := unop_injective (star_add x.unop y.unop)
 
-instance [Semiring R] [StarRing R] : StarRing Rᵐᵒᵖ
-  where star_add x y := unop_injective (star_add x.unop y.unop)
+instance [Semiring R] [StarRing R] : StarRing Rᵐᵒᵖ where
+  star_add x y := unop_injective (star_add x.unop y.unop)
 
 end MulOpposite
 

Mathlib/Analysis/Seminorm.lean

@@ -1206,16 +1206,16 @@ protected theorem uniformContinuous [UniformSpace E] [UniformAddGroup E] [Contin
 /-- A seminorm is uniformly continuous if `p.closedBall 0 r ∈ 𝓝 0` for *all* `r > 0`.
 Over a `NontriviallyNormedField` it is actually enough to check that this is true
 for *some* `r`, see `Seminorm.uniformContinuous'`. -/
-protected theorem uniform_continuous_of_forall' [UniformSpace E] [UniformAddGroup E]
+protected theorem uniformContinuous_of_forall' [UniformSpace E] [UniformAddGroup E]
     {p : Seminorm 𝕝 E} (hp : ∀ r > 0, p.closedBall 0 r ∈ (𝓝 0 : Filter E)) :
     UniformContinuous p :=
   Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero_of_forall' hp)
 
-protected theorem uniform_continuous' [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul 𝕜 E]
+protected theorem uniformContinuous' [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul 𝕜 E]
     {p : Seminorm 𝕜 E} {r : ℝ} (hp : p.closedBall 0 r ∈ (𝓝 0 : Filter E)) :
     UniformContinuous p :=
   Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero' hp)
-#align seminorm.uniform_continuous' Seminorm.uniform_continuous'
+#align seminorm.uniform_continuous' Seminorm.uniformContinuous'
 
 /-- A seminorm is continuous if `p.ball 0 r ∈ 𝓝 0` for *all* `r > 0`.
 Over a `NontriviallyNormedField` it is actually enough to check that this is true

Mathlib/Data/Int/GCD.lean

@@ -20,12 +20,12 @@ import Mathlib.Order.Bounds.Basic
 ## Main definitions
 
 * Given `x y : ℕ`, `xgcd x y` computes the pair of integers `(a, b)` such that
-  `gcd x y = x * a + y * b`. `gcd_a x y` and `gcd_b x y` are defined to be `a` and `b`,
+  `gcd x y = x * a + y * b`. `gcdA x y` and `gcdB x y` are defined to be `a` and `b`,
   respectively.
 
 ## Main statements
 
-* `gcd_eq_gcd_ab`: Bézout's lemma, given `x y : ℕ`, `gcd x y = x * gcd_a x y + y * gcd_b x y`.
+* `gcd_eq_gcd_ab`: Bézout's lemma, given `x y : ℕ`, `gcd x y = x * gcdA x y + y * gcdB x y`.
 
 ## Tags
 
@@ -58,11 +58,11 @@ theorem xgcdAux_succ : xgcdAux (succ k) s t r' s' t' =
 theorem xgcd_zero_left {s t r' s' t'} : xgcdAux 0 s t r' s' t' = (r', s', t') := by simp [xgcdAux]
 #align nat.xgcd_zero_left Nat.xgcd_zero_left
 
-theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) :
+theorem xgcdAux_rec {r s t r' s' t'} (h : 0 < r) :
     xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
   obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
   rfl
-#align nat.xgcd_aux_rec Nat.xgcd_aux_rec
+#align nat.xgcd_aux_rec Nat.xgcdAux_rec
 
 /-- Use the extended GCD algorithm to generate the `a` and `b` values
   satisfying `gcd x y = x * a + y * b`. -/
@@ -96,7 +96,8 @@ theorem gcdB_zero_left {s : ℕ} : gcdB 0 s = 1 := by
 theorem gcdA_zero_right {s : ℕ} (h : s ≠ 0) : gcdA s 0 = 1 := by
   unfold gcdA xgcd
   obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
-  -- Porting note: `simp [xgcdAux_succ]` crashes Lean here
+  -- Porting note (https://github.com/leanprover/lean4/issues/2330):
+  -- `simp [xgcdAux_succ]` crashes Lean here
   rw [xgcdAux_succ]
   rfl
 #align nat.gcd_a_zero_right Nat.gcdA_zero_right
@@ -105,21 +106,22 @@ theorem gcdA_zero_right {s : ℕ} (h : s ≠ 0) : gcdA s 0 = 1 := by
 theorem gcdB_zero_right {s : ℕ} (h : s ≠ 0) : gcdB s 0 = 0 := by
   unfold gcdB xgcd
   obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
-  -- Porting note: `simp [xgcdAux_succ]` crashes Lean here
+  -- Porting note (https://github.com/leanprover/lean4/issues/2330):
+  -- `simp [xgcdAux_succ]` crashes Lean here
   rw [xgcdAux_succ]
   rfl
 #align nat.gcd_b_zero_right Nat.gcdB_zero_right
 
 @[simp]
-theorem xgcd_aux_fst (x y) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
+theorem xgcdAux_fst (x y) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
   gcd.induction x y (by simp) fun x y h IH s t s' t' => by
-    simp [xgcd_aux_rec, h, IH]
+    simp [xgcdAux_rec, h, IH]
     rw [← gcd_rec]
-#align nat.xgcd_aux_fst Nat.xgcd_aux_fst
+#align nat.xgcd_aux_fst Nat.xgcdAux_fst
 
-theorem xgcd_aux_val (x y) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y) := by
-  rw [xgcd, ← xgcd_aux_fst x y 1 0 0 1]
-#align nat.xgcd_aux_val Nat.xgcd_aux_val
+theorem xgcdAux_val (x y) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y) := by
+  rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
+#align nat.xgcd_aux_val Nat.xgcdAux_val
 
 theorem xgcd_val (x y) : xgcd x y = (gcdA x y, gcdB x y) := by
   unfold gcdA gcdB; cases xgcd x y; rfl
@@ -132,25 +134,25 @@ variable (x y : ℕ)
 private def P : ℕ × ℤ × ℤ → Prop
   | (r, s, t) => (r : ℤ) = x * s + y * t
 
-theorem xgcd_aux_P {r r'} :
+theorem xgcdAux_P {r r'} :
     ∀ {s t s' t'}, P x y (r, s, t) → P x y (r', s', t') → P x y (xgcdAux r s t r' s' t') := by
   induction r, r' using gcd.induction with
   | H0 => simp
   | H1 a b h IH =>
     intro s t s' t' p p'
-    rw [xgcd_aux_rec h]; refine' IH _ p; dsimp [P] at *
+    rw [xgcdAux_rec h]; refine' IH _ p; dsimp [P] at *
     rw [Int.emod_def]; generalize (b / a : ℤ) = k
     rw [p, p', mul_sub, sub_add_eq_add_sub, mul_sub, add_mul, mul_comm k t, mul_comm k s,
       ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
 set_option linter.uppercaseLean3 false in
-#align nat.xgcd_aux_P Nat.xgcd_aux_P
+#align nat.xgcd_aux_P Nat.xgcdAux_P
 
 /-- **Bézout's lemma**: given `x y : ℕ`, `gcd x y = x * a + y * b`, where `a = gcd_a x y` and
 `b = gcd_b x y` are computed by the extended Euclidean algorithm.
 -/
 theorem gcd_eq_gcd_ab : (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y := by
-  have := @xgcd_aux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
-  rwa [xgcd_aux_val, xgcd_val] at this
+  have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
+  rwa [xgcdAux_val, xgcd_val] at this
 #align nat.gcd_eq_gcd_ab Nat.gcd_eq_gcd_ab
 
 end
@@ -212,8 +214,8 @@ theorem gcd_eq_gcd_ab : ∀ x y : ℤ, (gcd x y : ℤ) = x * gcdA x y + y * gcdB
 
 theorem natAbs_ediv (a b : ℤ) (H : b ∣ a) : natAbs (a / b) = natAbs a / natAbs b := by
   rcases Nat.eq_zero_or_pos (natAbs b) with (h | h)
-  rw [natAbs_eq_zero.1 h]
-  simp [Int.ediv_zero]
+  · rw [natAbs_eq_zero.1 h]
+    simp [Int.ediv_zero]
   calc
     natAbs (a / b) = natAbs (a / b) * 1 := by rw [mul_one]
     _ = natAbs (a / b) * (natAbs b / natAbs b) := by rw [Nat.div_self h]

Mathlib/GroupTheory/FiniteAbelian.lean

@@ -14,10 +14,10 @@ import Mathlib.Data.ZMod.Quotient
 /-!
 # Structure of finite(ly generated) abelian groups
 
-* `AddCommGroup.equiv_free_prod_directSum_zMod` : Any finitely generated abelian group is the
+* `AddCommGroup.equiv_free_prod_directSum_zmod` : Any finitely generated abelian group is the
   product of a power of `ℤ` and a direct sum of some `ZMod (p i ^ e i)` for some prime powers
   `p i ^ e i`.
-* `AddCommGroup.equiv_directSum_zMod_of_fintype` : Any finite abelian group is a direct sum of
+* `AddCommGroup.equiv_directSum_zmod_of_fintype` : Any finite abelian group is a direct sum of
   some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`.
 
 -/
@@ -54,7 +54,7 @@ variable [AddCommGroup G]
 /-- **Structure theorem of finitely generated abelian groups** : Any finitely generated abelian
 group is the product of a power of `ℤ` and a direct sum of some `ZMod (p i ^ e i)` for some
 prime powers `p i ^ e i`. -/
-theorem equiv_free_prod_directSum_zMod [hG : AddGroup.FG G] :
+theorem equiv_free_prod_directSum_zmod [hG : AddGroup.FG G] :
     ∃ (n : ℕ) (ι : Type) (_ : Fintype ι) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ),
       Nonempty <| G ≃+ (Fin n →₀ ℤ) × ⨁ i : ι, ZMod (p i ^ e i) := by
   obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ :=
@@ -67,15 +67,15 @@ theorem equiv_free_prod_directSum_zMod [hG : AddGroup.FG G] :
         DFinsupp.mapRange.addEquiv fun i =>
           ((Int.quotientSpanEquivZMod _).trans <|
               ZMod.ringEquivCongr <| (p i).natAbs_pow _).toAddEquiv)
-#align add_comm_group.equiv_free_prod_direct_sum_zmod AddCommGroup.equiv_free_prod_directSum_zMod
+#align add_comm_group.equiv_free_prod_direct_sum_zmod AddCommGroup.equiv_free_prod_directSum_zmod
 
 /-- **Structure theorem of finite abelian groups** : Any finite abelian group is a direct sum of
 some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`. -/
-theorem equiv_directSum_zMod_of_fintype [Finite G] :
+theorem equiv_directSum_zmod_of_fintype [Finite G] :
     ∃ (ι : Type) (_ : Fintype ι) (p : ι → ℕ) (_ : ∀ i, Nat.Prime <| p i) (e : ι → ℕ),
       Nonempty <| G ≃+ ⨁ i : ι, ZMod (p i ^ e i) := by
   cases nonempty_fintype G
-  obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zMod G
+  obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G
   cases' n with n
   · have : Unique (Fin Nat.zero →₀ ℤ) :=
       { uniq := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton] }
@@ -84,19 +84,19 @@ theorem equiv_directSum_zMod_of_fintype [Finite G] :
     exact
       (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
             ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim
-#align add_comm_group.equiv_direct_sum_zmod_of_fintype AddCommGroup.equiv_directSum_zMod_of_fintype
+#align add_comm_group.equiv_direct_sum_zmod_of_fintype AddCommGroup.equiv_directSum_zmod_of_fintype
 
-theorem finite_of_fG_torsion [hG' : AddGroup.FG G] (hG : AddMonoid.IsTorsion G) : Finite G :=
+theorem finite_of_fg_torsion [hG' : AddGroup.FG G] (hG : AddMonoid.IsTorsion G) : Finite G :=
   @Module.finite_of_fg_torsion _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG') <|
     AddMonoid.isTorsion_iff_isTorsion_int.mp hG
-#align add_comm_group.finite_of_fg_torsion AddCommGroup.finite_of_fG_torsion
+#align add_comm_group.finite_of_fg_torsion AddCommGroup.finite_of_fg_torsion
 
 end AddCommGroup
 
 namespace CommGroup
 
-theorem finite_of_fG_torsion [CommGroup G] [Group.FG G] (hG : Monoid.IsTorsion G) : Finite G :=
-  @Finite.of_equiv _ _ (AddCommGroup.finite_of_fG_torsion (Additive G) hG) Multiplicative.ofAdd
-#align comm_group.finite_of_fg_torsion CommGroup.finite_of_fG_torsion
+theorem finite_of_fg_torsion [CommGroup G] [Group.FG G] (hG : Monoid.IsTorsion G) : Finite G :=
+  @Finite.of_equiv _ _ (AddCommGroup.finite_of_fg_torsion (Additive G) hG) Multiplicative.ofAdd
+#align comm_group.finite_of_fg_torsion CommGroup.finite_of_fg_torsion
 
 end CommGroup