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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (v : α), v ∈ C → degRes (mp (minsert M h)) v M.A = card M.A
Tactic:
intro v hv
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ degRes (mp (minsert M h)) v M.A = card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ degRes (mp (minsert M h)) v M.A = card M.A
Tactic:
rw [degRes]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = card M.A
Tactic:
congr
State after:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ nbhdRes (mp (minsert M h)) v M.A = M.A

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

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

State before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A ∧ a ∈ neighborFinset (mp (minsert M h)) v ↔ a ∈ M.A
Tactic:
simp only [mem_neighborFinset, mem_range, Ne.def, exists_prop, and_iff_left_iff_imp]
State after:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A →
    ∃ i,
      i < (minsert M h).t + 1 ∧
        ∃ j,
          j < (minsert M h).t + 1 ∧
            ¬i = j ∧
              (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
                v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)

State before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A →
    ∃ i,
      i < (minsert M h).t + 1 ∧
        ∃ j,
          j < (minsert M h).t + 1 ∧
            ¬i = j ∧
              (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
                v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Tactic:
intro ha
State after:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)

State before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Tactic:
obtain ⟨j, hjr, hjm⟩ := inv_part ha
State after:
case e_s.a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)

State before:
case e_s.a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Tactic:
use j
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < (minsert M h).t + 1 ∧
    ∃ j_1,
      j_1 < (minsert M h).t + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < (minsert M h).t + 1 ∧
    ∃ j_1,
      j_1 < (minsert M h).t + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
Tactic:
rw [insert_t]
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1 ∧
    ∃ j_1,
      j_1 < M.t + 1 + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1 ∧
    ∃ j_1,
      j_1 < M.t + 1 + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
Tactic:
refine' ⟨_, _, _, _, _⟩
State after:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1

case h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ℕ

case h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ?h.refine'_2 < M.t + 1 + 1

case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ¬j = ?h.refine'_2

case h.refine'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) ?h.refine'_2 ∨
    v ∈ MultiPart.P (minsert M h) ?h.refine'_2 ∧ a ∈ MultiPart.P (minsert M h) j

State before:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1
Tactic:
rw [mem_range] at *
State after:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j < M.t + 1
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1

State before:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j < M.t + 1
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1
Tactic:
apply hjr.trans (lt_succ_self _)
State after:
no goals

State before:
case h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ℕ
Tactic:
exact M.t + 1
State after:
no goals

State before:
case h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ M.t + 1 < M.t + 1 + 1
Tactic:
exact lt_succ_self _
State after:
no goals

State before:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ¬j = M.t + 1
Tactic:
intro eq
State after:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False

State before:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False
Tactic:
rw [eq] at hjr
State after:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False

State before:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False
Tactic:
exact not_mem_range_self hjr
State after:
no goals

State before:
case h.refine'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) (M.t + 1) ∨
    v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j
Tactic:
right
State after:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j

State before:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j
Tactic:
rw [insert_P]
State after:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ (v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else C) ∧ a ∈ MultiPart.P (minsert M h) j

State before:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ (v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else C) ∧ a ∈ MultiPart.P (minsert M h) j
Tactic:
split_ifs with h
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h✝) j

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ MultiPart.P (minsert M h✝) j

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h✝) j
Tactic:
exfalso
State after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ False

State before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ False
Tactic:
exact h rfl
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ MultiPart.P (minsert M h✝) j
Tactic:
rw [insert_P]
State after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C
Tactic:
refine' ⟨hv, _⟩
State after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C
Tactic:
split_ifs with h_2
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j ≠ M.t + 1
⊢ a ∈ MultiPart.P M j

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : ¬j ≠ M.t + 1
⊢ a ∈ C

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j ≠ M.t + 1
⊢ a ∈ MultiPart.P M j
Tactic:
exact hjm
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : ¬j ≠ M.t + 1
⊢ a ∈ C
Tactic:
push_neg at h_2
State after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ a ∈ C

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ a ∈ C
Tactic:
exfalso
State after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False

State before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False
Tactic:
rw [h_2] at hjr
State after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False

State before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False
Tactic:
exact not_mem_range_self hjr
State after:
no goals