simp only [Finset.union_right_comm S {x} T]
α : Type
inst✝ : DecidableEq α
x : α
S T : Finset α
⊢ S ∪ (T ∪ {x}) = S ∪ {x} ∪ T
α : Type
inst✝ : DecidableEq α
x : α
S T : Finset α
⊢ S ∪ (T ∪ {x}) = S ∪ T ∪ {x}