[Merged by Bors] - chore: tidy various files

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -1201,7 +1201,6 @@ section Multiplicative
 
 open Multiplicative
 
--- Porting note: the proof became a little roundabout while porting.
 @[simp]
 theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b :=
   mul_comm _ _

Mathlib/Algebra/GroupRingAction/Basic.lean

@@ -63,10 +63,10 @@ def MulSemiringAction.toRingHom [MulSemiringAction M R] (x : M) : R →+* R :=
   { MulDistribMulAction.toMonoidHom R x, DistribMulAction.toAddMonoidHom R x with }
 #align mul_semiring_action.to_ring_hom MulSemiringAction.toRingHom
 
-theorem to_ring_hom_injective [MulSemiringAction M R] [FaithfulSMul M R] :
+theorem toRingHom_injective [MulSemiringAction M R] [FaithfulSMul M R] :
     Function.Injective (MulSemiringAction.toRingHom M R) := fun _ _ h =>
   eq_of_smul_eq_smul fun r => RingHom.ext_iff.1 h r
-#align to_ring_hom_injective to_ring_hom_injective
+#align to_ring_hom_injective toRingHom_injective
 
 /-- Each element of the group defines a semiring isomorphism. -/
 @[simps]
@@ -78,7 +78,7 @@ section
 
 variable {M N}
 
