chore(measure_theory): golf (#14657)

Also use `@measurable_set α m s` instead of `m.measurable_set' s` in the definition of the partial order on `measurable_space`. This way we can use dot notation lemmas about measurable sets in a proof of `m₁ ≤ m₂`.

src/measure_theory/measurable_space_def.lean

@@ -219,6 +219,8 @@ lemma nonempty_measurable_superset (s : set α) : nonempty { t // s ⊆ t ∧ me
 
 end
 
+open_locale measure_theory
+
 @[ext] lemma measurable_space.ext : ∀ {m₁ m₂ : measurable_space α},
   (∀ s : set α, m₁.measurable_set' s ↔ m₂.measurable_set' s) → m₁ = m₂
 | ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
@@ -276,16 +278,15 @@ namespace measurable_space
 section complete_lattice
 
 instance : has_le (measurable_space α) :=
-{ le          := λ m₁ m₂, m₁.measurable_set' ≤ m₂.measurable_set' }
+{ le          := λ m₁ m₂, ∀ s, measurable_set[m₁] s → measurable_set[m₂] s }
 
 lemma le_def {α} {a b : measurable_space α} :
   a ≤ b ↔ a.measurable_set' ≤ b.measurable_set' := iff.rfl
 
 instance : partial_order (measurable_space α) :=
-{ le_refl     := assume a b, le_rfl,
-  le_trans    := assume a b c hab hbc, le_def.mpr (le_trans hab hbc),
-  le_antisymm := assume a b h₁ h₂, measurable_space.ext $ assume s, ⟨h₁ s, h₂ s⟩,
-  ..measurable_space.has_le }
+{ lt := λ m₁ m₂, m₁ ≤ m₂ ∧ ¬m₂ ≤ m₁,
+  .. measurable_space.has_le,
+  .. partial_order.lift (@measurable_space.measurable_set' α) (λ m₁ m₂ h, ext $ λ s, h ▸ iff.rfl) }
 
 /-- The smallest σ-algebra containing a collection `s` of basic sets -/
 inductive generate_measurable (s : set (set α)) : set α → Prop
@@ -399,10 +400,8 @@ by simp only [supr, measurable_set_Sup, exists_range_iff]
 
 end complete_lattice
 
-
 end measurable_space
 
-
 section measurable_functions
 open measurable_space
 

src/measure_theory/measure/measure_space_def.lean

@@ -268,9 +268,8 @@ not_iff_not.1 $ by simp only [← lt_top_iff_ne_top, ← ne.def, not_or_distrib,
 lemma exists_measure_pos_of_not_measure_Union_null [encodable β] {s : β → set α}
   (hs : μ (⋃ n, s n) ≠ 0) : ∃ n, 0 < μ (s n) :=
 begin
-  by_contra' h,
-  simp_rw nonpos_iff_eq_zero at h,
-  exact hs (measure_Union_null h),
+  contrapose! hs,
+  exact measure_Union_null (λ n, nonpos_iff_eq_zero.1 (hs n))
 end
 
 lemma measure_inter_lt_top_of_left_ne_top (hs_finite : μ s ≠ ∞) : μ (s ∩ t) < ∞ :=
@@ -325,9 +324,8 @@ eventually_of_forall
 instance : countable_Inter_filter μ.ae :=
 ⟨begin
   intros S hSc hS,
-  simp only [mem_ae_iff, compl_sInter, sUnion_image, bUnion_eq_Union] at hS ⊢,
-  haveI := hSc.to_encodable,
-  exact measure_Union_null (subtype.forall.2 hS)
+  rw [mem_ae_iff, compl_sInter, sUnion_image],
+  exact (measure_bUnion_null_iff hSc).2 hS
 end⟩
 
 lemma ae_imp_iff {p : α → Prop} {q : Prop} : (∀ᵐ x ∂μ, q → p x) ↔ (q → ∀ᵐ x ∂μ, p x) :=