Theorem: Turanpartition.not_turanPartition_imp (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ¬TuranPartition M
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
rw [turanPartition_iff_not_moveable,  Moveable, Balanced] at h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h :
  ¬¬¬∀ (i : ℕ),
          i ∈ range (M.t + 1) → ∀ (j : ℕ), j ∈ range (M.t + 1) → card (MultiPart.P M i) ≤ card (MultiPart.P M j) + 1
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h :
  ¬¬¬∀ (i : ℕ),
          i ∈ range (M.t + 1) → ∀ (j : ℕ), j ∈ range (M.t + 1) → card (MultiPart.P M i) ≤ card (MultiPart.P M j) + 1
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
push_neg at h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ∃ i, i ∈ range (M.t + 1) ∧ ∃ j, j ∈ range (M.t + 1) ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ∃ i, i ∈ range (M.t + 1) ∧ ∃ j, j ∈ range (M.t + 1) ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
obtain ⟨i, hi, j, hj, hc⟩ := h
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
refine ⟨i,hi,j,hj,?_⟩
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
obtain ⟨v,hv⟩:= card_pos.1 <| pos_of_gt hc
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
have cne :=((lt_succ_self _).trans hc).ne.symm
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
refine ⟨v, hv, λ eq => ?_, hc⟩
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
eq : j = i
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
eq : j = i
⊢ False
Tactic:
rw [eq] at cne
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M i)
eq : j = i
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M i)
eq : j = i
⊢ False
Tactic:
contradiction
State after:
no goals