chore(topology/algebra/group): review (#4570)

* Ensure that we don't use `[topological_group G]` when it suffices to ask for, e.g., `[has_continuous_mul G]`.
* Introduce `[has_continuous_sub]`, add an instance for `nnreal`.

Author: urkud

src/analysis/convex/topology.lean

@@ -84,11 +84,11 @@ convex_iff_pointwise_add_subset.mpr $ λ a b ha hb hab,
   or.elim (classical.em (a = 0))
   (λ heq,
     have hne : b ≠ 0, by { rw [heq, zero_add] at hab, rw hab, exact one_ne_zero },
-    by { rw ← image_smul, apply is_open_add_left,
-         exact is_open_map_smul_of_ne_zero hne _ is_open_interior } )
+    by { rw ← image_smul,
+         exact (is_open_map_smul_of_ne_zero hne _ is_open_interior).add_left } )
   (λ hne,
-    by { rw ← image_smul, apply is_open_add_right,
-         exact is_open_map_smul_of_ne_zero hne _ is_open_interior }),
+    by { rw ← image_smul,
+         exact (is_open_map_smul_of_ne_zero hne _ is_open_interior).add_right }),
   (subset_interior_iff_subset_of_open h).mpr $ subset.trans
     (by { simp only [← image_smul], apply add_subset_add; exact image_subset _ interior_subset })
     (convex_iff_pointwise_add_subset.mp hs ha hb hab)

src/measure_theory/borel_space.lean

@@ -794,7 +794,7 @@ variable [measurable_space α]
 
 lemma measurable.sub_nnreal {f g : α → ℝ≥0} :
   measurable f → measurable g → measurable (λ a, f a - g a) :=
-nnreal.continuous_sub.measurable2
+continuous_sub.measurable2
 
 lemma measurable.nnreal_of_real {f : α → ℝ} (hf : measurable f) :
   measurable (λ x, nnreal.of_real (f x)) :=
@@ -876,7 +876,7 @@ end
 
 lemma measurable_sub : measurable (λ p : ennreal × ennreal, p.1 - p.2) :=
 by apply measurable_of_measurable_nnreal_nnreal;
-  simp [← ennreal.coe_sub, nnreal.continuous_sub.measurable.ennreal_coe]
+  simp [← ennreal.coe_sub, continuous_sub.measurable.ennreal_coe]
 
 end ennreal