diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean
index f100e4b04bde7..8d93049b266b8 100644
--- a/src/algebra/group_power/lemmas.lean
+++ b/src/algebra/group_power/lemmas.lean
@@ -365,7 +365,7 @@ calc 1 + (n + 2) •ℕ a ≤ 1 + (n + 2) •ℕ a + (n •ℕ (a * a * (2 + a))
 /-- Bernoulli's inequality reformulated to estimate `a^n`. -/
 theorem one_add_sub_mul_le_pow [linear_ordered_ring R]
   {a : R} (H : -1 ≤ a) (n : ℕ) : 1 + n •ℕ (a - 1) ≤ a ^ n :=
-have -2 ≤ a - 1, by { rw [bit0, neg_add, ← sub_eq_add_neg], exact sub_le_sub_right H 1 },
+have -2 ≤ a - 1, by rwa [bit0, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right],
 by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
 
 namespace int
diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean
index 8b95c819ed436..4dcd55c367109 100644
--- a/src/algebra/ordered_group.lean
+++ b/src/algebra/ordered_group.lean
@@ -376,241 +376,21 @@ end ordered_comm_group
 section ordered_add_comm_group
 variables [ordered_add_comm_group α] {a b c d : α}
 
-lemma sub_nonneg_of_le (h : b ≤ a) : 0 ≤ a - b :=
-begin
-  have h := add_le_add_right h (-b),
-  rwa [add_right_neg, ← sub_eq_add_neg] at h
-end
-
-lemma le_of_sub_nonneg (h : 0 ≤ a - b) : b ≤ a :=
-begin
-  have h := add_le_add_right h b,
-  rwa [sub_add_cancel, zero_add] at h
-end
-
-lemma sub_nonpos_of_le (h : a ≤ b) : a - b ≤ 0 :=
-begin
-  have h := add_le_add_right h (-b),
-  rwa [add_right_neg, ← sub_eq_add_neg] at h
-end
-
-lemma le_of_sub_nonpos (h : a - b ≤ 0) : a ≤ b :=
-begin
-  have h := add_le_add_right h b,
-  rwa [sub_add_cancel, zero_add] at h
-end
-
-lemma sub_pos_of_lt (h : b < a) : 0 < a - b :=
-begin
-  have h := add_lt_add_right h (-b),
-  rwa [add_right_neg, ← sub_eq_add_neg] at h
-end
-
-lemma lt_of_sub_pos (h : 0 < a - b) : b < a :=
-begin
-  have h := add_lt_add_right h b,
-  rwa [sub_add_cancel, zero_add] at h
-end
-
-lemma sub_neg_of_lt (h : a < b) : a - b < 0 :=
-begin
-  have h := add_lt_add_right h (-b),
-  rwa [add_right_neg, ← sub_eq_add_neg] at h
-end
-
-lemma lt_of_sub_neg (h : a - b < 0) : a < b :=
-begin
-  have h := add_lt_add_right h b,
-  rwa [sub_add_cancel, zero_add] at h
-end
-
-lemma add_le_of_le_sub_left (h : b ≤ c - a) : a + b ≤ c :=
-begin
-  have h := add_le_add_left h a,
-  rwa [← add_sub_assoc, add_comm a c, add_sub_cancel] at h
-end
-
-lemma le_sub_left_of_add_le (h : a + b ≤ c) : b ≤ c - a :=
-begin
-  have h := add_le_add_right h (-a),
-  rwa [add_comm a b, add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma add_le_of_le_sub_right (h : a ≤ c - b) : a + b ≤ c :=
-begin
-  have h := add_le_add_right h b,
-  rwa sub_add_cancel at h
-end
-
-lemma le_sub_right_of_add_le (h : a + b ≤ c) : a ≤ c - b :=
-begin
-  have h := add_le_add_right h (-b),
-  rwa [add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma le_add_of_sub_left_le (h : a - b ≤ c) : a ≤ b + c :=
-begin
-  have h := add_le_add_right h b,
-  rwa [sub_add_cancel, add_comm] at h
-end
-
-lemma sub_left_le_of_le_add (h : a ≤ b + c) : a - b ≤ c :=
-begin
-  have h := add_le_add_right h (-b),
-  rwa [add_comm b c, add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma le_add_of_sub_right_le (h : a - c ≤ b) : a ≤ b + c :=
-begin
-  have h := add_le_add_right h c,
-  rwa sub_add_cancel at h
-end
-
-lemma sub_right_le_of_le_add (h : a ≤ b + c) : a - c ≤ b :=
-begin
-  have h := add_le_add_right h (-c),
-  rwa [add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma le_add_of_neg_le_sub_left (h : -a ≤ b - c) : c ≤ a + b :=
-le_add_of_neg_add_le_left (add_le_of_le_sub_right h)
-
-lemma neg_le_sub_left_of_le_add (h : c ≤ a + b) : -a ≤ b - c :=
-begin
-  rw [sub_eq_add_neg, add_comm],
-  apply le_neg_add_of_add_le,
-  have h := (sub_left_le_of_le_add h),
-  rwa sub_eq_add_neg at h
-end
-
-lemma le_add_of_neg_le_sub_right (h : -b ≤ a - c) : c ≤ a + b :=
-begin
-  have h := add_le_of_le_sub_left h,
-  rw ← sub_eq_add_neg at h,
-  exact le_add_of_sub_right_le h
-end
-
-lemma neg_le_sub_right_of_le_add (h : c ≤ a + b) : -b ≤ a - c :=
-begin
-  have h := sub_right_le_of_le_add h,
-  rw sub_eq_add_neg at h,
-  exact le_sub_left_of_add_le h
-end
-
-lemma sub_le_of_sub_le (h : a - b ≤ c) : a - c ≤ b :=
-sub_left_le_of_le_add (le_add_of_sub_right_le h)
-
-lemma sub_le_sub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
-by simpa only [sub_eq_add_neg] using add_le_add_left (neg_le_neg h) c
-
-lemma sub_le_sub_right (h : a ≤ b) (c : α) : a - c ≤ b - c :=
-by simpa only [sub_eq_add_neg] using add_le_add_right h (-c)
-
 lemma sub_le_sub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
 by simpa only [sub_eq_add_neg] using add_le_add hab (neg_le_neg hcd)
 
-lemma add_lt_of_lt_sub_left (h : b < c - a) : a + b < c :=
-begin
-  have h := add_lt_add_left h a,
-  rwa [← add_sub_assoc, add_comm a c, add_sub_cancel] at h
-end
-
-lemma lt_sub_left_of_add_lt (h : a + b < c) : b < c - a :=
-begin
-  have h := add_lt_add_right h (-a),
-  rwa [add_comm a b, add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma add_lt_of_lt_sub_right (h : a < c - b) : a + b < c :=
-begin
-  have h := add_lt_add_right h b,
-  rwa sub_add_cancel at h
-end
-
-lemma lt_sub_right_of_add_lt (h : a + b < c) : a < c - b :=
-begin
-  have h := add_lt_add_right h (-b),
-  rwa [add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma lt_add_of_sub_left_lt (h : a - b < c) : a < b + c :=
-begin
-  have h := add_lt_add_right h b,
-  rwa [sub_add_cancel, add_comm] at h
-end
-
-lemma sub_left_lt_of_lt_add (h : a < b + c) : a - b < c :=
-begin
-  have h := add_lt_add_right h (-b),
-  rwa [add_comm b c, add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma lt_add_of_sub_right_lt (h : a - c < b) : a < b + c :=
-begin
-  have h := add_lt_add_right h c,
-  rwa sub_add_cancel at h
-end
-
-lemma sub_right_lt_of_lt_add (h : a < b + c) : a - c < b :=
-begin
-  have h := add_lt_add_right h (-c),
-  rwa [add_neg_cancel_right, ← sub_eq_add_neg] at h
-end
-
-lemma lt_add_of_neg_lt_sub_left (h : -a < b - c) : c < a + b :=
-lt_add_of_neg_add_lt_left (add_lt_of_lt_sub_right h)
-
-lemma neg_lt_sub_left_of_lt_add (h : c < a + b) : -a < b - c :=
-begin
-  have h := sub_left_lt_of_lt_add h,
-  rw sub_eq_add_neg at h,
-  have h := lt_neg_add_of_add_lt h,
-  rwa [add_comm, ← sub_eq_add_neg] at h
-end
-
-lemma lt_add_of_neg_lt_sub_right (h : -b < a - c) : c < a + b :=
-begin
-  have h := add_lt_of_lt_sub_left h,
-  rw ← sub_eq_add_neg at h,
-  exact lt_add_of_sub_right_lt h
-end
-
-lemma neg_lt_sub_right_of_lt_add (h : c < a + b) : -b < a - c :=
-begin
-  have h := sub_right_lt_of_lt_add h,
-  rw sub_eq_add_neg at h,
-  exact lt_sub_left_of_add_lt h
-end
-
-lemma sub_lt_of_sub_lt (h : a - b < c) : a - c < b :=
-sub_left_lt_of_lt_add (lt_add_of_sub_right_lt h)
-
-lemma sub_lt_sub_left (h : a < b) (c : α) : c - b < c - a :=
-by simpa only [sub_eq_add_neg] using add_lt_add_left (neg_lt_neg h) c
-
-lemma sub_lt_sub_right (h : a < b) (c : α) : a - c < b - c :=
-by simpa only [sub_eq_add_neg] using add_lt_add_right h (-c)
-
 lemma sub_lt_sub (hab : a < b) (hcd : c < d) : a - d < b - c :=
 by simpa only [sub_eq_add_neg] using add_lt_add hab (neg_lt_neg hcd)
 
-lemma sub_lt_sub_of_le_of_lt (hab : a ≤ b) (hcd : c < d) : a - d < b - c :=
-by simpa only [sub_eq_add_neg] using add_lt_add_of_le_of_lt hab (neg_lt_neg hcd)
+@[simp] lemma sub_le_self_iff (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b :=
+by simp [sub_eq_add_neg]
 
-lemma sub_lt_sub_of_lt_of_le (hab : a < b) (hcd : c ≤ d) : a - d < b - c :=
-by simpa only [sub_eq_add_neg] using add_lt_add_of_lt_of_le hab (neg_le_neg hcd)
+alias sub_le_self_iff ↔ _ sub_le_self
 
-lemma sub_le_self (a : α) {b : α} (h : 0 ≤ b) : a - b ≤ a :=
-calc
-  a - b = a + -b : sub_eq_add_neg _ _
-    ... ≤ a + 0  : add_le_add_left (neg_nonpos_of_nonneg h) _
-    ... = a      : by rw add_zero
+@[simp] lemma sub_lt_self_iff (a : α) {b : α} : a - b < a ↔ 0 < b :=
+by simp [sub_eq_add_neg]
 
-lemma sub_lt_self (a : α) {b : α} (h : 0 < b) : a - b < a :=
-calc
-  a - b = a + -b : sub_eq_add_neg _ _
-    ... < a + 0  : add_lt_add_left (neg_neg_of_pos h) _
-    ... = a      : by rw add_zero
+alias sub_lt_self_iff ↔ _ sub_lt_self
 
 lemma sub_le_sub_iff : a - b ≤ c - d ↔ a + d ≤ c + b :=
 by simpa only [sub_eq_add_neg] using add_neg_le_add_neg_iff
@@ -619,33 +399,49 @@ by simpa only [sub_eq_add_neg] using add_neg_le_add_neg_iff
 lemma sub_le_sub_iff_left (a : α) {b c : α} : a - b ≤ a - c ↔ c ≤ b :=
 by rw [sub_eq_add_neg, sub_eq_add_neg, add_le_add_iff_left, neg_le_neg_iff]
 
+lemma sub_le_sub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
+(sub_le_sub_iff_left c).2 h
+
 @[simp]
 lemma sub_le_sub_iff_right (c : α) : a - c ≤ b - c ↔ a ≤ b :=
 by simpa only [sub_eq_add_neg] using add_le_add_iff_right _
 
+lemma sub_le_sub_right (h : a ≤ b) (c : α) : a - c ≤ b - c :=
+(sub_le_sub_iff_right c).2 h
+
 @[simp]
 lemma sub_lt_sub_iff_left (a : α) {b c : α} : a - b < a - c ↔ c < b :=
 by rw [sub_eq_add_neg, sub_eq_add_neg, add_lt_add_iff_left, neg_lt_neg_iff]
 
+lemma sub_lt_sub_left (h : a < b) (c : α) : c - b < c - a :=
+(sub_lt_sub_iff_left c).2 h
+
 @[simp]
 lemma sub_lt_sub_iff_right (c : α) : a - c < b - c ↔ a < b :=
 by simpa only [sub_eq_add_neg] using add_lt_add_iff_right _
 
+lemma sub_lt_sub_right (h : a < b) (c : α) : a - c < b - c :=
+(sub_lt_sub_iff_right c).2 h
+
 @[simp] lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a :=
-have a - a ≤ a - b ↔ b ≤ a, from sub_le_sub_iff_left a,
-by rwa sub_self at this
+by rw [← sub_self a, sub_le_sub_iff_left]
+
+alias sub_nonneg ↔ le_of_sub_nonneg sub_nonneg_of_le
 
 @[simp] lemma sub_nonpos : a - b ≤ 0 ↔ a ≤ b :=
-have a - b ≤ b - b ↔ a ≤ b, from sub_le_sub_iff_right b,
-by rwa sub_self at this
+by rw [← sub_self b,  sub_le_sub_iff_right]
+
+alias sub_nonpos ↔ le_of_sub_nonpos sub_nonpos_of_le
 
 @[simp] lemma sub_pos : 0 < a - b ↔ b < a :=
-have a - a < a - b ↔ b < a, from sub_lt_sub_iff_left a,
-by rwa sub_self at this
+by rw [← sub_self a, sub_lt_sub_iff_left]
+
+alias sub_pos ↔ lt_of_sub_pos sub_pos_of_lt
 
 @[simp] lemma sub_lt_zero : a - b < 0 ↔ a < b :=
-have a - b < b - b ↔ a < b, from sub_lt_sub_iff_right b,
-by rwa sub_self at this
+by rw [← sub_self b, sub_lt_sub_iff_right]
+
+alias sub_lt_zero ↔ lt_of_sub_neg sub_neg_of_lt
 
 lemma le_sub_iff_add_le' : b ≤ c - a ↔ a + b ≤ c :=
 by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
@@ -653,9 +449,13 @@ by rw [sub_eq_add_neg, add_comm, le_neg_add_iff_add_le]
 lemma le_sub_iff_add_le : a ≤ c - b ↔ a + b ≤ c :=
 by rw [le_sub_iff_add_le', add_comm]
 
+alias le_sub_iff_add_le ↔ add_le_of_le_sub_right le_sub_right_of_add_le
+
 lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c :=
 by rw [sub_eq_add_neg, add_comm, neg_add_le_iff_le_add]
 
+alias le_sub_iff_add_le' ↔ add_le_of_le_sub_left le_sub_left_of_add_le
+
 lemma sub_le_iff_le_add : a - c ≤ b ↔ a ≤ b + c :=
 by rw [sub_le_iff_le_add', add_comm]
 
@@ -674,15 +474,23 @@ le_sub_iff_add_le'.trans le_sub_iff_add_le.symm
 lemma lt_sub_iff_add_lt' : b < c - a ↔ a + b < c :=
 by rw [sub_eq_add_neg, add_comm, lt_neg_add_iff_add_lt]
 
+alias lt_sub_iff_add_lt' ↔ add_lt_of_lt_sub_left lt_sub_left_of_add_lt
+
 lemma lt_sub_iff_add_lt : a < c - b ↔ a + b < c :=
 by rw [lt_sub_iff_add_lt', add_comm]
 
+alias lt_sub_iff_add_lt ↔ add_lt_of_lt_sub_right lt_sub_right_of_add_lt
+
 lemma sub_lt_iff_lt_add' : a - b < c ↔ a < b + c :=
 by rw [sub_eq_add_neg, add_comm, neg_add_lt_iff_lt_add]
 
+alias sub_lt_iff_lt_add' ↔ lt_add_of_sub_left_lt sub_left_lt_of_lt_add
+
 lemma sub_lt_iff_lt_add : a - c < b ↔ a < b + c :=
 by rw [sub_lt_iff_lt_add', add_comm]
 
+alias sub_lt_iff_lt_add ↔ lt_add_of_sub_right_lt sub_right_lt_of_lt_add
+
 @[simp] lemma neg_lt_sub_iff_lt_add : -b < a - c ↔ c < a + b :=
 lt_sub_iff_add_lt.trans neg_add_lt_iff_lt_add_right
 
@@ -695,12 +503,6 @@ sub_lt_iff_lt_add'.trans sub_lt_iff_lt_add.symm
 theorem lt_sub : a < b - c ↔ c < b - a :=
 lt_sub_iff_add_lt'.trans lt_sub_iff_add_lt.symm
 
-lemma sub_le_self_iff (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b :=
-sub_le_iff_le_add'.trans (le_add_iff_nonneg_left _)
-
-lemma sub_lt_self_iff (a : α) {b : α} : a - b < a ↔ 0 < b :=
-sub_lt_iff_lt_add'.trans (lt_add_iff_pos_left _)
-
 end ordered_add_comm_group
 
 /-- A decidable linearly ordered additive commutative group is an
@@ -821,7 +623,7 @@ lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = abs (a - b) :=
 begin
   cases le_total a b with ab ba,
   { rw [max_eq_right ab, min_eq_left ab, abs_of_nonpos, neg_sub], rwa sub_nonpos },
-  { rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg], exact sub_nonneg_of_le ba }
+  { rw [max_eq_left ba, min_eq_right ba, abs_of_nonneg], rwa sub_nonneg }
 end
 
 lemma max_sub_min_eq_abs (a b : α) : max a b - min a b = abs (b - a) :=
@@ -838,6 +640,18 @@ by rw [abs_le, neg_le_sub_iff_le_add, @sub_le_iff_le_add' _ _ b, and_comm]
 lemma abs_sub_lt_iff : abs (a - b) < c ↔ a - b < c ∧ b - a < c :=
 by rw [abs_lt, neg_lt_sub_iff_lt_add, @sub_lt_iff_lt_add' _ _ b, and_comm]
 
+lemma sub_le_of_abs_sub_le_left (h : abs (a - b) ≤ c) : b - c ≤ a :=
+sub_le.1 $ (abs_sub_le_iff.1 h).2
+
+lemma sub_le_of_abs_sub_le_right (h : abs (a - b) ≤ c) : a - c ≤ b :=
+sub_le_of_abs_sub_le_left (abs_sub a b ▸ h)
+
+lemma sub_lt_of_abs_sub_lt_left (h : abs (a - b) < c) : b - c < a :=
+sub_lt.1 $ (abs_sub_lt_iff.1 h).2
+
+lemma sub_lt_of_abs_sub_lt_right (h : abs (a - b) < c) : a - c < b :=
+sub_lt_of_abs_sub_lt_left (abs_sub a b ▸ h)
+
 lemma abs_sub_abs_le_abs_sub (a b : α) : abs a - abs b ≤ abs (a - b) :=
 sub_le_iff_le_add.2 $
 calc abs a = abs (a - b + b)     : by rw [sub_add_cancel]
@@ -902,7 +716,7 @@ abs_sub_le_iff.2 ⟨sub_le_sub hau hbl, sub_le_sub hbu hal⟩
 lemma eq_of_abs_sub_nonpos (h : abs (a - b) ≤ 0) : a = b :=
 eq_of_abs_sub_eq_zero (le_antisymm h (abs_nonneg (a - b)))
 
-lemma exists_gt_zero [nontrivial α] : ∃ (a:α), 0 < a :=
+lemma exists_zero_lt [nontrivial α] : ∃ (a:α), 0 < a :=
 begin
   obtain ⟨y, hy⟩ := exists_ne (0 : α),
   cases hy.lt_or_lt,
@@ -914,14 +728,14 @@ end
 instance linear_ordered_add_comm_group.to_no_top_order [nontrivial α] :
   no_top_order α :=
 ⟨ begin
-    obtain ⟨y, hy⟩ : ∃ (a:α), 0 < a := exists_gt_zero,
+    obtain ⟨y, hy⟩ : ∃ (a:α), 0 < a := exists_zero_lt,
     exact λ a, ⟨a + y, lt_add_of_pos_right a hy⟩
   end ⟩
 
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_add_comm_group.to_no_bot_order [nontrivial α] : no_bot_order α :=
 ⟨ begin
-    obtain ⟨y, hy⟩ : ∃ (a:α), 0 < a := exists_gt_zero,
+    obtain ⟨y, hy⟩ : ∃ (a:α), 0 < a := exists_zero_lt,
     exact λ a, ⟨a - y, sub_lt_self a hy⟩
   end ⟩
 
diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean
index b1c086b08be61..fe36fbe09003b 100644
--- a/src/algebra/ordered_ring.lean
+++ b/src/algebra/ordered_ring.lean
@@ -493,35 +493,27 @@ begin
 end
 
 lemma ordered_ring.mul_le_mul_of_nonneg_left (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
-have 0 ≤ b - a,       from sub_nonneg_of_le h₁,
-have 0 ≤ c * (b - a), from ordered_ring.mul_nonneg c (b - a) h₂ this,
 begin
-  rw mul_sub_left_distrib at this,
-  apply le_of_sub_nonneg this
+  rw [← sub_nonneg, ← mul_sub],
+  exact ordered_ring.mul_nonneg c (b - a) h₂ (sub_nonneg.2 h₁),
 end
 
 lemma ordered_ring.mul_le_mul_of_nonneg_right (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c :=
-have 0 ≤ b - a,       from sub_nonneg_of_le h₁,
-have 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg (b - a) c this h₂,
 begin
-  rw mul_sub_right_distrib at this,
-  apply le_of_sub_nonneg this
+  rw [← sub_nonneg, ← sub_mul],
+  exact ordered_ring.mul_nonneg _ _ (sub_nonneg.2 h₁) h₂,
 end
 
 lemma ordered_ring.mul_lt_mul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
-have 0 < b - a,       from sub_pos_of_lt h₁,
-have 0 < c * (b - a), from ordered_ring.mul_pos c (b - a) h₂ this,
 begin
-  rw mul_sub_left_distrib at this,
-  apply lt_of_sub_pos this
+  rw [← sub_pos, ← mul_sub],
+  exact ordered_ring.mul_pos _ _ h₂ (sub_pos.2 h₁),
 end
 
 lemma ordered_ring.mul_lt_mul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c :=
-have 0 < b - a,       from sub_pos_of_lt h₁,
-have 0 < (b - a) * c, from ordered_ring.mul_pos (b - a) c this h₂,
 begin
-  rw mul_sub_right_distrib at this,
-  apply lt_of_sub_pos this
+  rw [← sub_pos, ← sub_mul],
+  exact ordered_ring.mul_pos _ _ (sub_pos.2 h₁) h₂,
 end
 
 @[priority 100] -- see Note [lower instance priority]
@@ -720,32 +712,6 @@ lt_of_not_ge (λ hb, absurd h (mul_nonneg_of_nonpos_of_nonpos ha hb).not_lt)
 lemma mul_self_add_mul_self_eq_zero {x y : α} : x * x + y * y = 0 ↔ x = 0 ∧ y = 0 :=
 by rw [add_eq_zero_iff', mul_self_eq_zero, mul_self_eq_zero]; apply mul_self_nonneg
 
-lemma sub_le_of_abs_sub_le_left (h : abs (a - b) ≤ c) : b - c ≤ a :=
-if hz : 0 ≤ a - b then
-  (calc
-      a ≥ b     : le_of_sub_nonneg hz
-    ... ≥ b - c : sub_le_self _ $ (abs_nonneg _).trans h)
-else
-  have habs : b - a ≤ c, by rwa [abs_of_neg (lt_of_not_ge hz), neg_sub] at h,
-  have habs' : b ≤ c + a, from le_add_of_sub_right_le habs,
-  sub_left_le_of_le_add habs'
-
-lemma sub_le_of_abs_sub_le_right (h : abs (a - b) ≤ c) : a - c ≤ b :=
-sub_le_of_abs_sub_le_left (abs_sub a b ▸ h)
-
-lemma sub_lt_of_abs_sub_lt_left (h : abs (a - b) < c) : b - c < a :=
-if hz : 0 ≤ a - b then
-   (calc
-      a ≥ b     : le_of_sub_nonneg hz
-    ... > b - c : sub_lt_self _ ((abs_nonneg _).trans_lt h))
-else
-  have habs : b - a < c, by rwa [abs_of_neg (lt_of_not_ge hz), neg_sub] at h,
-  have habs' : b < c + a, from lt_add_of_sub_right_lt habs,
-  sub_left_lt_of_lt_add habs'
-
-lemma sub_lt_of_abs_sub_lt_right (h : abs (a - b) < c) : a - c < b :=
-sub_lt_of_abs_sub_lt_left (abs_sub a b ▸ h)
-
 lemma eq_zero_of_mul_self_add_mul_self_eq_zero (h : a * a + b * b = 0) : a = 0 :=
 (mul_self_add_mul_self_eq_zero.mp h).left
 
diff --git a/src/data/int/basic.lean b/src/data/int/basic.lean
index 2015b2070ce70..48d3901122c51 100644
--- a/src/data/int/basic.lean
+++ b/src/data/int/basic.lean
@@ -587,8 +587,8 @@ by rw [mul_comm, mul_comm c, mul_div_mul_of_pos _ _ H]
 by rw [mod_def, mod_def, mul_div_mul_of_pos _ _ H, mul_sub_left_distrib, mul_assoc]
 
 theorem lt_div_add_one_mul_self (a : ℤ) {b : ℤ} (H : 0 < b) : a < (a / b + 1) * b :=
-by rw [add_mul, one_mul, mul_comm]; apply lt_add_of_sub_left_lt;
-   rw [← mod_def]; apply mod_lt_of_pos _ H
+by { rw [add_mul, one_mul, mul_comm, ← sub_lt_iff_lt_add', ← mod_def],
+  exact mod_lt_of_pos _ H }
 
 theorem abs_div_le_abs : ∀ (a b : ℤ), abs (a / b) ≤ abs a :=
 suffices ∀ (a : ℤ) (n : ℕ), abs (a / n) ≤ abs a, from
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
index 38b6d2cc79e25..560671d1deafb 100644
--- a/src/data/real/basic.lean
+++ b/src/data/real/basic.lean
@@ -399,7 +399,7 @@ begin
     ((lt_total _ _).resolve_left (λ h, _)).resolve_right (λ h, _)⟩,
   { rcases h with ⟨ε, ε0, i, ih⟩,
     refine not_lt_of_le (Sup_le_ub S lb (ub' _ _))
-      ((sub_lt_self_iff _).2 (half_pos ε0)),
+      (sub_lt_self _ (half_pos ε0)),
     refine ⟨_, half_pos ε0, i, λ j ij, _⟩,
     rw [sub_apply, const_apply, sub_right_comm,
       le_sub_iff_add_le, add_halves],