no goals
α : Type u_1
β : Type ?u.13146
γ : Type ?u.13149
δ : Type ?u.13152
δ' : Type ?u.13155
ι : Sort ?u.13158
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet s
rwa [← insert_eq_of_mem ha]