chore: tidy various files (#10453)

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -65,7 +65,7 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance FunLike_instance (X Y : GroupCat) : FunLike (X ⟶ Y) X Y :=
+instance instFunLike (X Y : GroupCat) : FunLike (X ⟶ Y) X Y :=
   show FunLike (X →* Y) X Y from inferInstance
 
 -- porting note: added
@@ -214,7 +214,7 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance FunLike_instance (X Y : CommGroupCat) : FunLike (X ⟶ Y) X Y :=
+instance instFunLike (X Y : CommGroupCat) : FunLike (X ⟶ Y) X Y :=
   show FunLike (X →* Y) X Y from inferInstance
 
 -- porting note: added

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -10,7 +10,7 @@ import Mathlib.CategoryTheory.Functor.ReflectsIso
 #align_import algebra.category.Mon.basic from "leanprover-community/mathlib"@"0caf3701139ef2e69c215717665361cda205a90b"
 
 /-!
-# Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.
+# Category instances for `Monoid`, `AddMonoid`, `CommMonoid`, and `AddCommMmonoid`.
 
 We introduce the bundled categories:
 * `MonCat`

Mathlib/Algebra/Group/Defs.lean

@@ -290,16 +290,16 @@ theorem mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) :=
 
 end Semigroup
 
-/-- A commutative addition is a type with an addition which commutes-/
+/-- A commutative additive magma is a type with an addition which commutes. -/
 @[ext]
 class AddCommMagma (G : Type u) extends Add G where
-  /-- Addition is commutative in an additive commutative semigroup. -/
+  /-- Addition is commutative in an commutative additive magma. -/
   protected add_comm : ∀ a b : G, a + b = b + a
 
-/-- A commutative multiplication is a type with a multiplication which commutes-/
+/-- A commutative multiplicative magma is a type with a multiplication which commutes. -/
 @[ext]
 class CommMagma (G : Type u) extends Mul G where
-  /-- Multiplication is commutative in a commutative semigroup. -/
+  /-- Multiplication is commutative in a commutative multiplicative magma. -/
   protected mul_comm : ∀ a b : G, a * b = b * a
 
 attribute [to_additive] CommMagma

Mathlib/Algebra/Ring/Units.lean

@@ -95,8 +95,8 @@ protected theorem map_neg {F : Type*} [Ring β] [FunLike F α β] [RingHomClass
   ext (by simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg])
 
 protected theorem map_neg_one {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β]
-    (f : F) : map (f : α →* β) (-1) = -1 :=
-  by simp only [Units.map_neg, map_one]
+    (f : F) : map (f : α →* β) (-1) = -1 := by
+  simp only [Units.map_neg, map_one]
 
 end Ring
 

Mathlib/CategoryTheory/ConcreteCategory/Bundled.lean

@@ -14,9 +14,10 @@ import Mathlib.Mathport.Rename
 
 `Bundled c` provides a uniform structure for bundling a type equipped with a type class.
 
-We provide `Category` instances for these in `CategoryTheory/ConcreteCategory/UnbundledHom.lean`
+We provide `Category` instances for these in
+`Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.lean`
 (for categories with unbundled homs, e.g. topological spaces)
-and in `CategoryTheory/ConcreteCategory/BundledHom.lean`
+and in `Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean`
 (for categories with bundled homs, e.g. monoids).
 -/
 

Mathlib/Data/Fintype/Basic.lean

@@ -623,12 +623,12 @@ def ofIsEmpty [IsEmpty α] : Fintype α :=
   ⟨∅, isEmptyElim⟩
 #align fintype.of_is_empty Fintype.ofIsEmpty
 
-/-- Note: this lemma is specifically about `Fintype.of_isEmpty`. For a statement about
+/-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
 arbitrary `Fintype` instances, use `Finset.univ_eq_empty`. -/
 @[simp]
-theorem univ_of_isEmpty [IsEmpty α] : @univ α Fintype.ofIsEmpty = ∅ :=
+theorem univ_ofIsEmpty [IsEmpty α] : @univ α Fintype.ofIsEmpty = ∅ :=
   rfl
-#align fintype.univ_of_is_empty Fintype.univ_of_isEmpty
+#align fintype.univ_of_is_empty Fintype.univ_ofIsEmpty
 
 instance : Fintype Empty := Fintype.ofIsEmpty
 instance : Fintype PEmpty := Fintype.ofIsEmpty

Mathlib/Data/Fintype/Card.lean

@@ -225,9 +225,9 @@ theorem card_unique [Unique α] [h : Fintype α] : Fintype.card α = 1 :=
 /-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
 arbitrary `Fintype` instances, use `Fintype.card_eq_zero`. -/
 @[simp]
-theorem card_of_isEmpty [IsEmpty α] : @Fintype.card α Fintype.ofIsEmpty = 0 :=
+theorem card_ofIsEmpty [IsEmpty α] : @Fintype.card α Fintype.ofIsEmpty = 0 :=
   rfl
-#align fintype.card_of_is_empty Fintype.card_of_isEmpty
+#align fintype.card_of_is_empty Fintype.card_ofIsEmpty
 
 end Fintype
 

