internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_3.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
lkc : (v ∈ if l ≠ M.t + 1 then MultiPart.P M l else C) ∧ w ∈ if k ≠ M.t + 1 then MultiPart.P M k else C
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
split_ifs at lkc with h_1 h_2
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : ¬k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ C
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k

case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M k
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : ¬k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ C
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
right
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
exact lkc
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : ¬k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ C
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
exfalso
Proof state after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : ¬k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ C
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : l ≠ M.t + 1
h_2 : ¬k ≠ M.t + 1
lkc : v ∈ MultiPart.P M l ∧ w ∈ C
⊢ False
Tactic:
exact not_disjoint_iff.2 ⟨w, hw, lkc.2⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M k
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
exfalso
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M k
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M k
⊢ False
Tactic:
exact not_disjoint_iff.2 ⟨v, hv, lkc.1⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : ¬k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ C
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
exfalso
Proof state after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : ¬k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ C
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
k : ℕ
hkr : k ∈ range (M.t + 1 + 1)
l : ℕ
hlr : l ∈ range (M.t + 1 + 1)
lnek : k ≠ l
h_1 : ¬l ≠ M.t + 1
h✝ : ¬k ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ C
⊢ False
Tactic:
exact not_disjoint_iff.2 ⟨w, hw, lkc.2⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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 *
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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, _⟩
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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]
Proof 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✝
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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✝
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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 *
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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, _⟩
Proof 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
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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]
Proof 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✝
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof 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✝
Theorem: SimpleGraph.mp_old_nbhdRes
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_degRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_old_degRes
Proof 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]
Proof 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
Theorem: SimpleGraph.mp_old_degRes
Proof 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]
Proof 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)
Theorem: SimpleGraph.mp_old_degRes
Proof 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]
Proof state after:
no goals
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
⊢ v ∈ C → w ∈ C → ¬Adj (mp (minsert M h)) v w
Tactic:
intro hv hw
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
⊢ ¬Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
have vin := insert_P' M h v hv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
have win := insert_P' M h w hw
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
have := self_mem_range_succ (M.t + 1)
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : M.t + 1 ∈ range (M.t + 1 + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : M.t + 1 ∈ range (M.t + 1 + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
rw [← insert_t M h] at this
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
contrapose win
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win : ¬¬Adj (mp (minsert M h)) v w
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win : ¬¬Adj (mp (minsert M h)) v w
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
push_neg at win
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win :
  ∃ i,
    i ∈ range ((minsert M h).t + 1) ∧
      ∃ j,
        j ∈ range ((minsert M h).t + 1) ∧
          i ≠ j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ w ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) i)
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
Theorem: SimpleGraph.mp_int_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win :
  ∃ i,
    i ∈ range ((minsert M h).t + 1) ∧
      ∃ j,
        j ∈ range ((minsert M h).t + 1) ∧
          i ≠ j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ w ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) i)
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
exact not_nbhr_same_part this vin win
Proof state after:
no goals
Theorem: SimpleGraph.mp_int_degRes
Proof 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
Proof 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
Theorem: SimpleGraph.mp_int_degRes
Proof 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]
Proof 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
Theorem: SimpleGraph.mp_int_degRes
Proof 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]
Proof 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 = ∅
Theorem: SimpleGraph.mp_int_degRes
Proof 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'
Proof 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
Theorem: SimpleGraph.mp_int_degRes
Proof 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'
Proof 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
Theorem: SimpleGraph.mp_int_degRes
Proof 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
Proof state after:
no goals