feat(data/real/ennreal): tsub lemmas (#13525)

Inherit lemmas about subtraction on `ℝ≥0∞` from `algebra.order.sub`. Generalize `add_le_cancellable.tsub_lt_self` in passing.

New `ennreal` lemmas

Author: YaelDillies

src/algebra/order/sub.lean

@@ -693,23 +693,16 @@ protected lemma tsub_lt_tsub_iff_right (hc : add_le_cancellable c) (h : c ≤ a)
   a - c < b - c ↔ a < b :=
 by rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
 
-protected lemma tsub_lt_self (ha : add_le_cancellable a) (hb : add_le_cancellable b)
-  (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a :=
+protected lemma tsub_lt_self (ha : add_le_cancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a :=
 begin
-  refine tsub_le_self.lt_of_ne _,
-  intro h,
+  refine tsub_le_self.lt_of_ne (λ h, _),
   rw [← h, tsub_pos_iff_lt] at h₁,
-  have := h.ge,
-  rw [hb.le_tsub_iff_left h₁.le, ha.add_le_iff_nonpos_left] at this,
-  exact h₂.not_le this,
+  exact h₂.not_le (ha.add_le_iff_nonpos_left.1 $ add_le_of_le_tsub_left_of_le h₁.le h.ge),
 end
 
-protected lemma tsub_lt_self_iff (ha : add_le_cancellable a) (hb : add_le_cancellable b) :
-  a - b < a ↔ 0 < a ∧ 0 < b :=
+protected lemma tsub_lt_self_iff (ha : add_le_cancellable a) : a - b < a ↔ 0 < a ∧ 0 < b :=
 begin
-  refine ⟨_, λ h, ha.tsub_lt_self hb h.1 h.2⟩,
-  intro h,
-  refine ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne _⟩,
+  refine ⟨λ h, ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne _⟩, λ h, ha.tsub_lt_self h.1 h.2⟩,
   rintro rfl,
   rw [tsub_zero] at h,
   exact h.false
@@ -729,11 +722,10 @@ variable [contravariant_class α α (+) (≤)]
 lemma tsub_lt_tsub_iff_right (h : c ≤ a) : a - c < b - c ↔ a < b :=
 contravariant.add_le_cancellable.tsub_lt_tsub_iff_right h
 
-lemma tsub_lt_self (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a :=
-contravariant.add_le_cancellable.tsub_lt_self contravariant.add_le_cancellable h₁ h₂
+lemma tsub_lt_self : 0 < a → 0 < b → a - b < a := contravariant.add_le_cancellable.tsub_lt_self
 
 lemma tsub_lt_self_iff : a - b < a ↔ 0 < a ∧ 0 < b :=
-contravariant.add_le_cancellable.tsub_lt_self_iff contravariant.add_le_cancellable
+contravariant.add_le_cancellable.tsub_lt_self_iff
 
 /-- See `lt_tsub_iff_left_of_le_of_le` for a weaker statement in a partial order. -/
 lemma tsub_lt_tsub_iff_left_of_le (h : b ≤ a) : a - b < a - c ↔ c < b :=

src/data/real/ennreal.lean

@@ -743,37 +743,54 @@ by { cases a; cases b; simp [← with_top.coe_sub] }
 lemma sub_ne_top (ha : a ≠ ∞) : a - b ≠ ∞ :=
 mt sub_eq_top_iff.mp $ mt and.left ha
 
-protected lemma sub_lt_of_lt_add (hac : c ≤ a) (h : a < b + c) : a - c < b :=
-((cancel_of_lt' $ hac.trans_lt h).tsub_lt_iff_right hac).mpr h
+protected lemma sub_eq_of_eq_add (hb : b ≠ ∞) : a = c + b → a - b = c :=
+(cancel_of_ne hb).tsub_eq_of_eq_add
 
-@[simp] lemma add_sub_self (hb : b ≠ ∞) : (a + b) - b = a :=
-(cancel_of_ne hb).add_tsub_cancel_right
+protected lemma eq_sub_of_add_eq (hc : c ≠ ∞) : a + c = b → a = b - c :=
+(cancel_of_ne hc).eq_tsub_of_add_eq
 
-@[simp] lemma add_sub_self' (ha : a ≠ ∞) : (a + b) - a = b :=
-(cancel_of_ne ha).add_tsub_cancel_left
+protected lemma sub_eq_of_eq_add_rev (hb : b ≠ ∞) : a = b + c → a - b = c :=
+(cancel_of_ne hb).tsub_eq_of_eq_add_rev
 
 lemma sub_eq_of_add_eq (hb : b ≠ ∞) (hc : a + b = c) : c - b = a :=
-(cancel_of_ne hb).tsub_eq_of_eq_add hc.symm
+ennreal.sub_eq_of_eq_add hb hc.symm
 
-protected lemma lt_add_of_sub_lt (ht : a ≠ ∞ ∨ b ≠ ∞) (h : a - b < c) : a < c + b :=
+@[simp] protected lemma add_sub_cancel_left (ha : a ≠ ∞) : a + b - a = b :=
+(cancel_of_ne ha).add_tsub_cancel_left
+
+@[simp] protected lemma add_sub_cancel_right (hb : b ≠ ∞) : a + b - b = a :=
+(cancel_of_ne hb).add_tsub_cancel_right
+
+protected lemma lt_add_of_sub_lt_left (h : a ≠ ∞ ∨ b ≠ ∞) : a - b < c → a < b + c :=
 begin
-  rcases eq_or_ne b ∞ with rfl|hb,
-  { rw [add_top, lt_top_iff_ne_top], exact ht.resolve_right (not_not.2 rfl) },
-  { exact (cancel_of_ne hb).lt_add_of_tsub_lt_right h }
+  obtain rfl | hb := eq_or_ne b ∞,
+  { rw [top_add, lt_top_iff_ne_top],
+    exact λ _, h.resolve_right (not_not.2 rfl) },
+  { exact (cancel_of_ne hb).lt_add_of_tsub_lt_left }
 end
 
-protected lemma sub_lt_iff_lt_add (hb : b ≠ ∞) (hab : b ≤ a) : a - b < c ↔ a < c + b :=
-(cancel_of_ne hb).tsub_lt_iff_right hab
-
-protected lemma sub_lt_self (hat : a ≠ ∞) (ha0 : a ≠ 0) (hb : b ≠ 0) : a - b < a :=
+protected lemma lt_add_of_sub_lt_right (h : a ≠ ∞ ∨ c ≠ ∞) : a - c < b → a < b + c :=
 begin
-  cases b, { simp [pos_iff_ne_zero, ha0] },
-  exact (cancel_of_ne hat).tsub_lt_self cancel_coe (pos_iff_ne_zero.mpr ha0)
-    (pos_iff_ne_zero.mpr hb)
+  obtain rfl | hc := eq_or_ne c ∞,
+  { rw [add_top, lt_top_iff_ne_top],
+    exact λ _, h.resolve_right (not_not.2 rfl) },
+  { exact (cancel_of_ne hc).lt_add_of_tsub_lt_right }
 end
 
+protected lemma sub_lt_of_lt_add (hac : c ≤ a) (h : a < b + c) : a - c < b :=
+((cancel_of_lt' $ hac.trans_lt h).tsub_lt_iff_right hac).mpr h
+
+protected lemma sub_lt_iff_lt_right (hb : b ≠ ∞) (hab : b ≤ a) : a - b < c ↔ a < c + b :=
+(cancel_of_ne hb).tsub_lt_iff_right hab
+
+protected lemma sub_lt_self (ha : a ≠ ∞) (ha₀ : a ≠ 0) (hb : b ≠ 0) : a - b < a :=
+(cancel_of_ne ha).tsub_lt_self (pos_iff_ne_zero.2 ha₀) (pos_iff_ne_zero.2 hb)
+
+protected lemma sub_lt_self_iff (ha : a ≠ ∞) : a - b < a ↔ 0 < a ∧ 0 < b :=
+(cancel_of_ne ha).tsub_lt_self_iff
+
 lemma sub_lt_of_sub_lt (h₂ : c ≤ a) (h₃ : a ≠ ∞ ∨ b ≠ ∞) (h₁ : a - b < c) : a - c < b :=
-ennreal.sub_lt_of_lt_add h₂ (add_comm c b ▸ ennreal.lt_add_of_sub_lt h₃ h₁)
+ennreal.sub_lt_of_lt_add h₂ (add_comm c b ▸ ennreal.lt_add_of_sub_lt_right h₃ h₁)
 
 lemma sub_sub_cancel (h : a ≠ ∞) (h2 : b ≤ a) : a - (a - b) = b :=
 (cancel_of_ne $ sub_ne_top h).tsub_tsub_cancel_of_le h2
@@ -1190,8 +1207,7 @@ le_of_forall_nnreal_lt $ λ r hr, (zero_le r).eq_or_lt.elim (λ h, h ▸ zero_le
 lemma eq_top_of_forall_nnreal_le {x : ℝ≥0∞} (h : ∀ r : ℝ≥0, ↑r ≤ x) : x = ∞ :=
 top_unique $ le_of_forall_nnreal_lt $ λ r hr, h r
 
-lemma add_div {a b c : ℝ≥0∞} : (a + b) / c = a / c + b / c :=
-right_distrib a b (c⁻¹)
+lemma add_div : (a + b) / c = a / c + b / c := right_distrib a b (c⁻¹)
 
 lemma div_add_div_same {a b c : ℝ≥0∞} : a / c + b / c = (a + b) / c :=
 eq.symm $ right_distrib a b (c⁻¹)

src/measure_theory/measure/regular.lean

@@ -163,7 +163,7 @@ begin
   { refine ⟨∅, empty_subset _, h0, _⟩,
     rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero] },
   { rcases H hU _ (ennreal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩,
-    exact ⟨K, hKU, hKc, ennreal.lt_add_of_sub_lt (or.inl hμU) hrK⟩ }
+    exact ⟨K, hKU, hKc, ennreal.lt_add_of_sub_lt_right (or.inl hμU) hrK⟩ }
 end
 
 lemma map {α β} [measurable_space α] [measurable_space β] {μ : measure α} {pa qa : set α → Prop}

src/topology/instances/ennreal.lean

@@ -830,7 +830,7 @@ lemma tsum_sub {f : ℕ → ℝ≥0∞} {g : ℕ → ℝ≥0∞} (h₁ : ∑' i,
   ∑' i, (f i - g i) = (∑' i, f i) - (∑' i, g i) :=
 begin
   have h₃: ∑' i, (f i - g i) = ∑' i, (f i - g i + g i) - ∑' i, g i,
-  { rw [ennreal.tsum_add, add_sub_self h₁]},
+  { rw [ennreal.tsum_add, ennreal.add_sub_cancel_right h₁]},
   have h₄:(λ i, (f i - g i) + (g i)) = f,
   { ext n, rw tsub_add_cancel_of_le (h₂ n)},
   rw h₄ at h₃, apply h₃,