internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_1
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬k < M.t + 1
⊢ False
Tactic:
have : k = M.t + 1
Proof state after:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬k < M.t + 1
⊢ k = M.t + 1

case mpr.intro.intro.intro.intro.intro.refine'_1
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬k < M.t + 1
this : k = M.t + 1
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_1
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬k < M.t + 1
this : k = M.t + 1
⊢ False
Tactic:
cases lkc with
| inl lkc => 
  rw [this] at lkc 
  apply not_disjoint_iff.2 ⟨v, hv, insert_C M h lkc.1⟩ h
| inr lkc => 
  rw [this] at lkc ; apply not_disjoint_iff.2 ⟨w, hw, insert_C M h lkc.2⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬k < M.t + 1
⊢ k = M.t + 1
Tactic:
push_neg at h'
Proof state after:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : M.t + 1 ≤ k
⊢ k = M.t + 1
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : M.t + 1 ≤ k
⊢ k = M.t + 1
Tactic:
apply le_antisymm (le_of_lt_succ hkr) h'
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_1.inl
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l
⊢ False
Tactic:
rw [this] at lkc
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_1.inl
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ w ∈ MultiPart.P (minsert M h) l
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_1.inl
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ w ∈ MultiPart.P (minsert M h) l
⊢ False
Tactic:
apply not_disjoint_iff.2 ⟨v, hv, insert_C M h lkc.1⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_1.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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ False
Tactic:
rw [this] at lkc
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_1.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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_1.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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬k < M.t + 1
this : k = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ False
Tactic:
apply not_disjoint_iff.2 ⟨w, hw, insert_C M h lkc.2⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ l ∈ range (M.t + 1)
Tactic:
rw [mem_range] at *
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ l < M.t + 1
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ l < M.t + 1
Tactic:
by_contra h'
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬l < M.t + 1
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬l < M.t + 1
⊢ False
Tactic:
have : l = M.t + 1
Proof state after:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬l < M.t + 1
⊢ l = M.t + 1

case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬l < M.t + 1
this : l = M.t + 1
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬l < M.t + 1
this : l = M.t + 1
⊢ False
Tactic:
cases lkc with
| inl lkc => 
  rw [this] at lkc 
  apply not_disjoint_iff.2 ⟨w, hw, insert_C M h lkc.2⟩ h
| inr lkc =>   
  rw [this] at lkc 
  apply not_disjoint_iff.2 ⟨v, hv, insert_C M h lkc.1⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : ¬l < M.t + 1
⊢ l = M.t + 1
Tactic:
push_neg at h'
Proof state after:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : M.t + 1 ≤ l
⊢ l = M.t + 1
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case this
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
lkc :
  v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l ∨
    v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
h' : M.t + 1 ≤ l
⊢ l = M.t + 1
Tactic:
apply le_antisymm (le_of_lt_succ hlr) h'
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2.inl
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬l < M.t + 1
this : l = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l
⊢ False
Tactic:
rw [this] at lkc
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_2.inl
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬l < M.t + 1
this : l = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2.inl
α : 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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬l < M.t + 1
this : l = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ False
Tactic:
apply not_disjoint_iff.2 ⟨w, hw, insert_C M h lkc.2⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2.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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬l < M.t + 1
this : l = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ False
Tactic:
rw [this] at lkc
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_2.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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬l < M.t + 1
this : l = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ w ∈ MultiPart.P (minsert M h) k
⊢ False
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_2.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 < M.t + 1 + 1
l : ℕ
hlr : l < M.t + 1 + 1
lnek : k ≠ l
h' : ¬l < M.t + 1
this : l = M.t + 1
lkc : v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ w ∈ MultiPart.P (minsert M h) k
⊢ False
Tactic:
apply not_disjoint_iff.2 ⟨v, hv, insert_C M h lkc.1⟩ h
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro.refine'_3.inl
α : 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 ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) l
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
rw [insert_P, insert_P] at lkc
Proof state after:
case mpr.intro.intro.intro.intro.intro.refine'_3.inl
α : 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 k ≠ M.t + 1 then MultiPart.P M k else C) ∧ w ∈ if l ≠ M.t + 1 then MultiPart.P M l else 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 mpr.intro.intro.intro.intro.intro.refine'_3.inl
α : 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 k ≠ M.t + 1 then MultiPart.P M k else C) ∧ w ∈ if l ≠ M.t + 1 then MultiPart.P M l 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 : k ≠ M.t + 1
h_2 : l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l
⊢ 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 : k ≠ M.t + 1
h_2 : ¬l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ 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 : ¬k ≠ M.t + 1
h✝ : l ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M l
⊢ 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 : ¬k ≠ M.t + 1
h✝ : ¬l ≠ 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 : k ≠ M.t + 1
h_2 : l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
left
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 : k ≠ M.t + 1
h_2 : l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l
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 : k ≠ M.t + 1
h_2 : l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l
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 : k ≠ M.t + 1
h_2 : ¬l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ 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 : k ≠ M.t + 1
h_2 : ¬l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ 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 : k ≠ M.t + 1
h_2 : ¬l ≠ M.t + 1
lkc : v ∈ MultiPart.P M k ∧ 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 : ¬k ≠ M.t + 1
h✝ : l ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M l
⊢ 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 : ¬k ≠ M.t + 1
h✝ : l ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M l
⊢ 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 : ¬k ≠ M.t + 1
h✝ : l ≠ M.t + 1
lkc : v ∈ C ∧ w ∈ MultiPart.P M l
⊢ 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 : ¬k ≠ M.t + 1
h✝ : ¬l ≠ 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 : ¬k ≠ M.t + 1
h✝ : ¬l ≠ 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 : ¬k ≠ M.t + 1
h✝ : ¬l ≠ 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_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 ∈ MultiPart.P (minsert M h) l ∧ w ∈ MultiPart.P (minsert M h) k
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
Tactic:
rw [insert_P, insert_P] at lkc
Proof state after:
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