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₂`.
