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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
h : Disjoint A B
⊢ ∑ v in C, degRes G v (A ∪ B) = ∑ v in C, degRes G v A + ∑ v in C, degRes G v B
Tactic:
rw [← sum_add_distrib]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
h : Disjoint A B
⊢ ∑ v in C, degRes G v (A ∪ B) = ∑ x in C, (degRes G x A + degRes G x B)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
h : Disjoint A B
⊢ ∑ v in C, degRes G v (A ∪ B) = ∑ x in C, (degRes G x A + degRes G x B)
Tactic:
exact sum_congr rfl fun _ _ => G.degRes_add' h
State after:
no goals