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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
⊢ v ∈ M.A → w ∈ M.A → (Adj (mp M) v w ↔ Adj (mp (minsert M h)) v w)
Tactic:
intro hv hw
State after:
α : 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

State before:
α : 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:
constructor
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
⊢ Adj (mp M) v w → Adj (mp (minsert M h)) v w

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

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
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

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
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

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
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)

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]
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)

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 *
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)

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, _⟩
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

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]
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

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 _)
State after:
no goals

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]
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
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

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
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

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, _⟩
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

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 *
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

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'
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

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
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

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
State after:
no goals

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'
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

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'
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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 *
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

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'
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

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
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

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
State after:
no goals

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'
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

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'
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals