internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.moved
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = Y.A ∧ N.t = Y.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
rw [move_t, move_a] at h
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Theorem: SimpleGraph.moved
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
have := mp_deg_sum_move ⟨hi, hv⟩ ⟨hj, ne⟩ hc
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this :
  ∑ w in X.A, degree (mp X) w <
    ∑ w in (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)).A,
      degree (mp (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i))) w
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Theorem: SimpleGraph.moved
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this :
  ∑ w in X.A, degree (mp X) w <
    ∑ w in (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)).A,
      degree (mp (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i))) w
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
rw [← mpDsum, ← mpDsum, ← hY] at this
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this : mpDsum X < mpDsum Y
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Theorem: SimpleGraph.moved
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this : mpDsum X < mpDsum Y
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
obtain ⟨N, h1, h2, h3, h4⟩ := h
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Theorem: SimpleGraph.moved
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
refine ⟨N, h1, h2, h3, ?_⟩
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ mpDsum X ≤ mpDsum N
Theorem: SimpleGraph.moved
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ mpDsum X ≤ mpDsum N
Tactic:
exact this.le.trans h4
Proof state after:
no goals
Theorem: SimpleGraph.moved_max
Proof 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
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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⟩
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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
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
⊢ mpDsum N < mpDsum M
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
⊢ mpDsum N < mpDsum M
Tactic:
have := turanPartition_deg_sum_eq M Q
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 M
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 Q
Tactic:
exact lt_of_lt_of_le Ns Qs
Proof state after:
no goals
Theorem: SimpleGraph.moved_max
Proof 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]
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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⟩
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.moved_max
Proof 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]
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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⟩
Proof 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
Theorem: SimpleGraph.moved_max
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.moved_max
Proof 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
Proof state after:
no goals