feat(algebra/order/ring): variants of mul_sub' (#9604)

Add some variants of `mul_sub'` and `sub_mul'` and use them in `ennreal`. (Also sneaking in a tiny stylistic change in `topology/ennreal`.)

src/algebra/order/ring.lean

@@ -1434,20 +1434,45 @@ lemma zero_lt_one [nontrivial α] : (0:α) < 1 := (zero_le 1).lt_of_ne zero_ne_o
 @[simp] lemma mul_pos : 0 < a * b ↔ (0 < a) ∧ (0 < b) :=
 by simp only [pos_iff_ne_zero, ne.def, mul_eq_zero, not_or_distrib]
 
-variables [has_sub α] [has_ordered_sub α] [contravariant_class α α (+) (≤)] [is_total α (≤)]
 
-lemma _root_.mul_sub' (a b c : α) : a * (b - c) = a * b - a * c :=
+end canonically_ordered_comm_semiring
+
+section sub
+
+variables [canonically_ordered_comm_semiring α] {a b c : α}
+variables [has_sub α] [has_ordered_sub α]
+
+lemma sub_mul_ge : a * c - b * c ≤ (a - b) * c :=
+by { rw [sub_le_iff_right, ← add_mul], exact mul_le_mul_right' le_sub_add c }
+
+lemma mul_sub_ge : a * b - a * c ≤ a * (b - c) :=
+by simp only [mul_comm a, sub_mul_ge]
+
+variables [is_total α (≤)]
+
+namespace add_le_cancellable
+protected lemma mul_sub (h : add_le_cancellable (a * c)) :
+  a * (b - c) = a * b - a * c :=
 begin
   cases total_of (≤) b c with hbc hcb,
   { rw [sub_eq_zero_iff_le.2 hbc, mul_zero, sub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)] },
-  { apply eq_sub_of_add_eq'',
-    rw [← mul_add, sub_add_cancel_of_le hcb] }
+  { apply h.eq_sub_of_add_eq, rw [← mul_add, sub_add_cancel_of_le hcb] }
 end
 
-lemma _root_.sub_mul' (a b c : α) : (a - b) * c = a * c - b * c :=
-by simp only [← mul_comm c, mul_sub']
+protected lemma sub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c :=
+by { simp only [mul_comm _ c] at *, exact h.mul_sub }
 
-end canonically_ordered_comm_semiring
+end add_le_cancellable
+
+variables [contravariant_class α α (+) (≤)]
+
+lemma mul_sub' (a b c : α) : a * (b - c) = a * b - a * c :=
+contravariant.add_le_cancellable.mul_sub
+
+lemma sub_mul' (a b c : α) : (a - b) * c = a * c - b * c :=
+contravariant.add_le_cancellable.sub_mul
+
+end sub
 
 /-! ### Structures involving `*` and `0` on `with_top` and `with_bot`
 

src/data/real/ennreal.lean

@@ -839,33 +839,15 @@ lemma sub_right_inj {a b c : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≤ a) (hc : c
 
 lemma sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c :=
 begin
-  cases le_or_lt a b with hab hab,
-  { simp [hab, mul_right_mono hab] },
-  symmetry,
-  cases eq_or_lt_of_le (zero_le b) with hb hb,
-  { subst b, simp },
-  apply sub_eq_of_add_eq,
-  { exact mul_ne_top (ne_top_of_lt hab) (h hb hab) },
-  rw [← add_mul, sub_add_cancel_of_le (le_of_lt hab)]
+  cases le_or_lt a b with hab hab, { simp [hab, mul_right_mono hab] },
+  rcases eq_or_lt_of_le (zero_le b) with rfl|hb, { simp },
+  exact (cancel_of_ne $ mul_ne_top hab.ne_top (h hb hab)).sub_mul
 end
 
 lemma mul_sub (h : 0 < c → c < b → a ≠ ∞) :
   a * (b - c) = a * b - a * c :=
 by { simp only [mul_comm a], exact sub_mul h }
 
-lemma sub_mul_ge : a * c - b * c ≤ (a - b) * c :=
-begin
-  -- with `0 < b → b < a → c ≠ ∞` Lean names the first variable `a`
-  by_cases h : ∀ (hb : 0 < b), b < a → c ≠ ∞,
-  { rw [sub_mul h],
-    exact le_refl _ },
-  { push_neg at h,
-    rcases h with ⟨hb, hba, hc⟩,
-    subst c,
-    simp only [mul_top, if_neg (ne_of_gt hb), if_neg (ne_of_gt $ lt_trans hb hba), sub_self,
-      zero_le] }
-end
-
 end sub
 
 section sum

src/topology/instances/ennreal.lean

@@ -481,7 +481,7 @@ supr_mul
 
 protected lemma tendsto_coe_sub : ∀{b:ℝ≥0∞}, tendsto (λb:ℝ≥0∞, ↑r - b) (𝓝 b) (𝓝 (↑r - b)) :=
 begin
-  refine (forall_ennreal.2 $ and.intro (assume a, _) _),
+  refine forall_ennreal.2 ⟨λ a, _, _⟩,
   { simp [@nhds_coe a, tendsto_map'_iff, (∘), tendsto_coe, ← with_top.coe_sub],
     exact tendsto_const_nhds.sub tendsto_id },
   simp,