no goals
α : Type u_1
β : Type ?u.150533
γ : Type ?u.150536
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ insert a (s ∪ t) = insert a s ∪ insert a t
simp only [insert_union, union_insert, insert_idem]