no goals
α : Type u_1
β : Type ?u.147908
γ : Type ?u.147911
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ v : Finset α
a b : α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t
simp only [mem_union, or_assoc, @or_comm (x ∈ t)]