exact card_disjoint_union (sdiff_inter_disj A B _)
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (B ∩ neighborFinset G v ∪ A \ B ∩ neighborFinset G v) =
    card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
no goals