Theorem: SimpleGraph.mp_old_nbhdRes (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 → nbhdRes (mp (minsert M h)) v M.A = nbhdRes (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
⊢ nbhdRes (mp (minsert M h)) v M.A = 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
⊢ nbhdRes (mp (minsert M h)) v M.A = nbhdRes (mp M) v M.A
Tactic:
ext
State after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A ↔ a✝ ∈ nbhdRes (mp M) v M.A

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A ↔ a✝ ∈ nbhdRes (mp M) v M.A
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A → a✝ ∈ nbhdRes (mp M) v M.A

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp M) v M.A → a✝ ∈ nbhdRes (mp (minsert M h)) v M.A

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A → a✝ ∈ nbhdRes (mp M) v M.A
Tactic:
intro ha
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ nbhdRes (mp (minsert M h)) v M.A
⊢ a✝ ∈ nbhdRes (mp M) v M.A

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ nbhdRes (mp (minsert M h)) v M.A
⊢ a✝ ∈ nbhdRes (mp M) v M.A
Tactic:
rw [mem_res_nbhd_iff] at *
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
⊢ a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
⊢ a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
Tactic:
refine' ⟨ha.1, _⟩
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
⊢ a✝ ∈ neighborFinset (mp M) v

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
⊢ a✝ ∈ neighborFinset (mp M) v
Tactic:
rw [mem_neighborFinset]
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
⊢ Adj (mp M) v a✝

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
⊢ Adj (mp M) v a✝
Tactic:
rw [mem_neighborFinset] at ha
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ Adj (mp (minsert M h)) v a✝
⊢ Adj (mp M) v a✝

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ Adj (mp (minsert M h)) v a✝
⊢ Adj (mp M) v a✝
Tactic:
exact (mp_old_adj M h hv ha.1).mpr ha.2
State after:
no goals

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
⊢ a✝ ∈ nbhdRes (mp M) v M.A → a✝ ∈ nbhdRes (mp (minsert M h)) v M.A
Tactic:
intro ha
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ nbhdRes (mp M) v M.A
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ nbhdRes (mp M) v M.A
⊢ a✝ ∈ nbhdRes (mp (minsert M h)) v M.A
Tactic:
rw [mem_res_nbhd_iff] at *
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp (minsert M h)) v
Tactic:
refine' ⟨ha.1, _⟩
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ a✝ ∈ neighborFinset (mp (minsert M h)) v

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ a✝ ∈ neighborFinset (mp (minsert M h)) v
Tactic:
rw [mem_neighborFinset]
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ Adj (mp (minsert M h)) v a✝

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ a✝ ∈ neighborFinset (mp M) v
⊢ Adj (mp (minsert M h)) v a✝
Tactic:
rw [mem_neighborFinset] at ha
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ Adj (mp M) v a✝
⊢ Adj (mp (minsert M h)) v a✝

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ M.A
a✝ : α
ha : a✝ ∈ M.A ∧ Adj (mp M) v a✝
⊢ Adj (mp (minsert M h)) v a✝
Tactic:
exact (mp_old_adj M h hv ha.1).mp ha.2
State after:
no goals