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

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
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

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
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

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
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

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)
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

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 *
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

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
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

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
State after:
no goals