no goals
α : Type u_1
β : Type ?u.10509
γ : Type ?u.10512
δ : Type ?u.10515
δ' : Type ?u.10518
ι : Sort ?u.10521
s t u : Set α
m : MeasurableSpace α
p : Prop
⊢ MeasurableSet {_a | p}
by_cases p <;> simp [*]