Theorem: Finset.union_right_comm_assoc (FOL/Finset.lean)

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

State before:
α : Type
inst✝ : DecidableEq α
x : α
S T : Finset α
⊢ S ∪ (T ∪ {x}) = S ∪ T ∪ {x}
Tactic:
simp only [Finset.union_assoc S T {x}]
State after:
no goals