Theorem: SimpleGraph.sum_sdf (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in A, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C
Tactic:
nth_rw 1 [← union_sdiff_of_subset hB]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in B ∪ A \ B, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in B ∪ A \ B, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C
Tactic:
exact sum_union disjoint_sdiff
State after:
no goals