feat(algebra/order/monoid): a + b ≤ c → a ≤ c (#15033)

Generalize four lemmas that were left by previous PRs before `canonically_ordered_monoid` was a thing.

src/algebra/order/monoid.lean

@@ -385,6 +385,9 @@ variables [canonically_ordered_monoid α] {a b c d : α}
 @[to_additive] lemma self_le_mul_right (a b : α) : a ≤ a * b := le_self_mul
 @[to_additive] lemma self_le_mul_left (a b : α) : a ≤ b * a := le_mul_self
 
+@[to_additive] lemma le_of_mul_le_left : a * b ≤ c → a ≤ c := le_self_mul.trans
+@[to_additive] lemma le_of_mul_le_right : a * b ≤ c → b ≤ c := le_mul_self.trans
+
 @[to_additive]
 lemma le_iff_exists_mul : a ≤ b ↔ ∃ c, b = a * c :=
 ⟨exists_mul_of_le, by { rintro ⟨c, rfl⟩, exact le_self_mul }⟩

src/data/matrix/rank.lean

@@ -44,7 +44,7 @@ by rw [rank, linear_equiv.map_zero, linear_map.range_zero, finrank_bot]
 
 lemma rank_le_card_width : A.rank ≤ fintype.card n :=
 begin
-  convert nat.le_of_add_le_left (A.to_lin'.finrank_range_add_finrank_ker).le,
+  convert le_of_add_le_left (A.to_lin'.finrank_range_add_finrank_ker).le,
   exact (module.free.finrank_pi K).symm,
 end
 

src/data/nat/basic.lean

@@ -468,13 +468,6 @@ begin
   exact add_lt_add_of_lt_of_le hab (nat.succ_le_iff.2 hcd)
 end
 
--- TODO: generalize to some ordered add_monoids, based on #6145
-lemma le_of_add_le_left {a b c : ℕ} (h : a + b ≤ c) : a ≤ c :=
-by { refine le_trans _ h, simp }
-
-lemma le_of_add_le_right {a b c : ℕ} (h : a + b ≤ c) : b ≤ c :=
-by { refine le_trans _ h, simp }
-
 /-! ### `pred` -/
 
 @[simp]

src/data/polynomial/coeff.lean

@@ -191,8 +191,7 @@ begin
   { rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right] },
   { refine (coeff_mul _ _ _).trans (finset.sum_eq_zero (λ x hx, _)),
     rw [coeff_X_pow, if_neg, mul_zero],
-    exact ne_of_lt (lt_of_le_of_lt (nat.le_of_add_le_right
-      (le_of_eq (finset.nat.mem_antidiagonal.mp hx))) (not_le.mp h)) },
+    exact ((le_of_add_le_right (finset.nat.mem_antidiagonal.mp hx).le).trans_lt $ not_le.mp h).ne }
 end
 
 lemma coeff_X_pow_mul' (p : R[X]) (n d : ℕ) :

src/data/polynomial/hasse_deriv.lean

@@ -159,7 +159,7 @@ begin
     { push_neg at hil, rw [← tsub_lt_iff_right hil] at hikl,
       rw [choose_eq_zero_of_lt hikl , zero_mul], }, },
   push_neg at hikl, apply @cast_injective ℚ,
-  have h1 : l ≤ i     := nat.le_of_add_le_right hikl,
+  have h1 : l ≤ i     := le_of_add_le_right hikl,
   have h2 : k ≤ i - l := le_tsub_of_add_le_right hikl,
   have h3 : k ≤ k + l := le_self_add,
   have H : ∀ (n : ℕ), (n! : ℚ) ≠ 0, { exact_mod_cast factorial_ne_zero },

src/data/real/nnreal.lean

@@ -364,13 +364,6 @@ begin
   exact h _ ((lt_add_iff_pos_right b).1 hxb)
 end
 
--- TODO: generalize to some ordered add_monoids, based on #6145
-lemma le_of_add_le_left {a b c : ℝ≥0} (h : a + b ≤ c) : a ≤ c :=
-by { refine le_trans _ h, exact (le_add_iff_nonneg_right _).mpr zero_le' }
-
-lemma le_of_add_le_right {a b c : ℝ≥0} (h : a + b ≤ c) : b ≤ c :=
-by { refine le_trans _ h, exact (le_add_iff_nonneg_left _).mpr zero_le' }
-
 lemma lt_iff_exists_rat_btwn (a b : ℝ≥0) :
   a < b ↔ (∃q:ℚ, 0 ≤ q ∧ a < real.to_nnreal q ∧ real.to_nnreal q < b) :=
 iff.intro

src/ring_theory/power_series/basic.lean

@@ -1160,8 +1160,7 @@ begin
   { rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right] },
   { refine (coeff_mul _ _ _).trans (finset.sum_eq_zero (λ x hx, _)),
     rw [coeff_X_pow, if_neg, mul_zero],
-    exact ne_of_lt (lt_of_le_of_lt (nat.le_of_add_le_right
-      (le_of_eq (finset.nat.mem_antidiagonal.mp hx))) (not_le.mp h)) },
+    exact ((le_of_add_le_right (finset.nat.mem_antidiagonal.mp hx).le).trans_lt $ not_le.mp h).ne }
 end
 
 lemma coeff_X_pow_mul' (p : power_series R) (n d : ℕ) :
@@ -1173,8 +1172,7 @@ begin
     rw [coeff_X_pow, if_neg, zero_mul],
     have := finset.nat.mem_antidiagonal.mp hx,
     rw add_comm at this,
-    exact ne_of_lt (lt_of_le_of_lt (nat.le_of_add_le_right
-      (le_of_eq this)) (not_le.mp h)) },
+    exact ((le_of_add_le_right this.le).trans_lt $ not_le.mp h).ne }
 end
 
 end