chore(algebra/order/group/basic): Improve lemma names (#16970)

YaelDillies · YaelDillies · commit 402f8982dddc · 2022-11-03T08:03:12.000Z
Rename
* `div_le''` → `div_le_comm`
* `le_div''` → `le_div_comm`
* `sub_le` → `sub_le_comm`
* `le_sub` → `le_sub_comm`
* `div_lt''` → `div_lt_comm`
* `lt_div''` → `lt_div_comm`
* `sub_lt` → `sub_lt_comm`
* `lt_sub` → `lt_sub_comm`
diff --git a/src/algebra/order/archimedean.lean b/src/algebra/order/archimedean.lean
@@ -262,7 +262,7 @@ by simpa only [rat.cast_pos] using exists_rat_btwn x0
 
 lemma exists_rat_near (x : α) (ε0 : 0 < ε) : ∃ q : ℚ, |x - q| < ε :=
 let ⟨q, h₁, h₂⟩ := exists_rat_btwn $ ((sub_lt_self_iff x).2 ε0).trans ((lt_add_iff_pos_left x).2 ε0)
-  in ⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
+  in ⟨q, abs_sub_lt_iff.2 ⟨sub_lt_comm.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
 
 end linear_ordered_field
 
diff --git a/src/algebra/order/complete_field.lean b/src/algebra/order/complete_field.lean
@@ -135,7 +135,7 @@ begin
   { rw [mem_set_of_eq, ←sub_lt_iff_lt_add] at hq,
     obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq,
     refine ⟨q₁, q - q₁, _, _, add_sub_cancel'_right _ _⟩; try {norm_cast}; rwa coe_mem_cut_map_iff,
-    exact_mod_cast sub_lt.mp hq₁q },
+    exact_mod_cast sub_lt_comm.mp hq₁q },
   { rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩,
     refine ⟨qa + qb, _, by norm_cast⟩,
     rw [mem_set_of_eq, cast_add],
diff --git a/src/algebra/order/floor.lean b/src/algebra/order/floor.lean
@@ -555,7 +555,7 @@ by rw [add_comm, fract_add_nat]
 
 @[simp] lemma fract_nonneg (a : α) : 0 ≤ fract a := sub_nonneg.2 $ floor_le _
 
-lemma fract_lt_one (a : α) : fract a < 1 := sub_lt.1 $ sub_one_lt_floor _
+lemma fract_lt_one (a : α) : fract a < 1 := sub_lt_comm.1 $ sub_one_lt_floor _
 
 @[simp] lemma fract_zero : fract (0 : α) = 0 := by rw [fract, floor_zero, cast_zero, sub_self]
 
@@ -878,7 +878,8 @@ begin
     simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx, },
   { rw abs_eq_neg_self.mpr (sub_neg.mpr hx).le,
     conv_rhs { rw ← fract_add_floor x, },
-    rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel, le_sub],
+    rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
+      le_sub_comm],
     norm_cast,
     exact floor_le_sub_one_iff.mpr hx, },
 end
diff --git a/src/algebra/order/group/basic.lean b/src/algebra/order/group/basic.lean
@@ -632,13 +632,11 @@ le_div_iff_mul_le.trans inv_mul_le_iff_le_mul'
 lemma inv_le_div_iff_le_mul' : a⁻¹ ≤ b / c ↔ c ≤ a * b :=
 by rw [inv_le_div_iff_le_mul, mul_comm]
 
-@[to_additive sub_le]
-lemma div_le'' : a / b ≤ c ↔ a / c ≤ b :=
-div_le_iff_le_mul'.trans div_le_iff_le_mul.symm
+@[to_additive]
+lemma div_le_comm : a / b ≤ c ↔ a / c ≤ b := div_le_iff_le_mul'.trans div_le_iff_le_mul.symm
 
-@[to_additive le_sub]
-lemma le_div'' : a ≤ b / c ↔ c ≤ b / a :=
-le_div_iff_mul_le'.trans le_div_iff_mul_le.symm
+@[to_additive]
+lemma le_div_comm : a ≤ b / c ↔ c ≤ b / a := le_div_iff_mul_le'.trans le_div_iff_mul_le.symm
 
 end has_le
 
