chore: tidy various files (#1412)

Author: Ruben-VandeVelde

Mathlib/Algebra/Associated.lean

@@ -847,9 +847,9 @@ protected def mkMonoidHom : α →* Associates α :=
 #align associates.mk_monoid_hom Associates.mkMonoidHom
 
 @[simp]
-theorem mk_monoidHom_apply (a : α) : Associates.mkMonoidHom a = Associates.mk a :=
+theorem mkMonoidHom_apply (a : α) : Associates.mkMonoidHom a = Associates.mk a :=
   rfl
-#align associates.mk_monoid_hom_apply Associates.mk_monoidHom_apply
+#align associates.mk_monoid_hom_apply Associates.mkMonoidHom_apply
 
 theorem associated_map_mk {f : Associates α →* α} (hinv : Function.RightInverse f Associates.mk)
     (a : α) : a ~ᵤ f (Associates.mk a) :=

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -212,7 +212,7 @@ variable [CancelCommMonoidWithZero α] [NormalizationMonoid α]
 
 attribute [local instance] Associated.setoid
 
-/-- Maps an element of `associates` back to the normalized element of its associate class -/
+/-- Maps an element of `Associates` back to the normalized element of its associate class -/
 protected def out : Associates α → α :=
   (Quotient.lift (normalize : α → α)) fun a _ ⟨_, hu⟩ =>
     hu ▸ normalize_eq_normalize ⟨_, rfl⟩ (Units.mul_right_dvd.2 <| dvd_refl a)
@@ -395,7 +395,8 @@ theorem gcd_eq_zero_iff [GCDMonoid α] (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b
     (fun h => by
       let ⟨ca, ha⟩ := gcd_dvd_left a b
       let ⟨cb, hb⟩ := gcd_dvd_right a b
-      rw [h, zero_mul] at ha hb; exact ⟨ha, hb⟩)
+      rw [h, zero_mul] at ha hb
+      exact ⟨ha, hb⟩)
     fun ⟨ha, hb⟩ => by
     rw [ha, hb, ← zero_dvd_iff]
     apply dvd_gcd <;> rfl
@@ -821,13 +822,13 @@ theorem lcm_mul_left [NormalizedGCDMonoid α] (a b c : α) :
     fun ha : a ≠ 0 =>
     suffices lcm (a * b) (a * c) = normalize (a * lcm b c) by simpa
     have : a ∣ lcm (a * b) (a * c) := (dvd_mul_right _ _).trans (dvd_lcm_left _ _)
-    let ⟨d, Eq⟩ := this
+    let ⟨d, eq⟩ := this
     lcm_eq_normalize
       (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
-      (Eq.symm ▸
+      (eq.symm ▸
         (mul_dvd_mul_left a <|
-          lcm_dvd ((mul_dvd_mul_iff_left ha).1 <| Eq ▸ dvd_lcm_left _ _)
-            ((mul_dvd_mul_iff_left ha).1 <| Eq ▸ dvd_lcm_right _ _)))
+          lcm_dvd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_left _ _)
+            ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_right _ _)))
 #align lcm_mul_left lcm_mul_left
 
 @[simp]
@@ -905,16 +906,14 @@ section UniqueUnit
 variable [CancelCommMonoidWithZero α] [Unique αˣ]
 
 -- see Note [lower instance priority]
-instance (priority := 100) normalizationMonoidOfUniqueUnits :
-    NormalizationMonoid α where
+instance (priority := 100) normalizationMonoidOfUniqueUnits : NormalizationMonoid α where
   normUnit _ := 1
   normUnit_zero := rfl
   normUnit_mul _ _ := (mul_one 1).symm
   normUnit_coe_units _ := Subsingleton.elim _ _
 #align normalization_monoid_of_unique_units normalizationMonoidOfUniqueUnits
 
-instance uniqueNormalizationMonoidOfUniqueUnits :
-    Unique (NormalizationMonoid α) where
+instance uniqueNormalizationMonoidOfUniqueUnits : Unique (NormalizationMonoid α) where
   default := normalizationMonoidOfUniqueUnits
   uniq := fun ⟨u, _, _, _⟩ => by congr; simp
 #align unique_normalization_monoid_of_unique_units uniqueNormalizationMonoidOfUniqueUnits
