rw [mp_com M h x hx]
α : 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
no goals