Mathlib/RingTheory/WittVector/Defs.lean

@@ -11,20 +11,20 @@ import Mathlib.RingTheory.WittVector.StructurePolynomial
 # Witt vectors
 
 In this file we define the type of `p`-typical Witt vectors and ring operations on it.
-The ring axioms are verified in `RingTheory.WittVector.Basic`.
+The ring axioms are verified in `Mathlib/RingTheory/WittVector/Basic.lean`.
 
 For a fixed commutative ring `R` and prime `p`,
 a Witt vector `x : 𝕎 R` is an infinite sequence `ℕ → R` of elements of `R`.
 However, the ring operations `+` and `*` are not defined in the obvious component-wise way.
 Instead, these operations are defined via certain polynomials
-using the machinery in `StructurePolynomial.lean`.
+using the machinery in `Mathlib/RingTheory/WittVector/StructurePolynomial.lean`.
 The `n`th value of the sum of two Witt vectors can depend on the `0`-th through `n`th values
 of the summands. This effectively simulates a “carrying” operation.
 
 ## Main definitions
 
-* `witt_vector p R`: the type of `p`-typical Witt vectors with coefficients in `R`.
-* `witt_vector.coeff x n`: projects the `n`th value of the Witt vector `x`.
+* `WittVector p R`: the type of `p`-typical Witt vectors with coefficients in `R`.
+* `WittVector.coeff x n`: projects the `n`th value of the Witt vector `x`.
 
 ## Notation
 
@@ -40,12 +40,12 @@ We use notation `𝕎 R`, entered `\bbW`, for the Witt vectors over `R`.
 
 noncomputable section
 
-/-- `witt_vector p R` is the ring of `p`-typical Witt vectors over the commutative ring `R`,
+/-- `WittVector p R` is the ring of `p`-typical Witt vectors over the commutative ring `R`,
 where `p` is a prime number.
 
 If `p` is invertible in `R`, this ring is isomorphic to `ℕ → R` (the product of `ℕ` copies of `R`).
-If `R` is a ring of characteristic `p`, then `witt_vector p R` is a ring of characteristic `0`.
-The canonical example is `witt_vector p (zmod p)`,
+If `R` is a ring of characteristic `p`, then `WittVector p R` is a ring of characteristic `0`.
+The canonical example is `WittVector p (ZMod p)`,
 which is isomorphic to the `p`-adic integers `ℤ_[p]`. -/
 structure WittVector (p : ℕ) (R : Type*) where mk' ::
   coeff : ℕ → R
@@ -56,13 +56,11 @@ def WittVector.mk (p : ℕ) {R : Type*} (coeff : ℕ → R) : WittVector p R :=
 
 variable {p : ℕ}
 
--- mathport name: expr𝕎
 /- We cannot make this `localized` notation, because the `p` on the RHS doesn't occur on the left
 Hiding the `p` in the notation is very convenient, so we opt for repeating the `local notation`
 in other files that use Witt vectors. -/
-local notation "𝕎" => WittVector p
+local notation "𝕎" => WittVector p -- type as `\bbW`
 
--- type as `\bbW`
 namespace WittVector
 
 variable {R : Type*}
@@ -95,7 +93,7 @@ theorem coeff_mk (x : ℕ → R) : (mk p x).coeff = x :=
 #align witt_vector.coeff_mk WittVector.coeff_mk
 
 /- These instances are not needed for the rest of the development,
-but it is interesting to establish early on that `witt_vector p` is a lawful functor. -/
+but it is interesting to establish early on that `WittVector p` is a lawful functor. -/
 instance : Functor (WittVector p) where
   map f v := mk p (f ∘ v.coeff)
   mapConst a _ := mk p fun _ => a
@@ -160,7 +158,7 @@ def wittPow (n : ℕ) : ℕ → MvPolynomial (Fin 1 × ℕ) ℤ :=
 variable {p}
 
 
-/-- An auxiliary definition used in `witt_vector.eval`.
+/-- An auxiliary definition used in `WittVector.eval`.
 Evaluates a polynomial whose variables come from the disjoint union of `k` copies of `ℕ`,
 with a curried evaluation `x`.
 This can be defined more generally but we use only a specific instance here. -/
