apply sum_congr rfl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ x in C, (degRes H x M.A + degRes H x M.A)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∀ (x : α), x ∈ C → 2 * card M.A = degRes H x M.A + degRes H x M.A