chore(measure_theory/function/strongly_measurable): remove useless no…

…_zero_divisors assumption (#12353)

src/algebra/support.lean

@@ -189,6 +189,14 @@ mul_support_binop_subset (/) (by simp only [div_one]) f g
   support (λ x, f x * g x) = support f ∩ support g :=
 set.ext $ λ x, by simp only [mem_support, mul_ne_zero_iff, mem_inter_eq, not_or_distrib]
 
+@[simp] lemma support_mul_subset_left [mul_zero_class R] (f g : α → R) :
+  support (λ x, f x * g x) ⊆ support f :=
+λ x hfg hf, hfg $ by simp only [hf, zero_mul]
+
+@[simp] lemma support_mul_subset_right [mul_zero_class R] (f g : α → R) :
+  support (λ x, f x * g x) ⊆ support g :=
+λ x hfg hg, hfg $ by simp only [hg, mul_zero]
+
 lemma support_smul_subset_right [add_monoid A] [monoid B] [distrib_mul_action B A]
   (b : B) (f : α → A) :
   support (b • f) ⊆ support f :=

src/measure_theory/function/strongly_measurable.lean

@@ -349,15 +349,13 @@ hf.strongly_measurable.measurable_ennreal
 section arithmetic
 variables [topological_space β]
 
-protected lemma mul [monoid_with_zero β] [no_zero_divisors β] [has_continuous_mul β]
+protected lemma mul [monoid_with_zero β] [has_continuous_mul β]
   (hf : fin_strongly_measurable f μ) (hg : fin_strongly_measurable g μ) :
   fin_strongly_measurable (f * g) μ :=
 begin
   refine ⟨λ n, hf.approx n * hg.approx n, _, λ x, (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩,
   intro n,
-  rw (_ : support ⇑(hf.approx n * hg.approx n) = support (hf.approx n) ∩ support (hg.approx n)),
-  { exact measure_inter_lt_top_of_left_ne_top (hf.fin_support_approx n).ne,},
-  { exact function.support_mul _ _, },
+  exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n),
 end
 
 protected lemma add [add_monoid β] [has_continuous_add β]
@@ -469,7 +467,7 @@ end mk
 
 section arithmetic
 
-protected lemma mul [monoid_with_zero β] [no_zero_divisors β] [has_continuous_mul β]
+protected lemma mul [monoid_with_zero β] [has_continuous_mul β]
   (hf : ae_fin_strongly_measurable f μ) (hg : ae_fin_strongly_measurable g μ) :
   ae_fin_strongly_measurable (f * g) μ :=
 ⟨hf.mk f * hg.mk g, hf.fin_strongly_measurable_mk.mul hg.fin_strongly_measurable_mk,