more

Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -456,7 +456,7 @@ lemma sum_ne_zero_of_injOn_supDegree (hs : s ≠ ∅)
   sum_ne_zero_of_injOn_supDegree' ⟨i, hi, hf i hi⟩ hd
 
 variable [Add B]
-variable [CovariantClass B B (· + ·) (· < ·)] [CovariantClass B B (Function.swap (· + ·)) (· < ·)]
+variable [AddLeftStrictMono B] [AddRightStrictMono B]
 
 lemma apply_supDegree_add_supDegree (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) :
     (p * q) (D.invFun (p.supDegree D + q.supDegree D)) = p.leadingCoeff D * q.leadingCoeff D := by
@@ -542,7 +542,7 @@ lemma Monic.mul
 section AddMonoid
 
 variable {A B : Type*} [AddMonoid A] [AddMonoid B] [LinearOrder B] [OrderBot B]
-  [CovariantClass B B (· + ·) (· < ·)] [CovariantClass B B (Function.swap (· + ·)) (· < ·)]
+  [AddLeftStrictMono B] [AddRightStrictMono B]
   {D : A → B} {p : R[A]} {n : ℕ}
 
 lemma Monic.pow

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -232,7 +232,7 @@ theorem abs_sum_of_nonneg' {G : Type*} [LinearOrderedAddCommGroup G] {f : ι →
   rw [abs_of_nonneg (Finset.sum_nonneg' hf)]
 
 section CommMonoid
-variable [CommMonoid α] [LE α] [CovariantClass α α (· * ·) (· ≤ ·)] {s : Finset ι} {f : ι → α}
+variable [CommMonoid α] [LE α] [MulLeftMono α] {s : Finset ι} {f : ι → α}
 
 @[to_additive (attr := simp)]
 lemma mulLECancellable_prod :

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -121,16 +121,16 @@ lemma one_le_prod_of_one_le [Preorder M] [MulLeftMono M] {l : List M}
 
 @[to_additive]
 lemma max_prod_le (l : List α) (f g : α → M) [LinearOrder M]
-    [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)] :
+    [MulLeftMono M] [MulRightMono M] :
     max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod := by
   rw [max_le_iff]
   constructor <;> apply List.prod_le_prod' <;> intros
   · apply le_max_left
   · apply le_max_right
 
 @[to_additive]
-lemma prod_min_le [LinearOrder M] [CovariantClass M M (· * ·) (· ≤ ·)]
-    [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)] (l : List α) (f g : α → M) :
+lemma prod_min_le [LinearOrder M] [MulLeftMono M]
+    [MulRightMono M] (l : List α) (f g : α → M) :
     (l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod := by
   rw [le_min_iff]
   constructor <;> apply List.prod_le_prod' <;> intros

Mathlib/Algebra/Order/Group/CompleteLattice.lean

@@ -15,7 +15,7 @@ open Function Set
 variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
 
 section Right
-variable [CovariantClass G G (swap (· * ·)) (· ≤ ·)]
+variable [MulRightMono G]
 
 @[to_additive]
 lemma ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a :=
@@ -36,7 +36,7 @@ lemma ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f
 end Right
 
 section Left
-variable [CovariantClass G G (· * ·) (· ≤ ·)]
+variable [MulLeftMono G]
 
 @[to_additive]
 lemma mul_ciSup (hf : BddAbove (range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i :=

Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

@@ -21,8 +21,8 @@ open scoped Pointwise
 variable {ι G M : Type*}
 
 section Mul
-variable [Mul M] [Preorder M] [CovariantClass M M (· * ·) (· ≤ ·)]
-  [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {f g : ι → M} {s t : Set M} {a b : M}
+variable [Mul M] [Preorder M] [MulLeftMono M]
+  [MulRightMono M] {f g : ι → M} {s t : Set M} {a b : M}
 
 @[to_additive]
 lemma mul_mem_upperBounds_mul (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) :
@@ -61,8 +61,8 @@ lemma BddBelow.range_mul (hf : BddBelow (range f)) (hg : BddBelow (range g)) :
 end Mul
 
 section InvNeg
-variable [Group G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)]
-  [CovariantClass G G (swap (· * ·)) (· ≤ ·)] {s : Set G} {a : G}
+variable [Group G] [Preorder G] [MulLeftMono G]
+  [MulRightMono G] {s : Set G} {a : G}
 
 @[to_additive (attr := simp)]
 theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s :=

Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean

@@ -34,7 +34,7 @@ variable [One M]
 end One
 
 section Group
-variable [Group M] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
+variable [Group M] [MulLeftMono M] [MulRightMono M]
   {s t : Set M}
 
 @[to_additive]
@@ -84,7 +84,7 @@ variable [One M]
 end One
 
 section Group
-variable [Group M] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
+variable [Group M] [MulLeftMono M] [MulRightMono M]
   (s t : Set M)
 
 @[to_additive]

Mathlib/Algebra/Order/Group/PosPart.lean

@@ -233,7 +233,7 @@ variable [MulLeftMono α]
 @[to_additive (attr := simp) negPart_pos_iff] lemma one_lt_ltOnePart_iff : 1 < a⁻ᵐ ↔ a < 1 :=
   lt_iff_lt_of_le_iff_le <| (one_le_leOnePart _).le_iff_eq.trans leOnePart_eq_one
 
-variable [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
+variable [MulRightMono α]
 
 @[to_additive (attr := simp)] lemma leOnePart_lt : a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b :=
   sup_lt_iff.trans <| by rw [inv_lt']

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -1354,16 +1354,16 @@ protected theorem mul_le_iff_le_one_left [MulOneClass α] [i : @Std.Commutative
     (hb : MulLECancellable b) : MulLECancellable (a * b) :=
   fun c d hcd ↦ hb <| ha <| by rwa [← mul_assoc, ← mul_assoc]
 
-@[to_additive] lemma of_mul_right [Semigroup α] [CovariantClass α α (· * ·) (· ≤ ·)] {a b : α}
+@[to_additive] lemma of_mul_right [Semigroup α] [MulLeftMono α] {a b : α}
     (h : MulLECancellable (a * b)) : MulLECancellable b :=
   fun c d hcd ↦ h <| by rw [mul_assoc, mul_assoc]; exact mul_le_mul_left' hcd _
 
-@[to_additive] lemma of_mul_left [CommSemigroup α] [CovariantClass α α (· * ·) (· ≤ ·)] {a b : α}
+@[to_additive] lemma of_mul_left [CommSemigroup α] [MulLeftMono α] {a b : α}
     (h : MulLECancellable (a * b)) : MulLECancellable a := (mul_comm a b ▸ h).of_mul_right
 
 end MulLECancellable
 
 @[to_additive (attr := simp)]
-lemma mulLECancellable_mul [LE α] [CommSemigroup α] [CovariantClass α α (· * ·) (· ≤ ·)] {a b : α} :
+lemma mulLECancellable_mul [LE α] [CommSemigroup α] [MulLeftMono α] {a b : α} :
     MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b :=
   ⟨fun h ↦ ⟨h.of_mul_left, h.of_mul_right⟩, fun h ↦ h.1.mul h.2⟩

Mathlib/Algebra/Order/Sub/Defs.lean

@@ -252,7 +252,7 @@ protected theorem tsub_eq_of_eq_add (hb : AddLECancellable b) (h : a = c + b) :
 
 /-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add` assuming that `a = c + b` itself is
 cancellable rather than `b`. -/
-protected lemma tsub_eq_of_eq_add' [CovariantClass α α (· + ·) (· ≤ ·)] (ha : AddLECancellable a)
+protected lemma tsub_eq_of_eq_add' [AddLeftMono α] (ha : AddLECancellable a)
     (h : a = c + b) : a - b = c := (h ▸ ha).of_add_right.tsub_eq_of_eq_add h
 
 /-- See `AddLECancellable.eq_tsub_of_add_eq'` for a version assuming that `b = a + c` itself is
@@ -262,7 +262,7 @@ protected theorem eq_tsub_of_add_eq (hc : AddLECancellable c) (h : a + c = b) :
 
 /-- Weaker version of `AddLECancellable.eq_tsub_of_add_eq` assuming that `b = a + c` itself is
 cancellable rather than `c`. -/
-protected lemma eq_tsub_of_add_eq' [CovariantClass α α (· + ·) (· ≤ ·)] (hb : AddLECancellable b)
+protected lemma eq_tsub_of_add_eq' [AddLeftMono α] (hb : AddLECancellable b)
     (h : a + c = b) : a = b - c := (hb.tsub_eq_of_eq_add' h.symm).symm
 
 /-- See `AddLECancellable.tsub_eq_of_eq_add_rev'` for a version assuming that `a = b + c` itself is
@@ -272,7 +272,7 @@ protected theorem tsub_eq_of_eq_add_rev (hb : AddLECancellable b) (h : a = b + c
 
 /-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add_rev` assuming that `a = b + c` itself is
 cancellable rather than `b`. -/
-protected lemma tsub_eq_of_eq_add_rev' [CovariantClass α α (· + ·) (· ≤ ·)]
+protected lemma tsub_eq_of_eq_add_rev' [AddLeftMono α]
     (ha : AddLECancellable a) (h : a = b + c) : a - b = c :=
   ha.tsub_eq_of_eq_add' <| by rw [add_comm, h]
 

Mathlib/Tactic/Ring/Compare.lean

@@ -66,7 +66,7 @@ abbrev lt_of_socs (α : Type*) [StrictOrderedCommSemiring α] : LT α := inferIn
 end Typeclass
 
 /-! The lemmas like `add_le_add_right` in the root namespace are stated under minimal type classes,
-typically just `[CovariantClass α α (swap (· + ·)) (· ≤ ·)]` or similar.  Here we restate these
+typically just `[AddRightMono α]` or similar.  Here we restate these
 lemmas under stronger type class assumptions (`[OrderedCommSemiring α]` or similar), which helps in
 speeding up the metaprograms in this file (`Mathlib.Tactic.Ring.proveLT` and
 `Mathlib.Tactic.Ring.proveLE`) substantially -- about a 50% reduction in heartbeat count in