Theorem: SimpleGraph.mp_deg_sum_move (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)
⊢ ∑ w in M.A, degree (mp M) w < ∑ w in (move M hvi hj).A, degree (mp (move M hvi hj)) w
Tactic:
rw [mp_deg_sum M, mp_deg_sum (move M hvi hj), move_t 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)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) <
    ∑ i_1 in range (M.t + 1),
      card (MultiPart.P (move M hvi hj) i_1) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i_1)

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 in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) <
    ∑ i_1 in range (M.t + 1),
      card (MultiPart.P (move M hvi hj) i_1) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i_1)
Tactic:
rw [← sum_erase_add (range (M.t + 1)) _ hj.1, ← sum_erase_add (range (M.t + 1)) _ hj.1]
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 (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)

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

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

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

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

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

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