Theorem: SimpleGraph.mp_deg_diff (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ degree (mp M) v = card M.A - card (MultiPart.P M i)
Tactic:
rw [mp_deg hv]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ card (M.A \ MultiPart.P M i) = card M.A - card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ card (M.A \ MultiPart.P M i) = card M.A - card (MultiPart.P M i)
Tactic:
exact card_sdiff (sub_part hv.1)
State after:
no goals