name covariant_class -> covariantClass + attribute

Mathlib/Algebra/Order/Group.lean

@@ -36,12 +36,12 @@ class OrderedCommGroup (α : Type u) extends CommGroup α, PartialOrder α where
 attribute [to_additive OrderedAddCommGroup] OrderedCommGroup
 
 @[to_additive]
-instance OrderedCommGroup.to_covariant_class_left_le [OrderedCommGroup α] :
+instance OrderedCommGroup.to_covariantClass_left_le [OrderedCommGroup α] :
     CovariantClass α α (· * ·) (· ≤ ·) where
   elim := fun a b c bc => OrderedCommGroup.mul_le_mul_left b c bc a
 
 -- TODO `to_additive` should copy this
-attribute [instance] OrderedAddCommGroup.to_covariant_class_left_le
+attribute [instance] OrderedAddCommGroup.to_covariantClass_left_le
 
 -- see Note [lower instance priority]
 @[to_additive OrderedAddCommGroup.toOrderedCancelAddCommMonoid]

Mathlib/Algebra/Order/Monoid.lean

@@ -38,46 +38,49 @@ attribute [to_additive OrderedAddCommMonoid] OrderedCommMonoid
 section OrderedInstances
 open Function
 
-@[to_additive OrderedAddCommMonoid.to_covariant_class_left]
-instance OrderedCommMonoid.to_covariant_class_left (M : Type _) [OrderedCommMonoid M] :
+@[to_additive OrderedAddCommMonoid.to_covariantClass_left]
+instance OrderedCommMonoid.to_covariantClass_left (M : Type _) [OrderedCommMonoid M] :
     CovariantClass M M (· * ·) (· ≤ ·) where
   elim := fun a _ _ bc => OrderedCommMonoid.mul_le_mul_left _ _ bc a
 
 -- TODO `to_additive` should copy this
-attribute [instance] OrderedAddCommMonoid.to_covariant_class_left
+attribute [instance] OrderedAddCommMonoid.to_covariantClass_left
 
 /- This instance can be proven with `by apply_instance`.  However, `with_bot ℕ` does not
-pick up a `covariant_class M M (function.swap (*)) (≤)` instance without it (see PR #7940). -/
-@[to_additive OrderedAddCommMonoid.to_covariant_class_right]
-instance OrderedCommMonoid.to_covariant_class_right (M : Type _) [OrderedCommMonoid M] :
+pick up a `covariantClass M M (function.swap (*)) (≤)` instance without it (see PR #7940). -/
+@[to_additive OrderedAddCommMonoid.to_covariantClass_right]
+instance OrderedCommMonoid.to_covariantClass_right (M : Type _) [OrderedCommMonoid M] :
     CovariantClass M M (swap (· * ·)) (· ≤ ·) :=
   covariant_swap_mul_le_of_covariant_mul_le M
 
 -- TODO `to_additive` should copy this
-attribute [instance] OrderedAddCommMonoid.to_covariant_class_right
+attribute [instance] OrderedAddCommMonoid.to_covariantClass_right
 
 /- This is not an instance, to avoid creating a loop in the type-class system: in a
-`left_cancel_semigroup` with a `partial_order`, assuming `covariant_class M M (*) (≤)` implies
-`covariant_class M M (*) (<)`, see `left_cancel_semigroup.covariant_mul_lt_of_covariant_mul_le`. -/
-@[to_additive Add.to_covariant_class_left]
-theorem Mul.to_covariant_class_left (M : Type _) [Mul M] [PartialOrder M]
+`left_cancel_semigroup` with a `partial_order`, assuming `covariantClass M M (*) (≤)` implies
+`covariantClass M M (*) (<)`, see `left_cancel_semigroup.covariant_mul_lt_of_covariant_mul_le`. -/
+@[to_additive Add.to_covariantClass_left]
+theorem Mul.to_covariantClass_left (M : Type _) [Mul M] [PartialOrder M]
     [CovariantClass M M (· * ·) (· < ·)] : CovariantClass M M (· * ·) (· ≤ ·) :=
   ⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩
+#align Mul.to_covariant_class_left Mul.to_covariantClass_left
+
 
 -- TODO `to_additive` should copy this
-attribute [instance] Add.to_covariant_class_left
+attribute [instance] Add.to_covariantClass_left
 
 /- This is not an instance, to avoid creating a loop in the type-class system: in a
-`right_cancel_semigroup` with a `partial_order`, assuming `covariant_class M M (swap (*)) (<)`
-implies `covariant_class M M (swap (*)) (≤)`, see
+`right_cancel_semigroup` with a `partial_order`, assuming `covariantClass M M (swap (*)) (<)`
+implies `covariantClass M M (swap (*)) (≤)`, see
 `right_cancel_semigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le`. -/
-@[to_additive Add.to_covariant_class_right]
-theorem Mul.to_covariant_class_right (M : Type _) [Mul M] [PartialOrder M]
+@[to_additive Add.to_covariantClass_right]
+theorem Mul.to_covariantClass_right (M : Type _) [Mul M] [PartialOrder M]
     [CovariantClass M M (swap (· * ·)) (· < ·)] : CovariantClass M M (swap (· * ·)) (· ≤ ·) :=
   ⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩
+#align Mul.to_covariant_class_right Mul.to_covariantClass_right
 
 -- TODO `to_additive` should copy this
-attribute [instance] Add.to_covariant_class_right
+attribute [instance] Add.to_covariantClass_right
 
 end OrderedInstances