Theorem: SimpleGraph.moved_max
Proof 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]
Proof 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