no goals
α : Type u_1
β : Type ?u.150066
γ : Type ?u.150069
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ s ∪ insert a t = insert a (s ∪ t)
simp only [insert_eq, union_left_comm]