Theorem: SimpleGraph.degRes_add' (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ degRes G v (A ∪ B) = degRes G v A + degRes G v B
Tactic:
rw [degRes, nbhdRes,inter_distrib_right]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ card (A ∩ neighborFinset G v ∪ B ∩ neighborFinset G v) = degRes G v A + degRes G v B

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ card (A ∩ neighborFinset G v ∪ B ∩ neighborFinset G v) = degRes G v A + degRes G v B
Tactic:
exact card_disjoint_union (disj_of_inter_disj _ _ h)
State after:
no goals