@@ -747,13 +745,11 @@ alias sub_lt_iff_lt_add' ↔ lt_add_of_sub_left_lt sub_left_lt_of_lt_add
 lemma inv_lt_div_iff_lt_mul' : b⁻¹ < a / c ↔ c < a * b :=
 lt_div_iff_mul_lt.trans inv_mul_lt_iff_lt_mul'
 
-@[to_additive sub_lt]
-lemma div_lt'' : a / b < c ↔ a / c < b :=
-div_lt_iff_lt_mul'.trans div_lt_iff_lt_mul.symm
+@[to_additive]
+lemma div_lt_comm : a / b < c ↔ a / c < b := div_lt_iff_lt_mul'.trans div_lt_iff_lt_mul.symm
 
-@[to_additive lt_sub]
-lemma lt_div'' : a < b / c ↔ c < b / a :=
-lt_div_iff_mul_lt'.trans lt_div_iff_mul_lt.symm
+@[to_additive]
+lemma lt_div_comm : a < b / c ↔ c < b / a := lt_div_iff_mul_lt'.trans lt_div_iff_mul_lt.symm
 
 end has_lt
 
@@ -1161,13 +1157,13 @@ lemma abs_sub_lt_iff : |a - b| < c ↔ a - b < c ∧ b - a < c :=
 by rw [abs_lt, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']
 
 lemma sub_le_of_abs_sub_le_left (h : |a - b| ≤ c) : b - c ≤ a :=
-sub_le.1 $ (abs_sub_le_iff.1 h).2
+sub_le_comm.1 $ (abs_sub_le_iff.1 h).2
 
 lemma sub_le_of_abs_sub_le_right (h : |a - b| ≤ c) : a - c ≤ b :=
 sub_le_of_abs_sub_le_left (abs_sub_comm a b ▸ h)
 
 lemma sub_lt_of_abs_sub_lt_left (h : |a - b| < c) : b - c < a :=
-sub_lt.1 $ (abs_sub_lt_iff.1 h).2
+sub_lt_comm.1 $ (abs_sub_lt_iff.1 h).2
 
 lemma sub_lt_of_abs_sub_lt_right (h : |a - b| < c) : a - c < b :=
 sub_lt_of_abs_sub_lt_left (abs_sub_comm a b ▸ h)
diff --git a/src/analysis/complex/roots_of_unity.lean b/src/analysis/complex/roots_of_unity.lean
@@ -166,7 +166,7 @@ begin
     exact mul_nonpos_of_nonpos_of_nonneg (sub_nonpos.mpr $ by exact_mod_cast h.le)
       (div_nonneg (by simp [real.pi_pos.le]) $ by simp) },
   rw [←mul_rotate', mul_div_assoc, neg_lt, ←mul_neg, mul_lt_iff_lt_one_right real.pi_pos,
-      ←neg_div, ←neg_mul, neg_sub, div_lt_iff, one_mul, sub_mul, sub_lt, ←mul_sub_one],
+      ←neg_div, ←neg_mul, neg_sub, div_lt_iff, one_mul, sub_mul, sub_lt_comm, ←mul_sub_one],
   norm_num,
   exact_mod_cast not_le.mp h₂,
   { exact (nat.cast_pos.mpr hn.bot_lt) }
