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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (v : α), v ∈ M.A → degRes (mp (minsert M h)) v M.A = degRes (mp M) v M.A
Tactic:
intro v hv
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
⊢ degRes (mp (minsert M h)) v M.A = degRes (mp M) v M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
⊢ degRes (mp (minsert M h)) v M.A = degRes (mp M) v M.A
Tactic:
rw [degRes]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = degRes (mp M) v M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = degRes (mp M) v M.A
Tactic:
rw [degRes]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = card (nbhdRes (mp M) v M.A)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = card (nbhdRes (mp M) v M.A)
Tactic:
rw [mp_old_nbhdRes M h v hv]
State after:
no goals