feat(algebra/order/ring): add some instances about covariance (#14763)

Most of the basic lemmas have been prepared. It is time to start trying to replace some of the lemmas in `algebra/order/ring`.

- [x] depends on: #14761

src/algebra/order/ring.lean

@@ -3,9 +3,10 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
+import algebra.char_zero.defs
 import algebra.order.group
+import algebra.order.monoid_lemmas_zero_lt
 import algebra.order.sub
-import algebra.char_zero.defs
 import algebra.hom.ring
 import data.set.intervals.basic
 
@@ -128,13 +129,27 @@ class ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_com
 (mul_lt_mul_of_pos_left  : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
 (mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
 
-@[priority 100] instance ordered_semiring.zero_le_one_class [h : ordered_semiring α] :
-  zero_le_one_class α :=
-{ ..h }
-
 section ordered_semiring
 variables [ordered_semiring α] {a b c d : α}
 
+lemma mul_lt_mul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
+ordered_semiring.mul_lt_mul_of_pos_left a b c h₁ h₂
+
+lemma mul_lt_mul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c :=
+ordered_semiring.mul_lt_mul_of_pos_right a b c h₁ h₂
+
+@[priority 100] -- see Note [lower instance priority]
+instance ordered_semiring.zero_le_one_class : zero_le_one_class α :=
+{ ..‹ordered_semiring α› }
+
+@[priority 200] -- see Note [lower instance priority]
+instance ordered_semiring.pos_mul_strict_mono : zero_lt.pos_mul_strict_mono α :=
+⟨λ x a b h, mul_lt_mul_of_pos_left h x.prop⟩
+
+@[priority 200] -- see Note [lower instance priority]
+instance ordered_semiring.mul_pos_strict_mono : zero_lt.mul_pos_strict_mono α :=
+⟨λ x a b h, mul_lt_mul_of_pos_right h x.prop⟩
+
 section nontrivial
 
 variables [nontrivial α]
@@ -169,12 +184,6 @@ alias zero_lt_four ← four_pos
 
 end nontrivial
 
-lemma mul_lt_mul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
-ordered_semiring.mul_lt_mul_of_pos_left a b c h₁ h₂
-
-lemma mul_lt_mul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c :=
-ordered_semiring.mul_lt_mul_of_pos_right a b c h₁ h₂
-
 lemma mul_lt_of_lt_one_left (hb : 0 < b) (ha : a < 1) : a * b < b :=
 (mul_lt_mul_of_pos_right ha hb).trans_le (one_mul _).le
 
@@ -1528,6 +1537,16 @@ begin
   apply self_le_add_right
 end
 
+@[priority 200] -- see Note [lower instance priority]
+instance canonically_ordered_comm_semiring.pos_mul_mono :
+  zero_lt.pos_mul_mono α :=
+⟨λ x a b h, by { obtain ⟨d, rfl⟩ := exists_add_of_le h, simp_rw [left_distrib, le_self_add], }⟩
+
+@[priority 200] -- see Note [lower instance priority]
+instance canonically_ordered_comm_semiring.mul_pos_mono :
+  zero_lt.mul_pos_mono α :=
+⟨λ x a b h, by { obtain ⟨d, rfl⟩ := exists_add_of_le h, simp_rw [right_distrib, le_self_add], }⟩
+
 /-- A version of `zero_lt_one : 0 < 1` for a `canonically_ordered_comm_semiring`. -/
 lemma zero_lt_one [nontrivial α] : (0:α) < 1 := (zero_le 1).lt_of_ne zero_ne_one
 
@@ -1825,4 +1844,20 @@ with_top.comm_monoid_with_zero
 instance [canonically_ordered_comm_semiring α] [nontrivial α] : comm_semiring (with_bot α) :=
 with_top.comm_semiring
 
+instance [canonically_ordered_comm_semiring α] [nontrivial α] :
+  zero_lt.pos_mul_mono (with_bot α) :=
+⟨ begin
+    rintros ⟨x, x0⟩ a b h, simp only [subtype.coe_mk],
+    induction x using with_bot.rec_bot_coe,
+    { have := bot_lt_coe (0 : α), rw [coe_zero] at this, exact absurd x0.le this.not_le, },
+    { induction a using with_bot.rec_bot_coe, { simp_rw [mul_bot x0.ne.symm, bot_le], },
+      induction b using with_bot.rec_bot_coe, { exact absurd h (bot_lt_coe a).not_le, },
+      { simp only [← coe_mul, coe_le_coe] at *,
+        exact zero_lt.mul_le_mul_left h (zero_le x), }, },
+  end ⟩
+
+instance [canonically_ordered_comm_semiring α] [nontrivial α] :
+  zero_lt.mul_pos_mono (with_bot α) :=
+zero_lt.pos_mul_mono_iff_mul_pos_mono.mp zero_lt.pos_mul_mono
+
 end with_bot

src/combinatorics/additive/behrend.lean

@@ -237,7 +237,7 @@ begin
   { rwa one_le_cast },
   rw le_sub_iff_add_le,
   norm_num,
-  exact le_mul_of_one_le_right zero_le_two (one_le_cast.2 hd),
+  exact one_le_cast.2 hd,
 end
 
 lemma bound_aux' (n d : ℕ) : (d ^ n / ↑(n * d^2) : ℝ) ≤ roth_number_nat ((2 * d - 1)^n) :=

src/data/nat/basic.lean

@@ -556,7 +556,7 @@ le_iff_le_iff_lt_iff_lt.1 mul_self_le_mul_self_iff
 
 theorem le_mul_self : Π (n : ℕ), n ≤ n * n
 | 0     := le_rfl
-| (n+1) := let t := nat.mul_le_mul_left (n+1) (succ_pos n) in by simp at t; exact t
+| (n+1) := by simp
 
 lemma le_mul_of_pos_left {m n : ℕ} (h : 0 < n) : m ≤ n * m :=
 begin