diff --git a/src/analysis/complex/upper_half_plane/metric.lean b/src/analysis/complex/upper_half_plane/metric.lean
@@ -288,7 +288,7 @@ lemma im_pos_of_dist_center_le {z : ℍ} {r : ℝ} {w : ℂ} (h : dist w (center
 calc 0 < z.im * (cosh r - sinh r) : mul_pos z.im_pos (sub_pos.2 $ sinh_lt_cosh _)
 ... = (z.center r).im - z.im * sinh r : mul_sub _ _ _
 ... ≤ (z.center r).im - dist (z.center r : ℂ) w : sub_le_sub_left (by rwa [dist_comm]) _
-... ≤ w.im : sub_le.1 $ (le_abs_self _).trans (abs_im_le_abs $ z.center r - w)
+... ≤ w.im : sub_le_comm.1 $ (le_abs_self _).trans (abs_im_le_abs $ z.center r - w)
 
 lemma image_coe_closed_ball (z : ℍ) (r : ℝ) :
   (coe : ℍ → ℂ) '' closed_ball z r = closed_ball (z.center r) (z.im * sinh r) :=
diff --git a/src/analysis/convex/uniform.lean b/src/analysis/convex/uniform.lean
@@ -71,7 +71,7 @@ begin
   { rintro z hz hδz,
     nth_rewrite 2 ←one_smul ℝ z,
     rwa [←sub_smul, norm_smul_of_nonneg (sub_nonneg_of_le $ one_le_inv (hδ'.trans_le hδz) hz),
-      sub_mul, inv_mul_cancel (hδ'.trans_le hδz).ne', one_mul, sub_le] },
+      sub_mul, inv_mul_cancel (hδ'.trans_le hδz).ne', one_mul, sub_le_comm] },
   set x' := ∥x∥⁻¹ • x,
   set y' := ∥y∥⁻¹ • y,
   have hxy' : ε/3 ≤ ∥x' - y'∥ :=
diff --git a/src/analysis/special_functions/gamma.lean b/src/analysis/special_functions/gamma.lean
@@ -510,7 +510,7 @@ begin
   { rw mem_nhds_iff, use S,
     refine ⟨subset.rfl, _, hn⟩,
     have : S = re⁻¹' Ioi (1 - n : ℝ),
-    { ext, rw [preimage,Ioi, mem_set_of_eq, mem_set_of_eq, mem_set_of_eq], exact sub_lt },
+    { ext, rw [preimage,Ioi, mem_set_of_eq, mem_set_of_eq, mem_set_of_eq], exact sub_lt_comm },
     rw this,
     refine continuous.is_open_preimage continuous_re _ is_open_Ioi, },
   apply eventually_eq_of_mem this,
diff --git a/src/analysis/special_functions/stirling.lean b/src/analysis/special_functions/stirling.lean
@@ -163,7 +163,7 @@ end
 lemma log_stirling_seq_bounded_by_constant : ∃ c, ∀ (n : ℕ), c ≤ log (stirling_seq n.succ) :=
 begin
   obtain ⟨d, h⟩ := log_stirling_seq_bounded_aux,
-  exact ⟨log (stirling_seq 1) - d, λ n, sub_le.mp (h n)⟩,
+  exact ⟨log (stirling_seq 1) - d, λ n, sub_le_comm.mp (h n)⟩,
 end
 
 /-- The sequence `stirling_seq` is positive for `n > 0`  -/
diff --git a/src/combinatorics/additive/behrend.lean b/src/combinatorics/additive/behrend.lean
@@ -269,7 +269,7 @@ end
 
 lemma two_div_one_sub_two_div_e_le_eight : 2 / (1 - 2 / exp 1) ≤ 8 :=
 begin
-  rw [div_le_iff, mul_sub, mul_one, mul_div_assoc', le_sub, div_le_iff (exp_pos _)],
+  rw [div_le_iff, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff (exp_pos _)],
   { linarith [exp_one_gt_d9] },
   rw [sub_pos, div_lt_one];
   exact exp_one_gt_d9.trans' (by norm_num),
@@ -329,8 +329,8 @@ begin
   have : 0 < 1 - 2 / exp 1,
   { rw [sub_pos, div_lt_one (exp_pos _)],
     exact lt_of_le_of_lt (by norm_num) exp_one_gt_d9 },
-  rwa [le_sub, div_eq_mul_one_div x, div_eq_mul_one_div x, ←mul_sub, div_sub', ←div_eq_mul_one_div,
-    mul_div_assoc', one_le_div, ←div_le_iff this],
+  rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ←mul_sub, div_sub',
+    ←div_eq_mul_one_div, mul_div_assoc', one_le_div, ←div_le_iff this],
   { exact zero_lt_two },
   { exact two_ne_zero }
 end
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
@@ -1519,7 +1519,7 @@ calc 0 < (1 - x ^ 2 / 2) - |x| ^ 4 * (5 / 96) :
           ((div_le_div_right (by norm_num)).2 (by rw [sq, ← abs_mul_self, _root_.abs_mul];
             exact mul_le_one hx (abs_nonneg _) hx))
       ... < 1 : by norm_num)
-... ≤ cos x : sub_le.1 (abs_sub_le_iff.1 (cos_bound hx)).2
+... ≤ cos x : sub_le_comm.1 (abs_sub_le_iff.1 (cos_bound hx)).2
 
 lemma sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < sin x :=
 calc 0 < x - x ^ 3 / 6 - |x| ^ 4 * (5 / 96) :
@@ -1536,7 +1536,7 @@ calc 0 < x - x ^ 3 / 6 - |x| ^ 4 * (5 / 96) :
           (calc x ^ 3 ≤ x ^ 1 : pow_le_pow_of_le_one (le_of_lt hx0) hx dec_trivial
             ... = x : pow_one _))
     ... < x : by linarith)
-... ≤ sin x : sub_le.1 (abs_sub_le_iff.1 (sin_bound
+... ≤ sin x : sub_le_comm.1 (abs_sub_le_iff.1 (sin_bound
     (by rwa [_root_.abs_of_nonneg (le_of_lt hx0)]))).2
 
 lemma sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) : 0 < sin x :=
diff --git a/src/data/complex/exponential_bounds.lean b/src/data/complex/exponential_bounds.lean
@@ -33,7 +33,7 @@ begin
 end
 
 lemma exp_one_gt_d9 : 2.7182818283 < exp 1 :=
-lt_of_lt_of_le (by norm_num) (sub_le.1 (abs_sub_le_iff.1 exp_one_near_10).2)
+lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)
 
 lemma exp_one_lt_d9 : exp 1 < 2.7182818286 :=
 lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) (by norm_num)
@@ -48,7 +48,7 @@ end
 lemma exp_neg_one_lt_d9 : exp (-1) < 0.36787944120 :=
 begin
   rw [exp_neg, inv_lt (exp_pos _)],
-  refine lt_of_lt_of_le _ (sub_le.1 (abs_sub_le_iff.1 exp_one_near_10).2),
+  refine lt_of_lt_of_le _ (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2),
   all_goals {norm_num},
 end
 
@@ -71,7 +71,7 @@ begin
 end
 
 lemma log_two_gt_d9 : 0.6931471803 < log 2 :=
-lt_of_lt_of_le (by norm_num1) (sub_le.1 (abs_sub_le_iff.1 log_two_near_10).2)
+lt_of_lt_of_le (by norm_num1) (sub_le_comm.1 (abs_sub_le_iff.1 log_two_near_10).2)
 
 lemma log_two_lt_d9 : log 2 < 0.6931471808 :=
 lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 log_two_near_10).1) (by norm_num)
