no goals
α : Type u_1
β : Type ?u.184956
γ : Type ?u.184959
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
rw [inter_comm, insert_inter_of_mem h, inter_comm]