internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_deg_sum_move
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (range (M.t + 1)) j, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (range (M.t + 1)) j,
        card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Tactic:
rw [← sum_erase_add ((range (M.t + 1)).erase j) _ (mem_erase_of_ne_of_mem hj.2.symm hvi.1)]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (range (M.t + 1)) j,
        card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Theorem: SimpleGraph.mp_deg_sum_move
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (range (M.t + 1)) j,
        card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Tactic:
rw [← sum_erase_add ((range (M.t + 1)).erase j) _ (mem_erase_of_ne_of_mem hj.2.symm hvi.1)]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (erase (range (M.t + 1)) j) i,
          card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
        card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Theorem: SimpleGraph.mp_deg_sum_move
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ x in erase (erase (range (M.t + 1)) j) i,
          card (MultiPart.P (move M hvi hj) x) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) x) +
        card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Tactic:
rw [mp_deg_sum_move_help2]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ y in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M y) * card (M.A \ MultiPart.P M y) +
        card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Theorem: SimpleGraph.mp_deg_sum_move
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
        card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ∑ y in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M y) * card (M.A \ MultiPart.P M y) +
        card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Tactic:
rw [add_assoc, add_assoc]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
      (card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j)) <
    ∑ y in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M y) * card (M.A \ MultiPart.P M y) +
      (card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
        card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j))
Theorem: SimpleGraph.mp_deg_sum_move
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ x in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) +
      (card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j)) <
    ∑ y in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M y) * card (M.A \ MultiPart.P M y) +
      (card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
        card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j))
Tactic:
refine' (add_lt_add_iff_left _).mpr _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Theorem: SimpleGraph.mp_deg_sum_move
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Tactic:
exact mp_deg_sum_move_help hvi hj hc
Proof state after:
no goals
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ sumSqC (move M hvi hj) < sumSqC M
Tactic:
unfold sumSqC
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Tactic:
have h3 := mp_deg_sum_move hvi hj hc
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Tactic:
have h1 := mp_deg_sum_sq' M
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
h1 : ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
h1 : ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Tactic:
have h2 := mp_deg_sum_sq' (move M hvi hj)
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
h1 : ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
h2 :
  ∑ v_1 in (move M hvi hj).A, degree (mp (move M hvi hj)) v_1 +
      ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card (move M hvi hj).A ^ 2
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
h1 : ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
h2 :
  ∑ v_1 in (move M hvi hj).A, degree (mp (move M hvi hj)) v_1 +
      ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card (move M hvi hj).A ^ 2
⊢ ∑ i_1 in range ((move M hvi hj).t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Tactic:
rw [move_a, move_t] at *
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in M.A, degree (mp (move M hvi hj)) w
h1 : ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
h2 :
  ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card M.A ^ 2
⊢ ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in M.A, degree (mp (move M hvi hj)) w
h1 : ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
h2 :
  ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card M.A ^ 2
⊢ ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Tactic:
rw [← h2] at h1
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in M.A, degree (mp (move M hvi hj)) w
h1 :
  ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2
h2 :
  ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card M.A ^ 2
⊢ ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Theorem: SimpleGraph.sumSqC_dec
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h3 : ∑ w in M.A, degree (mp M) w < ∑ w in M.A, degree (mp (move M hvi hj)) w
h1 :
  ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2
h2 :
  ∑ v_1 in M.A, degree (mp (move M hvi hj)) v_1 + ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 =
    card M.A ^ 2
⊢ ∑ i_1 in range (M.t + 1), card (MultiPart.P (move M hvi hj) i_1) ^ 2 <
    ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: SimpleGraph.moved
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∃ N, N.A = M.A ∧ N.t = M.t ∧ TuranPartition N ∧ mpDsum M ≤ mpDsum N
Tactic:
apply WellFounded.recursion (InvImage.wf sumSqC Nat.lt_wfRel.wf) M
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : MultiPart α),
    (∀ (y : MultiPart α),
        InvImage WellFoundedRelation.rel sumSqC y x →
          ∃ 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
Theorem: SimpleGraph.moved
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : MultiPart α),
    (∀ (y : MultiPart α),
        InvImage WellFoundedRelation.rel sumSqC y x →
          ∃ 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:
intro X h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ 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
Theorem: SimpleGraph.moved
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ 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:
by_cases h' : TuranPartition X
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Theorem: SimpleGraph.moved
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
exact ⟨X, rfl, rfl, h', le_rfl⟩
Proof state after:
no goals
Theorem: SimpleGraph.moved
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
obtain ⟨i, hi, j, hj, v, hv, ne, hc⟩ := not_turanPartition_imp h'
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
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)
⊢ ∃ 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 :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
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)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
set Y := move X ⟨hi, hv⟩ ⟨hj, ne⟩ with hY
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
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)
⊢ ∃ 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 :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
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)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
specialize h Y (sumSqC_dec X ⟨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 = 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