rw [←add_assoc, card_eq_sum_ones C, mul_sum]
α : 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)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + (∑ v in M.A, degRes H v C + ∑ v in C, degRes H v 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)
⊢ ∑ v in M.A, degRes (mp M) v M.A + ∑ x in C, 2 * card M.A * 1 =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A