@@ -173,8 +171,9 @@ disjoint union of `k` copies of `ℕ`, and let `xᵢ` be a Witt vector for `0 
 
 `eval φ x` evaluates `φ` mapping the variable `X_(i, n)` to the `n`th coefficient of `xᵢ`.
 
-Instantiating `φ` with certain polynomials defined in `structure_polynomial.lean` establishes the
-ring operations on `𝕎 R`. For example, `witt_vector.witt_add` is such a `φ` with `k = 2`;
+Instantiating `φ` with certain polynomials defined in
+`Mathlib/RingTheory/WittVector/StructurePolynomial.lean` establishes the
+ring operations on `𝕎 R`. For example, `WittVector.wittAdd` is such a `φ` with `k = 2`;
 evaluating this at `(x₀, x₁)` gives us the sum of two Witt vectors `x₀ + x₁`.
 -/
 def eval {k : ℕ} (φ : ℕ → MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → 𝕎 R) : 𝕎 R :=
@@ -353,16 +352,19 @@ theorem v2_coeff {p' R'} (x y : WittVector p' R') (i : Fin 2) :
 
 -- Porting note: the lemmas below needed `coeff_mk` added to the `simp` calls
 
-theorem add_coeff (x y : 𝕎 R) (n : ℕ) : (x + y).coeff n = peval (wittAdd p n) ![x.coeff, y.coeff] :=
-  by simp [(· + ·), Add.add, eval, coeff_mk]
+theorem add_coeff (x y : 𝕎 R) (n : ℕ) :
+    (x + y).coeff n = peval (wittAdd p n) ![x.coeff, y.coeff] := by
+  simp [(· + ·), Add.add, eval, coeff_mk]
 #align witt_vector.add_coeff WittVector.add_coeff
 
-theorem sub_coeff (x y : 𝕎 R) (n : ℕ) : (x - y).coeff n = peval (wittSub p n) ![x.coeff, y.coeff] :=
-  by simp [(· - ·), Sub.sub, eval, coeff_mk]
+theorem sub_coeff (x y : 𝕎 R) (n : ℕ) :
+    (x - y).coeff n = peval (wittSub p n) ![x.coeff, y.coeff] := by
+  simp [(· - ·), Sub.sub, eval, coeff_mk]
 #align witt_vector.sub_coeff WittVector.sub_coeff
 
-theorem mul_coeff (x y : 𝕎 R) (n : ℕ) : (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff] :=
-  by simp [(· * ·), Mul.mul, eval, coeff_mk]
+theorem mul_coeff (x y : 𝕎 R) (n : ℕ) :
+    (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff] := by
+  simp [(· * ·), Mul.mul, eval, coeff_mk]
 #align witt_vector.mul_coeff WittVector.mul_coeff
 
 theorem neg_coeff (x : 𝕎 R) (n : ℕ) : (-x).coeff n = peval (wittNeg p n) ![x.coeff] := by
@@ -379,8 +381,9 @@ theorem zsmul_coeff (m : ℤ) (x : 𝕎 R) (n : ℕ) :
   simp [(· • ·), SMul.smul, eval, Matrix.cons_fin_one, coeff_mk]
 #align witt_vector.zsmul_coeff WittVector.zsmul_coeff
 
-theorem pow_coeff (m : ℕ) (x : 𝕎 R) (n : ℕ) : (x ^ m).coeff n = peval (wittPow p m n) ![x.coeff] :=
-  by simp [(· ^ ·), Pow.pow, eval, Matrix.cons_fin_one, coeff_mk]
+theorem pow_coeff (m : ℕ) (x : 𝕎 R) (n : ℕ) :
+    (x ^ m).coeff n = peval (wittPow p m n) ![x.coeff] := by
+  simp [(· ^ ·), Pow.pow, eval, Matrix.cons_fin_one, coeff_mk]
 #align witt_vector.pow_coeff WittVector.pow_coeff
 
 theorem add_coeff_zero (x y : 𝕎 R) : (x + y).coeff 0 = x.coeff 0 + y.coeff 0 := by

Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

@@ -33,7 +33,7 @@ This construction is described in Dupuis, Lewis, and Macbeth,
 We approximately follow an approach sketched on MathOverflow:
 <https://mathoverflow.net/questions/62468/about-frobenius-of-witt-vectors>
 
-The result is a dependency for the proof of `witt_vector.isocrystal_classification`,
+The result is a dependency for the proof of `WittVector.isocrystal_classification`,
 the classification of one-dimensional isocrystals over an algebraically closed field.
 -/
 
@@ -54,7 +54,7 @@ namespace RecursionMain
 
 The first coefficient of our solution vector is easy to define below.
 In this section we focus on the recursive case.
-The goal is to turn `witt_poly_prod n` into a univariate polynomial
+The goal is to turn `WittVector.wittPolyProd n` into a univariate polynomial
 whose variable represents the `n`th coefficient of `x` in `x * a`.
 
 -/
@@ -205,8 +205,8 @@ noncomputable def frobeniusRotationCoeff {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coef
 decreasing_by apply Fin.is_lt
 #align witt_vector.frobenius_rotation_coeff WittVector.frobeniusRotationCoeff
 
-/-- For nonzero `a₁` and `a₂`, `frobenius_rotation a₁ a₂` is a Witt vector that satisfies the
-equation `frobenius (frobenius_rotation a₁ a₂) * a₁ = (frobenius_rotation a₁ a₂) * a₂`.
+/-- For nonzero `a₁` and `a₂`, `frobeniusRotation a₁ a₂` is a Witt vector that satisfies the
+equation `frobenius (frobeniusRotation a₁ a₂) * a₁ = (frobeniusRotation a₁ a₂) * a₂`.
 -/
 def frobeniusRotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) : 𝕎 k :=
   WittVector.mk p (frobeniusRotationCoeff p ha₁ ha₂)