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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (v : α), v ∈ C → degRes (mp (minsert M h)) v C = 0
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 ∈ C
⊢ degRes (mp (minsert M h)) v C = 0

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

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ nbhdRes (mp (minsert M h)) v C = ∅
Tactic:
by_contra h'
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
h' : ¬nbhdRes (mp (minsert M h)) v C = ∅
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
h' : ¬nbhdRes (mp (minsert M h)) v C = ∅
⊢ False
Tactic:
obtain ⟨w, hw, adw⟩ := (mp (minsert M h)).exists_mem_nempty h'
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
h' : ¬nbhdRes (mp (minsert M h)) v C = ∅
w : α
hw : w ∈ C
adw : Adj (mp (minsert M h)) v w
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
h' : ¬nbhdRes (mp (minsert M h)) v C = ∅
w : α
hw : w ∈ C
adw : Adj (mp (minsert M h)) v w
⊢ False
Tactic:
exact (mp_int_adj M h hv hw) adw
State after:
no goals