feat: use aliases for CovariantClass α α (· * ·) (· ≤ ·) etc

[FR-vdash-bot]

---

• depends on: [Merged by Bors] - chore(Algebra/Order/Module/Defs): remove unused assumptions #13465
• depends on: [Merged by Bors] - chore(Algebra/Order/Monoid/Defs): remove unused instances #13466
• depends on: [Merged by Bors] - feat: create aliases and lemmas for CovariantClass α α (· * ·) (· ≤ ·) etc #13467

[FR-vdash-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit d1510db.
There were significant changes against commit dd60782:

  Benchmark                Metric         Change
  ==============================================
+ ~Mathlib.Data.List.Sym   instructions   -23.4%

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Algebra/Order/Module/Defs): remove unused assumptions #13465
• [Merged by Bors] - chore(Algebra/Order/Monoid/Defs): remove unused instances #13466
• [Merged by Bors] - feat: create aliases and lemmas for CovariantClass α α (· * ·) (· ≤ ·) etc #13467
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary c969afd1af

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Int.instAddLeftMono
+ IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT
+ IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono
+ IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT
+ IsRightCancelMul.mulRightStrictMono_of_mulRightMono
+ Nat.instMulLeftMono
+ OrderedCancelCommMonoid.toMulLeftReflectLT
+ OrderedCancelCommMonoid.toMulRightReflectLT
+ OrderedCancelCommMonoid.to_mulLeftReflectLE
+ OrderedCommGroup.toMulLeftMono
+ OrderedCommGroup.toMulLeftReflectLE
+ OrderedCommGroup.toMulRightReflectLE
+ OrderedCommMonoid.toMulLeftMono
+ OrderedCommMonoid.toMulRightMono
+ addRightReflectLE
+ instMulLeftMono
+ instMulRightMono
+ instance (priority := 100) IdemSemiring.toMulLeftMono :
+ instance (priority := 100) IdemSemiring.toMulRightMono :
+ instance (priority := 100) toMulLeftMono : MulLeftMono α := by
+ instance (priority := 200) OrderedCancelCommMonoid.toMulLeftReflectLE :
+ instance : AddLeftMono (Multiset α)
+ instance : AddLeftMono ℚ
+ instance : AddLeftReflectLE (Multiset α)
+ instance [∀ i, OrderedAddCommMonoid (α i)] [∀ i, AddLeftReflectLE (α i)] :
+ instance {α : Type*} [Mul α] [Preorder α] [MulLeftMono α] :
+ instance {α : Type*} [Mul α] [Preorder α] [MulLeftStrictMono α] :
+ instance {α : Type*} [Mul α] [Preorder α] [MulRightMono α] :
+ instance {α : Type*} [Mul α] [Preorder α] [MulRightStrictMono α] :
+ mulLeftReflectLE
+ mulRightReflectLE
+ mulRightReflectLT
++ Lex.addLeftMono
++ Lex.addLeftStrictMono
++ Lex.addRightMono
++ Lex.addRightStrictMono
++ instAddLeftMono
++ mulLeftReflectLT
++ mulLeftStrictMono
++ mulRightStrictMono
+++ addRightStrictMono
++++ addRightReflectLT
+++++ addLeftReflectLE
+++++ mulRightMono
++++++ addLeftStrictMono
++++++ addRightMono
+++++++ addLeftReflectLT
++++++++ mulLeftMono
+++++++++++++++ addLeftMono
++-- add_martingale
++-- lt_of_tsub_lt_tsub_left_of_le
++-- neg
++-- sub_martingale
++-- tsub_lt_tsub_iff_left_of_le_of_le
+-++--++-- add
+-+- add_le_add_iff_left
+-+- add_le_add_iff_right
+-+- add_lt_add_iff_left
+-+- add_lt_add_iff_right
+-+- add_lt_add_left
+-+- add_lt_add_of_le_of_lt
+-+- add_lt_add_of_lt_of_le
+-+- add_lt_add_right
+-+- le_of_add_le_add_left
+-+- le_of_add_le_add_right
- Int.instCovariantClassAddLE
- IsLeftCancelMul.contravariant_mul_le_of_contravariant_mul_lt
- IsLeftCancelMul.covariant_mul_lt_of_covariant_mul_le
- IsRightCancelMul.contravariant_swap_mul_le_of_contravariant_swap_mul_lt
- IsRightCancelMul.covariant_swap_mul_lt_of_covariant_swap_mul_le
- Nat.instCovariantClassMulLE
- OrderedCancelCommMonoid.toContravariantClassLeft
- OrderedCancelCommMonoid.toContravariantClassRight
- OrderedCancelCommMonoid.to_contravariantClass
- OrderedCommGroup.to_contravariantClass_left_le
- OrderedCommGroup.to_contravariantClass_right_le
- OrderedCommGroup.to_covariantClass_left_le
- OrderedCommMonoid.toCovariantClassLeft
- OrderedCommMonoid.toCovariantClassRight
- add_contravariantClass_lt
- add_covariantClass
- add_swap_contravariantClass_lt
- add_swap_covariantClass
- add_swap_covariantClass_le
- contravariantClass
- contravariantClass_mul_le
- contravariantClass_swap_add_le
- contravariantClass_swap_mul_le
- contravariantClass_swap_mul_lt
- contravariant_add
- covariantClass_add
- covariantClass_mul_left
- covariantClass_mul_lt
- covariantClass_mul_right
- covariantClass_swap_mul_le
- covariantClass_swap_mul_lt
- covariant_mul_lt
- covariant_swap_mul_lt
- instCovariantClass_mul_le_left
- instCovariantClass_mul_le_right
- instance (priority := 100) IdemSemiring.toCovariantClass_mul_le :
- instance (priority := 100) IdemSemiring.toCovariantClass_swap_mul_le :
- instance (priority := 100) toCovariantClassMulLE : CovariantClass α α (· * ·) (· ≤ ·) := by
- instance (priority := 200) OrderedCancelCommMonoid.toContravariantClassLeLeft :
- instance : ContravariantClass (Multiset α) (Multiset α) (· + ·) (· ≤ ·)
- instance : CovariantClass (Multiset α) (Multiset α) (· + ·) (· ≤ ·)
- instance : CovariantClass ℚ ℚ (· + ·) (· ≤ ·)
- instance [∀ i, OrderedAddCommMonoid (α i)] [∀ i, ContravariantClass (α i) (α i) (· + ·) (· ≤ ·)] :
- instance {α : Type*} [Mul α] [Preorder α] [CovariantClass α α (swap (· * ·)) (· < ·)] :
- instance {α : Type*} [Mul α] [Preorder α] [CovariantClass α α (swap (· * ·)) (· ≤ ·)] :
- instance {α : Type*} [Mul α] [Preorder α] [CovariantClass α α (· * ·) (· < ·)] :
- instance {α : Type*} [Mul α] [Preorder α] [CovariantClass α α (· * ·) (· ≤ ·)] :
- mul_covariantClass_le
- mul_swap_covariantClass_le
-- Lex.covariantClass_le_left
-- Lex.covariantClass_le_right
-- Lex.covariantClass_lt_left
-- Lex.covariantClass_lt_right
-- add_contravariantClass_le
-- add_covariantClass_le
-- add_covariantClass_lt
-- contravariantClass_add_le
-- contravariantClass_mul_lt
-- covariant_add
-- covariant_swap_mul
-- instCovariantClassLE
--++ mul_le_mul'
--++ mul_le_mul_iff_left
--- contravariantClass_swap_add_lt
--- covariantClass_mul_le
--- covariantClass_swap_add_lt
--- covariant_mul
---- covariantClass_add_lt
---- covariantClass_swap_add_le
----- contravariantClass_add_lt
--------- covariantClass_add_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[FR-vdash-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit e017c9d.
There were no significant changes against commit ca2b360.