chore(algebra/order/ring/lemmas): use suffix ₚ, create aliases

src/algebra/group_power/order.lean

@@ -338,7 +338,7 @@ variables [strict_ordered_semiring R] {a x y : R} {n m : ℕ}
 lemma pow_lt_pow_of_lt_left (h : x < y) (hx : 0 ≤ x) : ∀ {n : ℕ}, 0 < n → x ^ n < y ^ n
 | 0 hn := hn.false.elim
 | (n + 1) _ := by simpa only [pow_succ'] using
-    mul_lt_mul_of_le_of_le' (pow_le_pow_of_le_left hx h.le _) h (pow_pos (hx.trans_lt h) _) hx
+    mul_lt_mul_of_le_of_ltₚ' (pow_le_pow_of_le_left hx h.le _) h hx (pow_pos (hx.trans_lt h) _)
 
 lemma strict_mono_on_pow (hn : 0 < n) : strict_mono_on (λ x : R, x ^ n) (set.Ici 0) :=
 λ x hx y hy h, pow_lt_pow_of_lt_left h hx hn

src/algebra/order/ring/defs.lean

@@ -438,12 +438,6 @@ instance strict_ordered_semiring.to_ordered_semiring : ordered_semiring α :=
   end,
   ..‹strict_ordered_semiring α› }
 
