no goals
α : Type u_1
β : Type ?u.263829
γ : Type ?u.263832
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t
simp_rw [insert_eq, union_distrib_left]