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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
⊢ M.A = N.A → M.t = N.t → TuranPartition M → ¬TuranPartition N → mpDsum N < mpDsum M
Tactic:
intro hA ht him h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
⊢ mpDsum N < mpDsum M

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
⊢ mpDsum N < mpDsum M
Tactic:
obtain ⟨i, hi, j, hj, v, hv, ne, hc⟩ := not_turanPartition_imp h1
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
⊢ mpDsum N < mpDsum M

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
⊢ mpDsum N < mpDsum M
Tactic:
set O := move N ⟨hi, hv⟩ ⟨hj, ne⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
⊢ mpDsum N < mpDsum M

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
⊢ mpDsum N < mpDsum M
Tactic:
have Ns : mpDsum N < mpDsum O := mp_deg_sum_move ⟨hi, hv⟩ ⟨hj, ne⟩ hc
State after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
⊢ mpDsum N < mpDsum M

State before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
⊢ mpDsum N < mpDsum M
Tactic:
obtain ⟨Q, QA, Qt, Qim, Qs⟩ := moved O
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
⊢ mpDsum N < mpDsum M

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
⊢ mpDsum N < mpDsum M
Tactic:
have := turanPartition_deg_sum_eq M Q
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ mpDsum N < mpDsum M

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ mpDsum N < mpDsum M
Tactic:
rw [this]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ mpDsum N < mpDsum Q

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ M.A = Q.A

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ M.t = Q.t

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ TuranPartition M

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ TuranPartition Q

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ mpDsum N < mpDsum Q
Tactic:
exact lt_of_lt_of_le Ns Qs
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ M.A = Q.A
Tactic:
rw [hA, QA]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ N.A = O.A

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ N.A = O.A
Tactic:
have NOA : N.A = O.A := move_a ⟨hi, hv⟩ ⟨hj, ne⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
NOA : N.A = O.A
⊢ N.A = O.A

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
NOA : N.A = O.A
⊢ N.A = O.A
Tactic:
exact NOA
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ M.t = Q.t
Tactic:
rw [ht, Qt]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ N.t = O.t

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ N.t = O.t
Tactic:
have NOt : N.t = O.t := move_t ⟨hi, hv⟩ ⟨hj, ne⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
NOt : N.t = O.t
⊢ N.t = O.t

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
NOt : N.t = O.t
⊢ N.t = O.t
Tactic:
exact NOt
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ TuranPartition M
Tactic:
exact him
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ TuranPartition Q
Tactic:
exact Qim
State after:
no goals