rw [← card_union_of_disjoint, ← union_inter_distrib_right]
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ ((s ∪ t) ∩ G.neighborFinset a).card = (s ∩ G.neighborFinset a).card + (t ∩ G.neighborFinset a).card
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ Disjoint (s ∩ G.neighborFinset a) (t ∩ G.neighborFinset a)