diff --git a/src/data/rat/nnrat.lean b/src/data/rat/nnrat.lean
@@ -76,7 +76,7 @@ open _root_.rat (to_nnrat)
 @[simp, norm_cast] lemma coe_bit0 (q : ℚ≥0) : ((bit0 q : ℚ≥0) : ℚ) = bit0 q := rfl
 @[simp, norm_cast] lemma coe_bit1 (q : ℚ≥0) : ((bit1 q : ℚ≥0) : ℚ) = bit1 q := rfl
 @[simp, norm_cast] lemma coe_sub (h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q :=
-max_eq_left $ le_sub.2 $ by simp [show (q : ℚ) ≤ p, from h]
+max_eq_left $ le_sub_comm.2 $ by simp [show (q : ℚ) ≤ p, from h]
 
 @[simp] lemma coe_eq_zero : (q : ℚ) = 0 ↔ q = 0 := by norm_cast
 lemma coe_ne_zero : (q : ℚ) ≠ 0 ↔ q ≠ 0 := coe_eq_zero.not
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
@@ -397,8 +397,8 @@ theorem mk_near_of_forall_near {f : cau_seq ℚ abs} {x : ℝ} {ε : ℝ}
 abs_sub_le_iff.2
   ⟨sub_le_iff_le_add'.2 $ mk_le_of_forall_le $
     H.imp $ λ i h j ij, sub_le_iff_le_add'.1 (abs_sub_le_iff.1 $ h j ij).1,
-  sub_le.1 $ le_mk_of_forall_le $
-    H.imp $ λ i h j ij, sub_le.1 (abs_sub_le_iff.1 $ h j ij).2⟩
+  sub_le_comm.1 $ le_mk_of_forall_le $
+    H.imp $ λ i h j ij, sub_le_comm.1 (abs_sub_le_iff.1 $ h j ij).2⟩
 
 instance : archimedean ℝ :=
 archimedean_iff_rat_le.2 $ λ x, real.ind_mk x $ λ f,
@@ -478,7 +478,7 @@ begin
     replace hK := hK.le.trans (nat.cast_le.2 nK),
     have n0 : 0 < n := nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK),
     refine le_trans _ (hf₂ _ n0 _ xS).le,
