set H : SimpleGraph α := mp (minsert M h) with hH
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).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 + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A