internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mp
α : 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
⊢ Adj (mp M) v w → Adj (mp (minsert M h)) v w
Tactic:
intro hins
Proof state after:
case mp
α : 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
hins : Adj (mp M) v w
⊢ Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mp
α : 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
hins : Adj (mp M) v w
⊢ Adj (mp (minsert M h)) v w
Tactic:
obtain ⟨k, hkr, l, hlr, lnek, lkc⟩ := hins
Proof state after:
case mp.intro.intro.intro.intro.intro
α : 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)
l : ℕ
hlr : l ∈ range (M.t + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mp.intro.intro.intro.intro.intro
α : 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)
l : ℕ
hlr : l ∈ range (M.t + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ Adj (mp (minsert M h)) v w
Tactic:
use k
Proof state after:
case 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)
l : ℕ
hlr : l ∈ range (M.t + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ k ∈ range ((minsert M h).t + 1) ∧
    ∃ j,
      j ∈ range ((minsert M h).t + 1) ∧
        k ≠ j ∧
          (v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) j ∨
            v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) k)
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case 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)
l : ℕ
hlr : l ∈ range (M.t + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ k ∈ range ((minsert M h).t + 1) ∧
    ∃ j,
      j ∈ range ((minsert M h).t + 1) ∧
        k ≠ j ∧
          (v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) j ∨
            v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) k)
Tactic:
rw [insert_t]
Proof state after:
case 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)
l : ℕ
hlr : l ∈ range (M.t + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ k ∈ range (M.t + 1 + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1 + 1) ∧
        k ≠ j ∧
          (v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) j ∨
            v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) k)
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case 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)
l : ℕ
hlr : l ∈ range (M.t + 1)
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ k ∈ range (M.t + 1 + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1 + 1) ∧
        k ≠ j ∧
          (v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) j ∨
            v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) k)
Tactic:
rw [mem_range] at *
Proof state after:
case 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ k < M.t + 1 + 1 ∧
    ∃ j,
      j ∈ range (M.t + 1 + 1) ∧
        k ≠ j ∧
          (v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) j ∨
            v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) k)
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ k < M.t + 1 + 1 ∧
    ∃ j,
      j ∈ range (M.t + 1 + 1) ∧
        k ≠ j ∧
          (v ∈ MultiPart.P (minsert M h) k ∧ w ∈ MultiPart.P (minsert M h) j ∨
            v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) k)
Tactic:
refine' ⟨hkr.trans (lt_succ_self _), l, _, lnek, _⟩
Proof state after:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ l ∈ range (M.t + 1 + 1)

case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ 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
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ l ∈ range (M.t + 1 + 1)
Tactic:
rw [mem_range]
Proof state after:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ l < M.t + 1 + 1
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ l < M.t + 1 + 1
Tactic:
exact hlr.trans (lt_succ_self _)
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ 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
Tactic:
simp [insert_P]
Proof state after:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ ((v ∈ if k = M.t + 1 then C else MultiPart.P M k) ∧ w ∈ if l = M.t + 1 then C else MultiPart.P M l) ∨
    (v ∈ if l = M.t + 1 then C else MultiPart.P M l) ∧ w ∈ if k = M.t + 1 then C else MultiPart.P M k
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case h.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
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
⊢ ((v ∈ if k = M.t + 1 then C else MultiPart.P M k) ∧ w ∈ if l = M.t + 1 then C else MultiPart.P M l) ∨
    (v ∈ if l = M.t + 1 then C else MultiPart.P M l) ∧ w ∈ if k = M.t + 1 then C else MultiPart.P M k
Tactic:
split_ifs with h_1 h_2 h_3
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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ v ∈ C ∧ w ∈ C ∨ v ∈ C ∧ w ∈ C

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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ v ∈ C ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ C

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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ v ∈ MultiPart.P M k ∧ w ∈ C ∨ v ∈ C ∧ 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : ¬l = M.t + 1
⊢ 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ v ∈ C ∧ w ∈ C ∨ v ∈ C ∧ w ∈ C
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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ False
Tactic:
rw [← h_1] at hkr
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 < k
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ 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 < k
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : l = M.t + 1
⊢ False
Tactic:
exact lt_irrefl k hkr
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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ v ∈ C ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ C
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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ False
Tactic:
rw [← h_1] at hkr
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 < k
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ 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 < k
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : k = M.t + 1
h_2 : ¬l = M.t + 1
⊢ False
Tactic:
exact lt_irrefl k hkr
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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ v ∈ MultiPart.P M k ∧ w ∈ C ∨ v ∈ C ∧ 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ 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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ False
Tactic:
rw [← h_3] at hlr
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 < M.t + 1
l : ℕ
hlr : l < l
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ 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 < M.t + 1
l : ℕ
hlr : l < l
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : l = M.t + 1
⊢ False
Tactic:
exact lt_irrefl l hlr
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 < M.t + 1
l : ℕ
hlr : l < M.t + 1
lnek : k ≠ l
lkc : v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ v ∈ MultiPart.P M l ∧ w ∈ MultiPart.P M k
h_1 : ¬k = M.t + 1
h_3 : ¬l = M.t + 1
⊢ v ∈ MultiPart.P M k ∧ w ∈ MultiPart.P M l ∨ 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 mpr
α : 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
⊢ Adj (mp (minsert M h)) v w → Adj (mp M) v w
Tactic:
intro hins
Proof state after:
case mpr
α : 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
hins : Adj (mp (minsert M h)) v w
⊢ Adj (mp M) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr
α : 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
hins : Adj (mp (minsert M h)) v w
⊢ Adj (mp M) v w
Tactic:
obtain ⟨k, hkr, l, hlr, lnek, lkc⟩ := hins
Proof state after:
case mpr.intro.intro.intro.intro.intro
α : 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 ((minsert M h).t + 1)
l : ℕ
hlr : l ∈ range ((minsert M h).t + 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
⊢ Adj (mp M) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro
α : 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 ((minsert M h).t + 1)
l : ℕ
hlr : l ∈ range ((minsert M h).t + 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
⊢ Adj (mp M) v w
Tactic:
rw [insert_t] at hkr
Proof state after:
case mpr.intro.intro.intro.intro.intro
α : 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 ((minsert M h).t + 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
⊢ Adj (mp M) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro
α : 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 ((minsert M h).t + 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
⊢ Adj (mp M) v w
Tactic:
rw [insert_t] at hlr
Proof state after:
case mpr.intro.intro.intro.intro.intro
α : 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
⊢ Adj (mp M) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
case mpr.intro.intro.intro.intro.intro
α : 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
⊢ Adj (mp M) v w
Tactic:
refine' ⟨k, _, l, _, lnek, _⟩
Proof state after:
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 ∈ 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
⊢ k ∈ range (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 ∈ 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)

case mpr.intro.intro.intro.intro.intro.refine'_3
α : 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
⊢ 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'_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 ∈ 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
⊢ k ∈ range (M.t + 1)
Tactic:
rw [mem_range] at *
Proof state after:
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
⊢ k < M.t + 1
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
⊢ k < M.t + 1
Tactic:
by_contra h'
Proof state after:
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