-    rwa [le_sub, inv_le ((nat.cast_pos.2 n0):((_:ℝ) < _)) xz] },
+    rwa [le_sub_comm, inv_le ((nat.cast_pos.2 n0):((_:ℝ) < _)) xz] },
   { exact mk_le_of_forall_le ⟨1, λ n n1,
       let ⟨x, xS, hx⟩ := hf₁ _ n1 in le_trans hx (h xS)⟩ }
 end
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
@@ -126,7 +126,7 @@ protected lemma coe_two : ((2 : ℝ≥0) : ℝ) = 2 := rfl
 
 @[simp, norm_cast] protected lemma coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) :
   ((r₁ - r₂ : ℝ≥0) : ℝ) = r₁ - r₂ :=
-max_eq_left $ le_sub.2 $ by simp [show (r₂ : ℝ) ≤ r₁, from h]
+max_eq_left $ le_sub_comm.2 $ by simp [show (r₂ : ℝ) ≤ r₁, from h]
 
 @[simp, norm_cast] protected lemma coe_eq_zero (r : ℝ≥0) : ↑r = (0 : ℝ) ↔ r = 0 :=
 by rw [← nnreal.coe_zero, nnreal.coe_eq]
diff --git a/src/data/real/pi/bounds.lean b/src/data/real/pi/bounds.lean
@@ -66,7 +66,7 @@ theorem pi_lower_bound_start (n : ℕ) {a}
 begin
   refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series n), rw [mul_comm],
   refine (div_le_iff (pow_pos (by norm_num) _ : (0 : ℝ) < _)).mp (le_sqrt_of_sq_le _),
