no goals
α : Type u_1
β : Type ?u.186096
γ : Type ?u.186099
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂
rw [inter_comm, insert_inter_of_not_mem h, inter_comm]