rw [(by norm_num : 2 = 1 + 1), add_mul, one_mul]
α : 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 : α
hx : x ∈ C
⊢ 2 * card M.A = 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 : α
hx : x ∈ C
⊢ card M.A + card M.A = degRes H x M.A + degRes H x M.A