-lemma mul_lt_mul (hac : a < c) (hbd : b ≤ d) (hb : 0 < b) (hc : 0 ≤ c) : a * b < c * d :=
-(mul_lt_mul_of_pos_right hac hb).trans_le $ mul_le_mul_of_nonneg_left hbd hc
-
-lemma mul_lt_mul' (hac : a ≤ c) (hbd : b < d) (hb : 0 ≤ b) (hc : 0 < c) : a * b < c * d :=
-(mul_le_mul_of_nonneg_right hac hb).trans_lt $ mul_lt_mul_of_pos_left hbd hc
-
 @[simp] theorem pow_pos (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
 | 0     := by { nontriviality, rw pow_zero, exact zero_lt_one }
 | (n+1) := by { rw pow_succ, exact mul_pos H (pow_pos _) }
@@ -466,9 +460,6 @@ h4.lt_or_eq_dec.elim
   (λ b0, by rw [← b0, mul_zero]; exact
     mul_pos (h3.trans_lt h1) (h4.trans_lt h2))
 
-lemma mul_lt_mul'' : a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d :=
-by classical; exact decidable.mul_lt_mul''
-
 lemma lt_mul_left (hn : 0 < a) (hm : 1 < b) : a < b * a :=
 by { convert mul_lt_mul_of_pos_right hm hn, rw one_mul }
 
@@ -673,12 +664,6 @@ le_of_not_gt $ λ ha, (mul_neg_of_neg_of_pos ha hb).not_le h
 lemma nonneg_of_mul_nonneg_right (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b :=
 le_of_not_gt $ λ hb, (mul_neg_of_pos_of_neg ha hb).not_le h
 
-lemma neg_of_mul_neg_left (h : a * b < 0) (hb : 0 ≤ b) : a < 0 :=
-lt_of_not_ge $ λ ha, (mul_nonneg ha hb).not_lt h
-
-lemma neg_of_mul_neg_right (h : a * b < 0) (ha : 0 ≤ a) : b < 0 :=
-lt_of_not_ge $ λ hb, (mul_nonneg ha hb).not_lt h
-
 lemma nonpos_of_mul_nonpos_left (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0 :=
 le_of_not_gt (assume ha : a > 0, (mul_pos ha hb).not_le h)
 

src/algebra/order/ring/lemmas.lean

@@ -168,45 +168,82 @@ alias le_of_mul_le_mul_right ← le_of_mul_le_mul_of_pos_right
   b * a ≤ c * a ↔ b ≤ c :=
 @rel_iff_cov α>0 α (λ x y, y * x) (≤) _ _ ⟨a, a0⟩ _ _
 
-lemma mul_lt_mul_of_pos_of_nonneg [pos_mul_strict_mono α] [mul_pos_mono α]
+lemma mul_le_mul_of_le_of_leₚ [pos_mul_mono α] [mul_pos_mono α]
+  (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 ≤ d) : a * c ≤ b * d :=
+(mul_le_mul_of_nonneg_left h₂ a0).trans (mul_le_mul_of_nonneg_right h₁ d0)
+
+lemma mul_le_mul_of_le_of_leₚ' [pos_mul_mono α] [mul_pos_mono α]
+  (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) : a * c ≤ b * d :=
+(mul_le_mul_of_nonneg_right h₁ c0).trans (mul_le_mul_of_nonneg_left h₂ b0)
+
+lemma mul_lt_mul_of_le_of_ltₚ [pos_mul_strict_mono α] [mul_pos_mono α]
   (h₁ : a ≤ b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 ≤ d) : a * c < b * d :=
 (mul_lt_mul_of_pos_left h₂ a0).trans_le (mul_le_mul_of_nonneg_right h₁ d0)
 
-lemma mul_lt_mul_of_le_of_le' [pos_mul_strict_mono α] [mul_pos_mono α]
-  (h₁ : a ≤ b) (h₂ : c < d) (b0 : 0 < b) (c0 : 0 ≤ c) : a * c < b * d :=
+lemma mul_lt_mul_of_le_of_ltₚ' [pos_mul_strict_mono α] [mul_pos_mono α]
+  (h₁ : a ≤ b) (h₂ : c < d) (c0 : 0 ≤ c) (b0 : 0 < b) : a * c < b * d :=
 (mul_le_mul_of_nonneg_right h₁ c0).trans_lt (mul_lt_mul_of_pos_left h₂ b0)
 
-lemma mul_lt_mul_of_nonneg_of_pos [pos_mul_mono α] [mul_pos_strict_mono α]
+lemma mul_lt_mul_of_lt_of_leₚ [pos_mul_mono α] [mul_pos_strict_mono α]
   (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d :=
 (mul_le_mul_of_nonneg_left h₂ a0).trans_lt (mul_lt_mul_of_pos_right h₁ d0)
 
-lemma mul_lt_mul_of_le_of_lt' [pos_mul_mono α] [mul_pos_strict_mono α]
-  (h₁ : a < b) (h₂ : c ≤ d) (b0 : 0 ≤ b) (c0 : 0 < c) : a * c < b * d :=
+lemma mul_lt_mul_of_lt_of_leₚ' [pos_mul_mono α] [mul_pos_strict_mono α]
+  (h₁ : a < b) (h₂ : c ≤ d) (c0 : 0 < c) (b0 : 0 ≤ b) : a * c < b * d :=
 (mul_lt_mul_of_pos_right h₁ c0).trans_le (mul_le_mul_of_nonneg_left h₂ b0)
 
-lemma mul_lt_mul_of_pos_of_pos [pos_mul_strict_mono α] [mul_pos_strict_mono α]
+lemma mul_lt_mul_of_lt_of_ltₚ [pos_mul_strict_mono α] [mul_pos_strict_mono α]
   (h₁ : a < b) (h₂ : c < d) (a0 : 0 < a) (d0 : 0 < d) : a * c < b * d :=
 (mul_lt_mul_of_pos_left h₂ a0).trans (mul_lt_mul_of_pos_right h₁ d0)
 
-lemma mul_lt_mul_of_lt_of_lt' [pos_mul_strict_mono α] [mul_pos_strict_mono α]
-  (h₁ : a < b) (h₂ : c < d) (b0 : 0 < b) (c0 : 0 < c) : a * c < b * d :=
+lemma mul_lt_mul_of_lt_of_ltₚ' [pos_mul_strict_mono α] [mul_pos_strict_mono α]
+  (h₁ : a < b) (h₂ : c < d) (c0 : 0 < c) (b0 : 0 < b) : a * c < b * d :=
 (mul_lt_mul_of_pos_right h₁ c0).trans (mul_lt_mul_of_pos_left h₂ b0)
 
-lemma mul_lt_of_mul_lt_of_nonneg_left [pos_mul_mono α] (h : a * b < c) (hdb : d ≤ b) (ha : 0 ≤ a) :
-  a * d < c :=
-(mul_le_mul_of_nonneg_left hdb ha).trans_lt h
+alias mul_le_mul_of_le_of_leₚ' ← mul_le_mul -- this name was in `algebra.order.ring`
+alias mul_lt_mul_of_lt_of_leₚ' ← mul_lt_mul -- this name was in `algebra.order.ring`
+alias mul_lt_mul_of_le_of_ltₚ' ← mul_lt_mul' -- this name was in `algebra.order.ring`
+
+lemma mul_le_of_mul_le_leftₚ [pos_mul_mono α]
+  (h : a * b ≤ c) (hle : d ≤ b) (a0 : 0 ≤ a) : a * d ≤ c :=
+(mul_le_mul_of_nonneg_left hle a0).trans h
+
+lemma mul_lt_of_mul_lt_leftₚ [pos_mul_mono α]
+  (h : a * b < c) (hle : d ≤ b) (a0 : 0 ≤ a) : a * d < c :=
+(mul_le_mul_of_nonneg_left hle a0).trans_lt h
 
-lemma lt_mul_of_lt_mul_of_nonneg_left [pos_mul_mono α] (h : a < b * c) (hcd : c ≤ d) (hb : 0 ≤ b) :
-  a < b * d :=
-h.trans_le $ mul_le_mul_of_nonneg_left hcd hb
+lemma le_mul_of_le_mul_leftₚ [pos_mul_mono α]
+  (h : a ≤ b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a ≤ b * d :=
+h.trans (mul_le_mul_of_nonneg_left hle b0)
 
-lemma mul_lt_of_mul_lt_of_nonneg_right [mul_pos_mono α] (h : a * b < c) (hda : d ≤ a) (hb : 0 ≤ b) :
-  d * b < c :=
-(mul_le_mul_of_nonneg_right hda hb).trans_lt h
+lemma lt_mul_of_lt_mul_leftₚ [pos_mul_mono α]
+  (h : a < b * c) (hle : c ≤ d) (b0 : 0 ≤ b) : a < b * d :=
+h.trans_le (mul_le_mul_of_nonneg_left hle b0)
+
+lemma mul_le_of_mul_le_rightₚ [mul_pos_mono α]
+  (h : a * b ≤ c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b ≤ c :=
+(mul_le_mul_of_nonneg_right hle b0).trans h
 
-lemma lt_mul_of_lt_mul_of_nonneg_right [mul_pos_mono α] (h : a < b * c) (hbd : b ≤ d) (hc : 0 ≤ c) :
-  a < d * c :=
-h.trans_le $ mul_le_mul_of_nonneg_right hbd hc
+lemma mul_lt_of_mul_lt_rightₚ [mul_pos_mono α]
+  (h : a * b < c) (hle : d ≤ a) (b0 : 0 ≤ b) : d * b < c :=
+(mul_le_mul_of_nonneg_right hle b0).trans_lt h
+
+lemma le_mul_of_le_mul_rightₚ [mul_pos_mono α]
+  (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a ≤ d * c :=
+h.trans (mul_le_mul_of_nonneg_right hle c0)
+
+lemma lt_mul_of_lt_mul_rightₚ [mul_pos_mono α]
+  (h : a < b * c) (hle : b ≤ d) (c0 : 0 ≤ c) : a < d * c :=
+h.trans_le (mul_le_mul_of_nonneg_right hle c0)
+
+alias mul_le_of_mul_le_leftₚ ← mul_le_of_mul_le_of_nonneg_left
+alias mul_lt_of_mul_lt_leftₚ ← mul_lt_of_mul_lt_of_nonneg_left
+alias le_mul_of_le_mul_leftₚ ← le_mul_of_le_mul_of_nonneg_left
+alias lt_mul_of_lt_mul_leftₚ ← lt_mul_of_lt_mul_of_nonneg_left
+alias mul_le_of_mul_le_rightₚ ← mul_le_of_mul_le_of_nonneg_right
+alias mul_lt_of_mul_lt_rightₚ ← mul_lt_of_mul_lt_of_nonneg_right
+alias le_mul_of_le_mul_rightₚ ← le_mul_of_le_mul_of_nonneg_right
+alias lt_mul_of_lt_mul_rightₚ ← lt_mul_of_lt_mul_of_nonneg_right
 
 end preorder
 
@@ -311,34 +348,23 @@ lemma pos_iff_pos_of_mul_pos [pos_mul_reflect_lt α] [mul_pos_reflect_lt α] (ha
   0 < a ↔ 0 < b :=
 ⟨pos_of_mul_pos_right hab ∘ le_of_lt, pos_of_mul_pos_left hab ∘ le_of_lt⟩
 
-lemma mul_le_mul_of_le_of_le [pos_mul_mono α] [mul_pos_mono α]
-  (h₁ : a ≤ b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 ≤ d) : a * c ≤ b * d :=
-(mul_le_mul_of_nonneg_left h₂ a0).trans $ mul_le_mul_of_nonneg_right h₁ d0
+/-- Assumes left strict covariance. -/
+lemma left.mul_lt_mulₚ [pos_mul_strict_mono α] [mul_pos_mono α]
+  (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d :=
+mul_lt_mul_of_le_of_ltₚ' h₁.le h₂ c0 (a0.trans_lt h₁)
 
-lemma mul_le_mul [pos_mul_mono α] [mul_pos_mono α]
-  (h₁ : a ≤ b) (h₂ : c ≤ d) (c0 : 0 ≤ c) (b0 : 0 ≤ b) : a * c ≤ b * d :=
-(mul_le_mul_of_nonneg_right h₁ c0).trans $ mul_le_mul_of_nonneg_left h₂ b0
+/-- Assumes right strict covariance. -/
+lemma right.mul_lt_mulₚ [pos_mul_mono α] [mul_pos_strict_mono α]
+  (h₁ : a < b) (h₂ : c < d) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * c < b * d :=
+mul_lt_mul_of_lt_of_leₚ h₁ h₂.le a0 (c0.trans_lt h₂)
+
+alias left.mul_lt_mulₚ ← mul_lt_mulₚ
+alias left.mul_lt_mulₚ ← mul_lt_mul'' -- this name was in `algebra.order.ring`
 
 lemma mul_self_le_mul_self [pos_mul_mono α] [mul_pos_mono α] (ha : 0 ≤ a) (hab : a ≤ b) :
   a * a ≤ b * b :=
 mul_le_mul hab hab ha $ ha.trans hab
 
-lemma mul_le_of_mul_le_of_nonneg_left [pos_mul_mono α] (h : a * b ≤ c) (hle : d ≤ b) (a0 : 0 ≤ a) :
-  a * d ≤ c :=
-(mul_le_mul_of_nonneg_left hle a0).trans h
-
-lemma le_mul_of_le_mul_of_nonneg_left [pos_mul_mono α] (h : a ≤ b * c) (hle : c ≤ d) (b0 : 0 ≤ b) :
-  a ≤ b * d :=
-h.trans (mul_le_mul_of_nonneg_left hle b0)
-
-lemma mul_le_of_mul_le_of_nonneg_right [mul_pos_mono α] (h : a * b ≤ c) (hle : d ≤ a) (b0 : 0 ≤ b) :
-  d * b ≤ c :=
-(mul_le_mul_of_nonneg_right hle b0).trans h
-
-lemma le_mul_of_le_mul_of_nonneg_right [mul_pos_mono α] (h : a ≤ b * c) (hle : b ≤ d) (c0 : 0 ≤ c) :
-  a ≤ d * c :=
-h.trans (mul_le_mul_of_nonneg_right hle c0)
-
 end preorder
 
 section partial_order
@@ -410,7 +436,7 @@ begin
   { exact ⟨rfl, (mul_left_cancel_iff_of_pos a0).mp h⟩ },
   rcases eq_or_lt_of_le hbd with rfl | hbd,
   { exact ⟨(mul_right_cancel_iff_of_pos d0).mp h, rfl⟩ },
-  exact ((mul_lt_mul_of_pos_of_pos hac hbd a0 d0).ne h).elim,
+  exact ((mul_lt_mul_of_lt_of_ltₚ hac hbd a0 d0).ne h).elim,
 end
 
 lemma mul_eq_mul_iff_eq_and_eq_of_pos' [pos_mul_strict_mono α] [mul_pos_strict_mono α]
@@ -423,7 +449,7 @@ begin
   { exact ⟨rfl, (mul_left_cancel_iff_of_pos b0).mp h⟩ },
   rcases eq_or_lt_of_le hbd with rfl | hbd,
   { exact ⟨(mul_right_cancel_iff_of_pos c0).mp h, rfl⟩ },
-  exact ((mul_lt_mul_of_lt_of_lt' hac hbd b0 c0).ne h).elim,
+  exact ((mul_lt_mul_of_lt_of_ltₚ' hac hbd c0 b0).ne h).elim,
 end
 
 end partial_order
@@ -458,23 +484,29 @@ lemma neg_iff_neg_of_mul_pos [pos_mul_mono α] [mul_pos_mono α]
   a < 0 ↔ b < 0 :=
 ⟨neg_of_mul_pos_right hab ∘ le_of_lt, neg_of_mul_pos_left hab ∘ le_of_lt⟩
 
-lemma left.neg_of_mul_neg_left [pos_mul_mono α]
-  (h : a * b < 0) (h1 : 0 ≤ a) :
+lemma left.neg_of_mul_neg_right [pos_mul_mono α]
+  (h : a * b < 0) (a0 : 0 ≤ a) :
   b < 0 :=
-lt_of_not_ge (assume h2 : b ≥ 0, (left.mul_nonneg h1 h2).not_lt h)
+lt_of_not_ge (λ b0 : b ≥ 0, (left.mul_nonneg a0 b0).not_lt h)
 
-lemma right.neg_of_mul_neg_left [mul_pos_mono α]
-  (h : a * b < 0) (h1 : 0 ≤ a) :
+alias left.neg_of_mul_neg_right ← neg_of_mul_neg_right
+
+lemma right.neg_of_mul_neg_right [mul_pos_mono α]
+  (h : a * b < 0) (a0 : 0 ≤ a) :
   b < 0 :=
-lt_of_not_ge (assume h2 : b ≥ 0, (right.mul_nonneg h1 h2).not_lt h)
+lt_of_not_ge (λ b0 : b ≥ 0, (right.mul_nonneg a0 b0).not_lt h)
 
-lemma left.neg_of_mul_neg_right [pos_mul_mono α]
-  (h : a * b < 0) (h1 : 0 ≤ b) : a < 0 :=
-lt_of_not_ge (assume h2 : a ≥ 0, (left.mul_nonneg h2 h1).not_lt h)
+lemma left.neg_of_mul_neg_left [pos_mul_mono α]
+  (h : a * b < 0) (b0 : 0 ≤ b) :
+  a < 0 :=
+lt_of_not_ge (λ a0 : a ≥ 0, (left.mul_nonneg a0 b0).not_lt h)
 
-lemma right.neg_of_mul_neg_right [mul_pos_mono α]
-  (h : a * b < 0) (h1 : 0 ≤ b) : a < 0 :=
-lt_of_not_ge (assume h2 : a ≥ 0, (right.mul_nonneg h2 h1).not_lt h)
+alias left.neg_of_mul_neg_left ← neg_of_mul_neg_left
+
+lemma right.neg_of_mul_neg_left [mul_pos_mono α]
+  (h : a * b < 0) (b0 : 0 ≤ b) :
+  a < 0 :=
+lt_of_not_ge (λ a0 : a ≥ 0, (right.mul_nonneg a0 b0).not_lt h)
 
 end linear_order
 

src/number_theory/class_number/finite.lean

@@ -114,7 +114,7 @@ begin
   have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i),
   apply (int.cast_le.mpr (norm_le abv bS a hy')).trans_lt,
   simp only [int.cast_mul, int.cast_pow],
-  apply mul_lt_mul' le_rfl,
+  refine mul_lt_mul' le_rfl _ _ _,
   { exact pow_lt_pow_of_lt_left this
       (int.cast_nonneg.mpr y'_nonneg)
       (fintype.card_pos_iff.mpr ⟨i⟩) },