-/-- Compose a `mul_semiring_action` with a `monoid_hom`, with action `f r' • m`.
+/-- Compose a `MulSemiringAction` with a `MonoidHom`, with action `f r' • m`.
 See note [reducible non-instances]. -/
 @[reducible]
 def MulSemiringAction.compHom (f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R :=

Mathlib/Algebra/Hom/Aut.lean

@@ -27,7 +27,7 @@ equivalences (and other files that use them) before the group structure is defin
 
 ## Tags
 
-mul_aut, add_aut
+MulAut, AddAut
 -/
 
 
@@ -50,13 +50,13 @@ This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.
 -/
 instance : Group (MulAut M) := by
   refine'
-            { mul := fun g h => MulEquiv.trans h g
-              one := MulEquiv.refl M
-              inv := MulEquiv.symm
-              div := fun g h => MulEquiv.trans h.symm g
-              npow := @npowRec _ ⟨MulEquiv.refl M⟩ ⟨fun g h => MulEquiv.trans h g⟩
-              zpow := @zpowRec _ ⟨MulEquiv.refl M⟩ ⟨fun g h => MulEquiv.trans h g⟩ ⟨MulEquiv.symm⟩
-              .. } <;>
+  { mul := fun g h => MulEquiv.trans h g
+    one := MulEquiv.refl M
+    inv := MulEquiv.symm
+    div := fun g h => MulEquiv.trans h.symm g
+    npow := @npowRec _ ⟨MulEquiv.refl M⟩ ⟨fun g h => MulEquiv.trans h g⟩
+    zpow := @zpowRec _ ⟨MulEquiv.refl M⟩ ⟨fun g h => MulEquiv.trans h g⟩ ⟨MulEquiv.symm⟩
+    .. } <;>
   intros <;>
   ext <;>
   try rfl
@@ -115,8 +115,7 @@ def toPerm : MulAut M →* Equiv.Perm M := by
 /-- The tautological action by `MulAut M` on `M`.
 
 This generalizes `Function.End.applyMulAction`. -/
-instance applyMulDistribMulAction {M} [Monoid M] :
-    MulDistribMulAction (MulAut M) M where
+instance applyMulDistribMulAction {M} [Monoid M] : MulDistribMulAction (MulAut M) M where
   smul := (· <| ·)
   one_smul _ := rfl
   mul_smul _ _ _ := rfl
@@ -178,13 +177,13 @@ This means that multiplication agrees with composition, `(g*h)(x) = g (h x)`.
 -/
 instance group : Group (AddAut A) := by
   refine'
-            { mul := fun g h => AddEquiv.trans h g
-              one := AddEquiv.refl A
-              inv := AddEquiv.symm
-              div := fun g h => AddEquiv.trans h.symm g
-              npow := @npowRec _ ⟨AddEquiv.refl A⟩ ⟨fun g h => AddEquiv.trans h g⟩
-              zpow := @zpowRec _ ⟨AddEquiv.refl A⟩ ⟨fun g h => AddEquiv.trans h g⟩ ⟨AddEquiv.symm⟩
-              .. } <;>
+  { mul := fun g h => AddEquiv.trans h g
+    one := AddEquiv.refl A
+    inv := AddEquiv.symm
+    div := fun g h => AddEquiv.trans h.symm g
+    npow := @npowRec _ ⟨AddEquiv.refl A⟩ ⟨fun g h => AddEquiv.trans h g⟩
+    zpow := @zpowRec _ ⟨AddEquiv.refl A⟩ ⟨fun g h => AddEquiv.trans h g⟩ ⟨AddEquiv.symm⟩
+    .. } <;>
   intros <;>
   ext <;>
   try rfl
@@ -244,8 +243,7 @@ def toPerm : AddAut A →* Equiv.Perm A := by
 /-- The tautological action by `AddAut A` on `A`.
 
 This generalizes `Function.End.applyMulAction`. -/
-instance applyDistribMulAction {A} [AddMonoid A] :
-    DistribMulAction (AddAut A) A where
+instance applyDistribMulAction {A} [AddMonoid A] : DistribMulAction (AddAut A) A where
   smul := (· <| ·)
   smul_zero := AddEquiv.map_zero
   smul_add := AddEquiv.map_add

Mathlib/Algebra/Ring/Prod.lean

@@ -16,14 +16,14 @@ import Mathlib.Algebra.Order.Group.Prod
 /-!
 # Semiring, ring etc structures on `R × S`
 
-In this file we define two-binop (`semiring`, `ring` etc) structures on `R × S`. We also prove
-trivial `simp` lemmas, and define the following operations on `ring_hom`s and similarly for
-`non_unital_ring_hom`s:
-
-* `fst R S : R × S →+* R`, `snd R S : R × S →+* S`: projections `prod.fst` and `prod.snd`
-  as `ring_hom`s;
-* `f.prod g : `R →+* S × T`: sends `x` to `(f x, g x)`;
-* `f.prod_map g : `R × S → R' × S'`: `prod.map f g` as a `ring_hom`,
+In this file we define two-binop (`Semiring`, `Ring` etc) structures on `R × S`. We also prove
+trivial `simp` lemmas, and define the following operations on `RingHom`s and similarly for
+`NonUnitalRingHom`s:
+
+* `fst R S : R × S →+* R`, `snd R S : R × S →+* S`: projections `Prod.fst` and `Prod.snd`
+  as `RingHom`s;
+* `f.prod g : R →+* S × T`: sends `x` to `(f x, g x)`;
+* `f.prod_map g : R × S → R' × S'`: `Prod.map f g` as a `RingHom`,
   sends `(x, y)` to `(f x, g y)`.
 -/
 
@@ -37,19 +37,19 @@ instance [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 `non_unital_non_assoc_semiring`s is a `non_unital_non_assoc_semiring`. -/
+/-- Product of two `NonUnitalNonAssocSemiring`s is a `NonUnitalNonAssocSemiring`. -/
 instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
     NonUnitalNonAssocSemiring (R × S) :=
   { inferInstanceAs (AddCommMonoid (R × S)),
     inferInstanceAs (Distrib (R × S)),
     inferInstanceAs (MulZeroClass (R × S)) with }
 
-/-- Product of two `non_unital_semiring`s is a `non_unital_semiring`. -/
+/-- Product of two `NonUnitalSemiring`s is a `NonUnitalSemiring`. -/
 instance [NonUnitalSemiring R] [NonUnitalSemiring S] : NonUnitalSemiring (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
     inferInstanceAs (SemigroupWithZero (R × S)) with }
 
-/-- Product of two `non_assoc_semiring`s is a `non_assoc_semiring`. -/
+/-- Product of two `NonAssocSemiring`s is a `NonAssocSemiring`. -/
 instance [NonAssocSemiring R] [NonAssocSemiring S] : NonAssocSemiring (R × S) :=
   { inferInstanceAs (NonUnitalNonAssocSemiring (R × S)),
     inferInstanceAs (MulZeroOneClass (R × S)),
@@ -61,7 +61,7 @@ instance [Semiring R] [Semiring S] : Semiring (R × S) :=
     inferInstanceAs (NonAssocSemiring (R × S)),
     inferInstanceAs (MonoidWithZero (R × S)) with }
 
-/-- Product of two `non_unital_comm_semiring`s is a `non_unital_comm_semiring`. -/
+/-- Product of two `NonUnitalCommSemiring`s is a `NonUnitalCommSemiring`. -/
 instance [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] : NonUnitalCommSemiring (R × S) :=
   { inferInstanceAs (NonUnitalSemiring (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
 
@@ -88,7 +88,7 @@ instance [Ring R] [Ring S] : Ring (R × S) :=
     inferInstanceAs (AddCommGroup (R × S)),
     inferInstanceAs (AddGroupWithOne (R × S)) with }
 
-/-- Product of two `non_unital_comm_ring`s is a `non_unital_comm_ring`. -/
+/-- Product of two `NonUnitalCommRing`s is a `NonUnitalCommRing`. -/
 instance [NonUnitalCommRing R] [NonUnitalCommRing S] : NonUnitalCommRing (R × S) :=
   { inferInstanceAs (NonUnitalRing (R × S)), inferInstanceAs (CommSemigroup (R × S)) with }
 
@@ -162,7 +162,7 @@ variable [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnita
 
 variable (f : R →ₙ+* R') (g : S →ₙ+* S')
 
-/-- `prod.map` as a `non_unital_ring_hom`. -/
+/-- `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
@@ -249,7 +249,7 @@ variable [NonAssocSemiring R'] [NonAssocSemiring S'] [NonAssocSemiring T]
 
 variable (f : R →+* R') (g : S →+* S')
 
-/-- `prod.map` as a `ring_hom`. -/
+/-- `Prod.map` as a `RingHom`. -/
 def prodMap : R × S →+* R' × S' :=
   (f.comp (fst R S)).prod (g.comp (snd R S))
 #align ring_hom.prod_map RingHom.prodMap
@@ -307,7 +307,7 @@ variable (R S) [Subsingleton S]
 
 /-- A ring `R` is isomorphic to `R × S` when `S` is the zero ring -/
 @[simps]
-def prodZeroRing : R ≃+* R × S where 
+def prodZeroRing : R ≃+* R × S where
   toFun x := (x, 0)
   invFun := Prod.fst
   map_add' := by simp
@@ -318,7 +318,7 @@ def prodZeroRing : R ≃+* R × S where
 
 /-- A ring `R` is isomorphic to `S × R` when `S` is the zero ring -/
 @[simps]
-def zeroRingProd : R ≃+* S × R where 
+def zeroRingProd : R ≃+* S × R where
   toFun x := (0, x)
   invFun := Prod.snd
   map_add' := by simp

Mathlib/Algebra/SMulWithZero.lean

@@ -14,7 +14,7 @@ import Mathlib.GroupTheory.GroupAction.Opposite
 import Mathlib.GroupTheory.GroupAction.Prod
 
 /-!
-# Introduce `smul_with_zero`
+# Introduce `SMulWithZero`
 
 In analogy with the usual monoid action on a Type `M`, we introduce an action of a
 `MonoidWithZero` on a Type with `0`.
@@ -46,24 +46,22 @@ section Zero
 
 variable (R M)
 
-/-- `smulWithZero` is a class consisting of a Type `R` with `0 ∈ R` and a scalar multiplication
+/-- `SMulWithZero` is a class consisting of a Type `R` with `0 ∈ R` and a scalar multiplication
 of `R` on a Type `M` with `0`, such that the equality `r • m = 0` holds if at least one among `r`
 or `m` equals `0`. -/
 class SMulWithZero [Zero R] [Zero M] extends SMulZeroClass R M where
   /-- Scalar multiplication by the scalar `0` is `0`. -/
   zero_smul : ∀ m : M, (0 : R) • m = 0
 #align smul_with_zero SMulWithZero
 
-instance MulZeroClass.toSMulWithZero [MulZeroClass R] :
-    SMulWithZero R R where
+instance MulZeroClass.toSMulWithZero [MulZeroClass R] : SMulWithZero R R where
   smul := (· * ·)
   smul_zero := mul_zero
   zero_smul := zero_mul
 #align mul_zero_class.to_smul_with_zero MulZeroClass.toSMulWithZero
 
 /-- Like `MulZeroClass.toSMulWithZero`, but multiplies on the right. -/
-instance MulZeroClass.toOppositeSMulWithZero [MulZeroClass R] :
-    SMulWithZero Rᵐᵒᵖ R where
+instance MulZeroClass.toOppositeSMulWithZero [MulZeroClass R] : SMulWithZero Rᵐᵒᵖ R where
   smul := (· • ·)
   smul_zero _ := zero_mul _
   zero_smul := mul_zero
@@ -106,8 +104,7 @@ protected def Function.Surjective.smulWithZero (f : ZeroHom M M') (hf : Function
 variable (M)
 
 /-- Compose a `SMulWithZero` with a `ZeroHom`, with action `f r' • m` -/
-def SMulWithZero.compHom (f : ZeroHom R' R) :
-    SMulWithZero R' M where
+def SMulWithZero.compHom (f : ZeroHom R' R) : SMulWithZero R' M where
   smul := (· • ·) ∘ f
   smul_zero m := smul_zero (f m)
   zero_smul m := by show (f 0) • m = 0 ; rw [map_zero, zero_smul]
@@ -116,14 +113,12 @@ def SMulWithZero.compHom (f : ZeroHom R' R) :
 
 end Zero
 
-instance AddMonoid.natSMulWithZero [AddMonoid M] :
-    SMulWithZero ℕ M where
+instance AddMonoid.natSMulWithZero [AddMonoid M] : SMulWithZero ℕ M where
   smul_zero := _root_.nsmul_zero
   zero_smul := zero_nsmul
 #align add_monoid.nat_smul_with_zero AddMonoid.natSMulWithZero
 
-instance AddGroup.intSMulWithZero [AddGroup M] :
-    SMulWithZero ℤ M where
+instance AddGroup.intSMulWithZero [AddGroup M] : SMulWithZero ℤ M where
   smul_zero := zsmul_zero
   zero_smul := zero_zsmul
 #align add_group.int_smul_with_zero AddGroup.intSMulWithZero
@@ -157,7 +152,7 @@ instance MonoidWithZero.toMulActionWithZero : MulActionWithZero R R :=
 #align monoid_with_zero.to_mul_action_with_zero MonoidWithZero.toMulActionWithZero
 
 /-- Like `MonoidWithZero.toMulActionWithZero`, but multiplies on the right. See also
-`semiring.toOppositeModule` -/
+`Semiring.toOppositeModule` -/
 instance MonoidWithZero.toOppositeMulActionWithZero : MulActionWithZero Rᵐᵒᵖ R :=
   { MulZeroClass.toOppositeSMulWithZero R, Monoid.toOppositeMulAction R with }
 #align monoid_with_zero.to_opposite_mul_action_with_zero MonoidWithZero.toOppositeMulActionWithZero

Mathlib/Data/Int/Order/Basic.lean

@@ -148,7 +148,7 @@ where
     conv => rhs; apply (add_zero b).symm
     rw [Int.add_lt_add_iff_left]; apply negSucc_lt_zero
 
-/-- See `int.induction_on'` for an induction in both directions. -/
+/-- See `Int.inductionOn'` for an induction in both directions. -/
 protected theorem le_induction {P : ℤ → Prop} {m : ℤ} (h0 : P m)
     (h1 : ∀ n : ℤ, m ≤ n → P n → P (n + 1)) (n : ℤ) : m ≤ n → P n := by
   refine Int.inductionOn' n m ?_ ?_ ?_
@@ -161,7 +161,7 @@ protected theorem le_induction {P : ℤ → Prop} {m : ℤ} (h0 : P m)
     exact lt_irrefl k (le_sub_one_iff.mp (hle.trans hle'))
 #align int.le_induction Int.le_induction
 
-/-- See `int.induction_on'` for an induction in both directions. -/
+/-- See `Int.inductionOn'` for an induction in both directions. -/
 protected theorem le_induction_down {P : ℤ → Prop} {m : ℤ} (h0 : P m)
     (h1 : ∀ n : ℤ, n ≤ m → P n → P (n - 1)) (n : ℤ) : n ≤ m → P n := by
   refine Int.inductionOn' n m ?_ ?_ ?_

Mathlib/Data/Nat/Bits.lean

@@ -34,7 +34,7 @@ universe u
 
 variable {n : ℕ}
 
-/-! ### `bodd_div2` and `bodd` -/
+/-! ### `boddDiv2_eq` and `bodd` -/
 
 
 @[simp]
@@ -65,9 +65,9 @@ theorem div2_bit1 (n) : div2 (bit1 n) = n :=
 /-! ### `bit0` and `bit1` -/
 
 -- There is no need to prove `bit0_eq_zero : bit0 n = 0 ↔ n = 0`
--- as this is true for any `[semiring R] [no_zero_divisors R] [char_zero R]`
+-- as this is true for any `[Semiring R] [NoZeroDivisors R] [CharZero R]`
 -- However the lemmas `bit0_eq_bit0`, `bit1_eq_bit1`, `bit1_eq_one`, `one_eq_bit1`
--- need `[ring R] [no_zero_divisors R] [char_zero R]` in general,
+-- need `[Ring R] [NoZeroDivisors R] [CharZero R]` in general,
 -- so we prove `ℕ` specialized versions here.
 @[simp]
 theorem bit0_eq_bit0 {m n : ℕ} : bit0 m = bit0 n ↔ m = n :=
@@ -115,8 +115,8 @@ theorem bit1_mod_two : bit1 n % 2 = 1 := by
 
 theorem pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n := by
   cases n
-  cases h
-  apply succ_pos
+  · cases h
+  · apply succ_pos
 #align nat.pos_of_bit0_pos Nat.pos_of_bit0_pos
 
 @[simp]
@@ -162,18 +162,17 @@ theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = fal
 #align nat.bit_eq_zero_iff Nat.bit_eq_zero_iff
 
 /--
-The same as `binary_rec_eq`,
+The same as `binaryRec_eq`,
 but that one unfortunately requires `f` to be the identity when appending `false` to `0`.
 Here, we allow you to explicitly say that that case is not happening,
 i.e. supplying `n = 0 → b = true`. -/
-@[nolint unusedHavesSuffices]
-theorem binary_rec_eq' {C : ℕ → Sort _} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
+theorem binaryRec_eq' {C : ℕ → Sort _} {z : C 0} {f : ∀ b n, C n → C (bit b n)} (b n)
     (h : f false 0 z = z ∨ (n = 0 → b = true)) :
     binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
   rw [binaryRec]
   split_ifs with h'
   · rcases bit_eq_zero_iff.mp h' with ⟨rfl, rfl⟩
-    rw [binary_rec_zero]
+    rw [binaryRec_zero]
     simp only [imp_false, or_false_iff, eq_self_iff_true, not_true] at h
     exact h.symm
   · dsimp only []
@@ -184,10 +183,10 @@ theorem binary_rec_eq' {C : ℕ → Sort _} {z : C 0} {f : ∀ b n, C n → C (b
     rw [bodd_bit, div2_bit]
     intros
     rfl
-#align nat.binary_rec_eq' Nat.binary_rec_eq'
+#align nat.binary_rec_eq' Nat.binaryRec_eq'
 
-/-- The same as `binary_rec`, but the induction step can assume that if `n=0`,
-  the bit being appended is `tt`-/
+/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
+  the bit being appended is `true`-/
 @[elab_as_elim]
 def binaryRec' {C : ℕ → Sort _} (z : C 0) (f : ∀ b n, (n = 0 → b = true) → C n → C (bit b n)) :
     ∀ n, C n :=
@@ -199,7 +198,7 @@ def binaryRec' {C : ℕ → Sort _} (z : C 0) (f : ∀ b n, (n = 0 → b = true)
       simpa using h
 #align nat.binary_rec' Nat.binaryRec'
 
-/-- The same as `binary_rec`, but special casing both 0 and 1 as base cases -/
+/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
 @[elab_as_elim]
 def binaryRecFromOne {C : ℕ → Sort _} (z₀ : C 0) (z₁ : C 1) (f : ∀ b n, n ≠ 0 → C n → C (bit b n)) :
     ∀ n, C n :=
@@ -217,7 +216,7 @@ theorem zero_bits : bits 0 = [] := by simp [Nat.bits]
 @[simp]
 theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
     (bit b n).bits = b :: n.bits := by
-  rw [Nat.bits, binary_rec_eq']
+  rw [Nat.bits, binaryRec_eq']
   simpa
 #align nat.bits_append_bit Nat.bits_append_bit
 
@@ -237,7 +236,8 @@ theorem one_bits : Nat.bits 1 = [true] := by
 #align nat.one_bits Nat.one_bits
 
 -- TODO Find somewhere this can live.
--- example : bits 3423 = [tt, tt, tt, tt, tt, ff, tt, ff, tt, ff, tt, tt] := by norm_num
+-- example : bits 3423 = [true, true, true, true, true, false, true, false, true, false, true, true]
+-- := by norm_num
 
 theorem bodd_eq_bits_head (n : ℕ) : n.bodd = n.bits.headI := by
   induction' n using Nat.binaryRec' with b n h _; · simp