chore(measure_theory/function/strongly_measurable): golf some proofs (#…

…14209)

src/measure_theory/function/strongly_measurable.lean

@@ -744,46 +744,26 @@ lemma measurable_set_eq_fun {m : measurable_space α} {E} [topological_space E]
   {f g : α → E} (hf : strongly_measurable f) (hg : strongly_measurable g) :
   measurable_set {x | f x = g x} :=
 begin
-  letI := metrizable_space_metric E,
-  have : {x | f x = g x} = {x | dist (f x) (g x) = 0}, by { ext x, simp },
-  rw this,
-  exact (hf.dist hg).measurable (measurable_set_singleton (0 : ℝ)),
+  borelize E × E,
+  exact (hf.prod_mk hg).measurable is_closed_diagonal.measurable_set
 end
 
 lemma measurable_set_lt {m : measurable_space α} [topological_space β]
   [linear_order β] [order_closed_topology β] [metrizable_space β]
   {f g : α → β} (hf : strongly_measurable f) (hg : strongly_measurable g) :
   measurable_set {a | f a < g a} :=
 begin
-  letI := metrizable_space_metric β,
-  let β' : Type* := (range f ∪ range g : set β),
-  haveI : second_countable_topology β',
-  { suffices : separable_space (range f ∪ range g : set β),
-      by exactI uniform_space.second_countable_of_separable _,
-    apply (hf.is_separable_range.union hg.is_separable_range).separable_space },
-  let f' : α → β' := cod_restrict f _ (by simp),
-  let g' : α → β' := cod_restrict g _ (by simp),
-  change measurable_set {a | f' a < g' a},
-  borelize β,
-  exact measurable_set_lt hf.measurable.subtype_mk hg.measurable.subtype_mk,
+  borelize β × β,
+  exact (hf.prod_mk hg).measurable is_open_lt_prod.measurable_set
 end
 
 lemma measurable_set_le {m : measurable_space α} [topological_space β]
-  [linear_order β] [order_closed_topology β] [metrizable_space β]
+  [preorder β] [order_closed_topology β] [metrizable_space β]
   {f g : α → β} (hf : strongly_measurable f) (hg : strongly_measurable g) :
   measurable_set {a | f a ≤ g a} :=
 begin
-  letI := metrizable_space_metric β,
-  let β' : Type* := (range f ∪ range g : set β),
-  haveI : second_countable_topology β',
-  { suffices : separable_space (range f ∪ range g : set β),
-      by exactI uniform_space.second_countable_of_separable _,
-    apply (hf.is_separable_range.union hg.is_separable_range).separable_space },
-  let f' : α → β' := cod_restrict f _ (by simp),
-  let g' : α → β' := cod_restrict g _ (by simp),
-  change measurable_set {a | f' a ≤ g' a},
-  borelize β,
-  exact measurable_set_le hf.measurable.subtype_mk hg.measurable.subtype_mk,
+  borelize β × β,
+  exact (hf.prod_mk hg).measurable is_closed_le_prod.measurable_set
 end
 
 end strongly_measurable