@@ -939,8 +938,7 @@ instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) :=
     simp only [hgcd, hlcm]⟩
 #align subsingleton_gcd_monoid_of_unique_units subsingleton_gcdMonoid_of_unique_units
 
-instance subsingleton_normalizedGCDMonoid_of_unique_units :
-    Subsingleton (NormalizedGCDMonoid α) :=
+instance subsingleton_normalizedGCDMonoid_of_unique_units : Subsingleton (NormalizedGCDMonoid α) :=
   ⟨by
     intro a b
     cases' a with a_norm a_gcd
@@ -967,8 +965,7 @@ theorem normalize_eq (x : α) : normalize x = x :=
 
 /-- If a monoid's only unit is `1`, then it is isomorphic to its associates. -/
 @[simps]
-def associatesEquivOfUniqueUnits :
-    Associates α ≃* α where
+def associatesEquivOfUniqueUnits : Associates α ≃* α where
   toFun := Associates.out
   invFun := Associates.mk
   left_inv := Associates.mk_out
@@ -984,7 +981,7 @@ variable [CommRing α] [IsDomain α] [NormalizedGCDMonoid α]
 
 theorem gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c := by
   apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;>
-      rw [dvd_gcd_iff] <;>
+    rw [dvd_gcd_iff] <;>
     refine' ⟨gcd_dvd_left _ _, _⟩
   · rcases h with ⟨d, hd⟩
     rcases gcd_dvd_right a b with ⟨e, he⟩