-  rwa [le_sub, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
+  rwa [le_sub_comm, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
 end
 
 lemma sqrt_two_add_series_step_up (c d : ℕ) {a b n : ℕ} {z : ℝ}
@@ -102,7 +102,7 @@ theorem pi_upper_bound_start (n : ℕ) {a}
   (h₂ : 1 / 4 ^ n ≤ a) : π < a :=
 begin
   refine lt_of_lt_of_le (pi_lt_sqrt_two_add_series n) _,
-  rw [← le_sub_iff_add_le, ← le_div_iff', sqrt_le_left, sub_le],
+  rw [← le_sub_iff_add_le, ← le_div_iff', sqrt_le_left, sub_le_comm],
   { rwa [nat.cast_zero, zero_div] at h },
   { exact div_nonneg (sub_nonneg.2 h₂) (pow_nonneg (le_of_lt zero_lt_two) _) },
   { exact pow_pos zero_lt_two _ }
diff --git a/src/data/set/intervals/basic.lean b/src/data/set/intervals/basic.lean
@@ -1363,19 +1363,19 @@ and_congr lt_sub_iff_add_lt sub_lt_iff_lt_add
 
 /-! `sub_mem_Ixx_iff_right` -/
 lemma sub_mem_Icc_iff_right : a - b ∈ set.Icc c d ↔ b ∈ set.Icc (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_le le_sub
+(and_comm _ _).trans $ and_congr sub_le_comm le_sub_comm
 lemma sub_mem_Ico_iff_right : a - b ∈ set.Ico c d ↔ b ∈ set.Ioc (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_lt le_sub
+(and_comm _ _).trans $ and_congr sub_lt_comm le_sub_comm
 lemma sub_mem_Ioc_iff_right : a - b ∈ set.Ioc c d ↔ b ∈ set.Ico (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_le lt_sub
+(and_comm _ _).trans $ and_congr sub_le_comm lt_sub_comm
 lemma sub_mem_Ioo_iff_right : a - b ∈ set.Ioo c d ↔ b ∈ set.Ioo (a - d) (a - c) :=
-(and_comm _ _).trans $ and_congr sub_lt lt_sub
+(and_comm _ _).trans $ and_congr sub_lt_comm lt_sub_comm
 
 -- I think that symmetric intervals deserve attention and API: they arise all the time,
 -- for instance when considering metric balls in `ℝ`.
 lemma mem_Icc_iff_abs_le {R : Type*} [linear_ordered_add_comm_group R] {x y z : R} :
   |x - y| ≤ z ↔ y ∈ Icc (x - z) (x + z) :=
-abs_le.trans $ (and_comm _ _).trans $ and_congr sub_le neg_le_sub_iff_le_add
+abs_le.trans $ (and_comm _ _).trans $ and_congr sub_le_comm neg_le_sub_iff_le_add
 
 end ordered_add_comm_group
 
diff --git a/src/data/set/intervals/image_preimage.lean b/src/data/set/intervals/image_preimage.lean
@@ -204,16 +204,16 @@ by simp [sub_eq_add_neg]
 -/
 
 @[simp] lemma preimage_const_sub_Ici : (λ x, a - x) ⁻¹' (Ici b) = Iic (a - b) :=
-ext $ λ x, le_sub
+ext $ λ x, le_sub_comm
 
 @[simp] lemma preimage_const_sub_Iic : (λ x, a - x) ⁻¹' (Iic b) = Ici (a - b) :=
-ext $ λ x, sub_le
+ext $ λ x, sub_le_comm
 
 @[simp] lemma preimage_const_sub_Ioi : (λ x, a - x) ⁻¹' (Ioi b) = Iio (a - b) :=
-ext $ λ x, lt_sub
+ext $ λ x, lt_sub_comm
 
 @[simp] lemma preimage_const_sub_Iio : (λ x, a - x) ⁻¹' (Iio b) = Ioi (a - b) :=
-ext $ λ x, sub_lt
+ext $ λ x, sub_lt_comm
 
 @[simp] lemma preimage_const_sub_Icc : (λ x, a - x) ⁻¹' (Icc b c) = Icc (a - c) (a - b) :=
 by simp [← Ici_inter_Iic, inter_comm]
diff --git a/src/geometry/manifold/instances/real.lean b/src/geometry/manifold/instances/real.lean
@@ -291,7 +291,7 @@ begin
     rintro _ ⟨⟨hz₁, hz₂⟩, ⟨z, hz₀⟩, rfl⟩,
     simp only [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart, max_lt_iff,
       update_same, max_eq_left hz₀] with mfld_simps at hz₁ hz₂,
-    rw lt_sub at hz₁,
+    rw lt_sub_comm at hz₁,
     ext i,
     rw subsingleton.elim i 0,
     simp only [model_with_corners_euclidean_half_space, Icc_left_chart, Icc_right_chart,
diff --git a/src/linear_algebra/affine_space/ordered.lean b/src/linear_algebra/affine_space/ordered.lean
@@ -237,7 +237,7 @@ begin
   revert h, generalize : 1 - r = r', clear r, intro h,
   simp_rw [line_map_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul],
   rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub, le_inv_smul_iff h,
-    smul_smul, mul_inv_cancel_right₀, le_sub, ← neg_sub (f b), smul_neg, neg_add_eq_sub],
+    smul_smul, mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b), smul_neg, neg_add_eq_sub],
   { exact right_ne_zero_of_mul h.ne' },
   { apply_instance }
 end
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
@@ -1029,7 +1029,7 @@ begin
   begin
     rw ennreal.mul_lt_top_iff,
     refine or.inl ⟨hfq_lt_top, ennreal.rpow_lt_top_of_nonneg _ (measure_ne_top μ set.univ)⟩,
-    rwa [le_sub, sub_zero, one_div, one_div, inv_le_inv hq_pos hp_pos],
+    rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv hq_pos hp_pos],
   end
 end
 
diff --git a/src/probability/martingale/upcrossing.lean b/src/probability/martingale/upcrossing.lean
@@ -418,8 +418,7 @@ lemma submartingale.sum_sub_upcrossing_strat_mul [is_finite_measure μ] (hf : su
 begin
   refine hf.sum_mul_sub (λ n, (adapted_const ℱ 1 n).sub (hf.adapted.upcrossing_strat_adapted n))
     (_ : ∀ n ω, (1 - upcrossing_strat a b f N n) ω ≤ 1) _,
-  { refine λ n ω, sub_le.1 _,
-    simp [upcrossing_strat_nonneg] },
+  { exact λ n ω, sub_le_self _ upcrossing_strat_nonneg },
   { intros n ω,
     simp [upcrossing_strat_le_one] }
 end
diff --git a/src/tactic/omega/int/dnf.lean b/src/tactic/omega/int/dnf.lean
@@ -155,7 +155,7 @@ begin
       rw [list.forall_mem_singleton],
       simp only [val_canonize,
         preterm.val, term.val_sub],
-      rw [le_sub, sub_zero], assumption } },
+      rw [le_sub_comm, sub_zero], assumption } },
   { cases h1 },
   { cases h2 with h2 h2;
     [ {cases (ihp h1.left h2) with c h3},
diff --git a/src/tactic/omega/nat/dnf.lean b/src/tactic/omega/nat/dnf.lean
@@ -43,7 +43,7 @@ begin
     rw list.forall_mem_singleton,
     simp only [val_canonize (h0.left), val_canonize (h0.right),
       term.val_sub, preform.holds, sub_eq_add_neg] at *,
-    rw [←sub_eq_add_neg, le_sub, sub_zero, int.coe_nat_le],
+    rw [←sub_eq_add_neg, le_sub_comm, sub_zero, int.coe_nat_le],
     assumption },
   { cases h1 },
   { cases h2 with h2 h2;
diff --git a/src/topology/algebra/order/basic.lean b/src/topology/algebra/order/basic.lean
@@ -1582,7 +1582,7 @@ variables {l : filter β} {f g : β → α}
 lemma nhds_eq_infi_abs_sub (a : α) : 𝓝 a = (⨅r>0, 𝓟 {b | |a - b| < r}) :=
 begin
   simp only [le_antisymm_iff, nhds_eq_order, le_inf_iff, le_infi_iff, le_principal_iff, mem_Ioi,
-    mem_Iio, abs_sub_lt_iff, @sub_lt_iff_lt_add _ _ _ _ _ _ a, @sub_lt _ _ _ _ a, set_of_and],
+    mem_Iio, abs_sub_lt_iff, @sub_lt_iff_lt_add _ _ _ _ _ _ a, @sub_lt_comm _ _ _ _ a, set_of_and],
   refine ⟨_, _, _⟩,
   { intros ε ε0,
     exact inter_mem_inf
@@ -1663,7 +1663,7 @@ lemma nhds_basis_Ioo_pos [no_min_order α] [no_max_order α] (a : α) :
     refine ⟨min (a-l) (u-a), by apply lt_min; rwa sub_pos, _⟩,
     rintros x ⟨hx, hx'⟩,
     apply h',
-    rw [sub_lt, lt_min_iff, sub_lt_sub_iff_left] at hx,
+    rw [sub_lt_comm, lt_min_iff, sub_lt_sub_iff_left] at hx,
     rw [← sub_lt_iff_lt_add', lt_min_iff, sub_lt_sub_iff_right] at hx',
     exact ⟨hx.1, hx'.2⟩ },
   { rintros ⟨ε, ε_pos, h⟩,
@@ -2033,11 +2033,11 @@ instance linear_ordered_field.to_topological_division_ring : topological_divisio
     rintros ε ⟨hε : ε > 0, hεt : ε ≤ t⁻¹⟩,
     refine ⟨min (t ^ 2 * ε / 2) (t / 2), by positivity, λ x h, _⟩,
     have hx : t / 2 < x,
-    { rw [set.mem_Ioo, sub_lt, lt_min_iff] at h,
+    { rw [set.mem_Ioo, sub_lt_comm, lt_min_iff] at h,
       nlinarith },
     have hx' : 0 < x := (half_pos ht).trans hx,
     have aux : 0 < 2 / t ^ 2 := by positivity,
-    rw [set.mem_Ioo, ←sub_lt_iff_lt_add', sub_lt, ←abs_sub_lt_iff] at h ⊢,
+    rw [set.mem_Ioo, ←sub_lt_iff_lt_add', sub_lt_comm, ←abs_sub_lt_iff] at h ⊢,
     rw [inv_sub_inv ht.ne' hx'.ne', abs_div, div_eq_mul_inv],
     suffices : |t * x|⁻¹ < 2 / t ^ 2,
     { rw [←abs_neg, neg_sub],
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
