rw [union_comm (Set.pureIf a₁ p₁) (Set.pureIf a₂ p₂)]
α : Sort u_1
p₁ p₂ : Prop
a₁ a₂ : α
s : Set α
⊢ ((Set.pureIf a₂ p₂).union (Set.pureIf a₁ p₁)).union s = ((Set.pureIf a₁ p₁).union (Set.pureIf a₂ p₂)).union s
no goals