@@ -1023,7 +1020,7 @@ def normalizationMonoidOfMonoidHomRightInverse [DecidableEq α] (f : Associates
     if a = 0 then 1
     else Classical.choose (Associates.mk_eq_mk_iff_associated.1 (hinv (Associates.mk a)).symm)
   normUnit_zero := if_pos rfl
-  normUnit_mul := fun {a b} ha hb => by
+  normUnit_mul {a b} ha hb := by
     simp_rw [if_neg (mul_ne_zero ha hb), if_neg ha, if_neg hb, Units.ext_iff, Units.val_mul]
     suffices
       a * b * ↑(Classical.choose (associated_map_mk hinv (a * b))) =
@@ -1363,9 +1360,7 @@ variable (G₀ : Type _) [CommGroupWithZero G₀] [DecidableEq G₀]
 
 -- Porting note: very slow; improve performance?
 -- see Note [lower instance priority]
-instance (priority := 100) :
-    NormalizedGCDMonoid
-      G₀ where
+instance (priority := 100) : NormalizedGCDMonoid G₀ where
   normUnit x := if h : x = 0 then 1 else (Units.mk0 x h)⁻¹
   normUnit_zero := dif_pos rfl
   normUnit_mul := fun {x y} x0 y0 => Units.eq_iff.1 (by

Mathlib/Algebra/Order/Monoid/WithTop.lean

@@ -92,24 +92,20 @@ theorem coe_add : ((x + y : α) : WithTop α) = x + y :=
   rfl
 #align with_top.coe_add WithTop.coe_add
 
--- Porting note: Linter says these are syntactic tautologies.
--- Porting note: `bit0` and `bit1` are deprecated. Section can be removed without replacement.
--- section deprecated
--- set_option linter.deprecated false
-
--- --@[norm_cast]
--- @[deprecated]
--- theorem coe_bit0 : ((bit0 x : α) : WithTop α) = bit0 x :=
---   rfl
--- #align with_top.coe_bit0 WithTop.coe_bit0
+section deprecated
+set_option linter.deprecated false
 
--- -- @[norm_cast]
--- @[deprecated]
--- theorem coe_bit1 [One α] {a : α} : ((bit1 a : α) : WithTop α) = bit1 a :=
---   rfl
--- #align with_top.coe_bit1 WithTop.coe_bit1
+@[norm_cast, deprecated]
+theorem coe_bit0 : ((bit0 x : α) : WithTop α) = (bit0 x : WithTop α) :=
+  rfl
+#align with_top.coe_bit0 WithTop.coe_bit0
+
+@[norm_cast, deprecated]
+theorem coe_bit1 [One α] {a : α} : ((bit1 a : α) : WithTop α) = (bit1 a : WithTop α) :=
+  rfl
+#align with_top.coe_bit1 WithTop.coe_bit1
 
--- end deprecated
+end deprecated
 
 @[simp]
 theorem top_add (a : WithTop α) : ⊤ + a = ⊤ :=
@@ -542,22 +538,22 @@ theorem coe_add (a b : α) : ((a + b : α) : WithBot α) = a + b :=
   rfl
 #align with_bot.coe_add WithBot.coe_add
 
--- Porting note: Linter says these are syntactical tautologies now.
--- Porting note: `bit0` and `bit1` are deprecated. Section can be removed without replacement.
--- section deprecated
--- set_option linter.deprecated false
+section deprecated
+set_option linter.deprecated false
 
--- @[deprecated]
--- theorem coe_bit0 : ((bit0 x : α) : WithBot α) = bit0 x :=
---   rfl
--- #align with_bot.coe_bit0 WithBot.coe_bit0
+-- Porting note: added norm_cast
+@[norm_cast, deprecated]
+theorem coe_bit0 : ((bit0 x : α) : WithBot α) = (bit0 x : WithBot α) :=
+  rfl
+#align with_bot.coe_bit0 WithBot.coe_bit0
 
--- @[deprecated]
--- theorem coe_bit1 [One α] {a : α} : ((bit1 a : α) : WithBot α) = bit1 a :=
---   rfl
--- #align with_bot.coe_bit1 WithBot.coe_bit1
+-- Porting note: added norm_cast
+@[norm_cast, deprecated]
+theorem coe_bit1 [One α] {a : α} : ((bit1 a : α) : WithBot α) = (bit1 a : WithBot α) :=
+  rfl
+#align with_bot.coe_bit1 WithBot.coe_bit1
 
--- end deprecated
+end deprecated
 
 @[simp]
 theorem bot_add (a : WithBot α) : ⊥ + a = ⊥ :=

Mathlib/Algebra/Tropical/Basic.lean

@@ -26,7 +26,7 @@ well as the expected implementations of tropical addition and tropical multiplic
 * `Tropical R`: The type synonym of the tropical interpretation of `R`.
     If `[LinearOrder R]`, then addition on `R` is via `min`.
 * `Semiring (Tropical R)`: A `LinearOrderedAddCommMonoidWithTop R`
-    induces a `Semiring (Tropical R)`. If one solely has `[LinearOrderedAddComm<onoid R]`,
+    induces a `Semiring (Tropical R)`. If one solely has `[LinearOrderedAddCommMonoid R]`,
     then the "tropicalization of `R`" would be `Tropical (WithTop R)`.
 
 ## Implementation notes
@@ -61,7 +61,7 @@ variable {R}
 
 namespace Tropical
 
-/-- Reinterpret `x : R` as an element of `tropical R`.
+/-- Reinterpret `x : R` as an element of `Tropical R`.
 See `Tropical.tropEquiv` for the equivalence.
 -/
 --@[pp_nodot] Porting note: not implemented in Lean4
@@ -105,13 +105,13 @@ theorem untrop_trop (x : R) : untrop (trop x) = x :=
 --Porting note: New attribute seems to fix things
 attribute [irreducible] Tropical
 
-theorem left_inverse_trop : Function.LeftInverse (trop : R → Tropical R) untrop :=
+theorem leftInverse_trop : Function.LeftInverse (trop : R → Tropical R) untrop :=
   trop_untrop
-#align tropical.left_inverse_trop Tropical.left_inverse_trop
+#align tropical.left_inverse_trop Tropical.leftInverse_trop
 
-theorem right_inverse_trop : Function.RightInverse (trop : R → Tropical R) untrop :=
+theorem rightInverse_trop : Function.RightInverse (trop : R → Tropical R) untrop :=
   untrop_trop
-#align tropical.right_inverse_trop Tropical.right_inverse_trop
+#align tropical.right_inverse_trop Tropical.rightInverse_trop
 
 /-- Reinterpret `x : R` as an element of `Tropical R`.
 See `Tropical.tropOrderIso` for the order-preserving equivalence. -/
@@ -177,10 +177,10 @@ theorem untrop_le_iff [LE R] {x y : Tropical R} : untrop x ≤ untrop y ↔ x 
   Iff.rfl
 #align tropical.untrop_le_iff Tropical.untrop_le_iff
 
-instance decidableLe [LE R] [DecidableRel ((· ≤ ·) : R → R → Prop)] :
+instance decidableLE [LE R] [DecidableRel ((· ≤ ·) : R → R → Prop)] :
     DecidableRel ((· ≤ ·) : Tropical R → Tropical R → Prop) := fun x y =>
   ‹DecidableRel (· ≤ ·)› (untrop x) (untrop y)
-#align tropical.decidable_le Tropical.decidableLe
+#align tropical.decidable_le Tropical.decidableLE
 
 instance [LT R] : LT (Tropical R) where lt x y := untrop x < untrop y
 
@@ -189,10 +189,10 @@ theorem untrop_lt_iff [LT R] {x y : Tropical R} : untrop x < untrop y ↔ x < y
   Iff.rfl
 #align tropical.untrop_lt_iff Tropical.untrop_lt_iff
 
-instance decidableLt [LT R] [DecidableRel ((· < ·) : R → R → Prop)] :
+instance decidableLT [LT R] [DecidableRel ((· < ·) : R → R → Prop)] :
     DecidableRel ((· < ·) : Tropical R → Tropical R → Prop) := fun x y =>
   ‹DecidableRel (· < ·)› (untrop x) (untrop y)
-#align tropical.decidable_lt Tropical.decidableLt
+#align tropical.decidable_lt Tropical.decidableLT
 
 instance [Preorder R] : Preorder (Tropical R) :=
   { instLETropical, instLTTropical with
@@ -206,14 +206,14 @@ def tropOrderIso [Preorder R] : R ≃o Tropical R :=
 #align tropical.trop_order_iso Tropical.tropOrderIso
 
 @[simp]
-theorem trop_order_iso_coe_fn [Preorder R] : (tropOrderIso : R → Tropical R) = trop :=
+theorem tropOrderIso_coe_fn [Preorder R] : (tropOrderIso : R → Tropical R) = trop :=
   rfl
-#align tropical.trop_order_iso_coe_fn Tropical.trop_order_iso_coe_fn
+#align tropical.trop_order_iso_coe_fn Tropical.tropOrderIso_coe_fn
 
 @[simp]
-theorem trop_order_iso_symm_coe_fn [Preorder R] : (tropOrderIso.symm : Tropical R → R) = untrop :=
+theorem tropOrderIso_symm_coe_fn [Preorder R] : (tropOrderIso.symm : Tropical R → R) = untrop :=
   rfl
-#align tropical.trop_order_iso_symm_coe_fn Tropical.trop_order_iso_symm_coe_fn
+#align tropical.trop_order_iso_symm_coe_fn Tropical.tropOrderIso_symm_coe_fn
 
 theorem trop_monotone [Preorder R] : Monotone (trop : R → Tropical R) := fun _ _ => id
 #align tropical.trop_monotone Tropical.trop_monotone
@@ -264,8 +264,7 @@ variable [LinearOrder R]
 instance : Add (Tropical R) :=
   ⟨fun x y => trop (min (untrop x) (untrop y))⟩
 
-instance : AddCommSemigroup (Tropical
-        R) where
+instance : AddCommSemigroup (Tropical R) where
   add := (· + ·)
   add_assoc _ _ _ := untrop_injective (min_assoc _ _ _)
   add_comm _ _ := untrop_injective (min_comm _ _)
@@ -292,7 +291,7 @@ theorem trop_add_def (x y : Tropical R) : x + y = trop (min (untrop x) (untrop y
 instance : LinearOrder (Tropical R) :=
   { instPartialOrderTropical with
     le_total := fun a b => le_total (untrop a) (untrop b)
-    decidable_le := Tropical.decidableLe
+    decidable_le := Tropical.decidableLE
     max := fun a b => trop (max (untrop a) (untrop b))
     max_def := fun a b => untrop_injective (by simp [max_def]; split_ifs <;> simp)
     min := (· + ·)
@@ -436,8 +435,7 @@ theorem untrop_div [Sub R] (x y : Tropical R) : untrop (x / y) = untrop x - untr
   rfl
 #align tropical.untrop_div Tropical.untrop_div
 
-instance [AddSemigroup R] :
-    Semigroup (Tropical R) where
+instance [AddSemigroup R] : Semigroup (Tropical R) where
   mul := (· * ·)
   mul_assoc _ _ _ := untrop_injective (add_assoc _ _ _)
 
@@ -457,8 +455,7 @@ theorem trop_smul {α : Type _} [SMul α R] (x : R) (n : α) : trop (n • x) =
   rfl
 #align tropical.trop_smul Tropical.trop_smul
 
-instance [AddZeroClass R] : MulOneClass
-      (Tropical R) where
+instance [AddZeroClass R] : MulOneClass (Tropical R) where
   one := 1
   mul := (· * ·)
   one_mul _ := untrop_injective <| zero_add _

Mathlib/Data/Bool/AllAny.lean

@@ -13,7 +13,7 @@ import Mathlib.Data.List.Basic
 /-!
 # Boolean quantifiers
 
-This proves a few properties about `List.all` and `List.any`, which are the `bool` universal and
+This proves a few properties about `List.all` and `List.any`, which are the `Bool` universal and
 existential quantifiers. Their definitions are in core Lean.
 -/
 

Mathlib/Data/List/Infix.lean

@@ -21,7 +21,7 @@ This file proves properties about
 * `List.tails`: The list of prefixes of a list.
 * `insert` on lists
 
-All those (except `insert`) are defined in `Mathlib>Data.List.Defs`.
+All those (except `insert`) are defined in `Mathlib.Data.List.Defs`.
 
 ## Notation
 
@@ -418,9 +418,6 @@ instance decidableSuffix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (
       suffix_cons_iff.symm
 termination_by decidableSuffix l₁ l₂ => (l₁, l₂)
 
-instance foo {a b : Prop }[Decidable a] [Decidable b] : Decidable (a ∨ b) :=
-  instDecidableOr
-
 #align list.decidable_suffix List.decidableSuffix
 
 instance decidableInfix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (l₁ <:+: l₂)
@@ -513,20 +510,17 @@ theorem isInfix.filter (p : α → Prop) [DecidablePred p] ⦃l₁ l₂ : List 
   exact infix_append _ _ _
 #align list.is_infix.filter List.isInfix.filter
 
-instance : IsPartialOrder (List α) (· <+: ·)
-    where
+instance : IsPartialOrder (List α) (· <+: ·) where
   refl := prefix_refl
   trans _ _ _ := isPrefix.trans
   antisymm _ _ h₁ h₂ := eq_of_prefix_of_length_eq h₁ <| h₁.length_le.antisymm h₂.length_le
 
-instance : IsPartialOrder (List α) (· <:+ ·)
-    where
+instance : IsPartialOrder (List α) (· <:+ ·) where
   refl := suffix_refl
   trans _ _ _ := isSuffix.trans
   antisymm _ _ h₁ h₂ := eq_of_suffix_of_length_eq h₁ <| h₁.length_le.antisymm h₂.length_le
 
-instance : IsPartialOrder (List α) (· <:+: ·)
-    where
+instance : IsPartialOrder (List α) (· <:+: ·) where
   refl := infix_refl
   trans _ _ _ := isInfix.trans
   antisymm _ _ h₁ h₂ := eq_of_infix_of_length_eq h₁ <| h₁.length_le.antisymm h₂.length_le