Theorem: SimpleGraph.mp_deg_sum_move_help
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) <
    ((if i ≠ i ∧ i ≠ j then card (MultiPart.P M i)
        else if i = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
        if i ≠ i ∧ i ≠ j then card (M.A \ MultiPart.P M i)
        else if i = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1) +
      (if j ≠ i ∧ j ≠ j then card (MultiPart.P M j)
        else if j = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
        if j ≠ i ∧ j ≠ j then card (M.A \ MultiPart.P M j)
        else if j = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Tactic:
split_ifs with h h_1 h_2 h_3 h_4 h_5 h_6 h_7
Proof state after:
case pos
α : 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)
h : i ≠ i ∧ i ≠ j
h_1 : j ≠ i ∧ j ≠ j
⊢ 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 M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j)

case pos
α : 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)
h : i ≠ i ∧ i ≠ j
h_1 : ¬(j ≠ i ∧ j ≠ j)
h_2 : j = 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 M i) * card (M.A \ MultiPart.P M i) +
      (card (MultiPart.P M i) - 1) * (card (M.A \ MultiPart.P M i) + 1)

case neg
α : 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)
h : i ≠ i ∧ i ≠ j
h_1 : ¬(j ≠ i ∧ j ≠ j)
h_2 : ¬j = 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 M i) * card (M.A \ MultiPart.P M i) +
      (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1)

case pos
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : i = i
h_4 : j ≠ i ∧ j ≠ j
⊢ 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 M i) - 1) * (card (M.A \ MultiPart.P M i) + 1) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j)

case pos
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : i = i
h_4 : ¬(j ≠ i ∧ j ≠ j)
h_5 : j = 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 M i) - 1) * (card (M.A \ MultiPart.P M i) + 1) +
      (card (MultiPart.P M i) - 1) * (card (M.A \ MultiPart.P M i) + 1)

case neg
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : i = i
h_4 : ¬(j ≠ i ∧ j ≠ j)
h_5 : ¬j = 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 M i) - 1) * (card (M.A \ MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1)

case pos
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : ¬i = i
h_6 : j ≠ i ∧ j ≠ j
⊢ 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 M j) + 1) * (card (M.A \ MultiPart.P M j) - 1) +
      card (MultiPart.P M j) * card (M.A \ MultiPart.P M j)

case pos
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : ¬i = i
h_6 : ¬(j ≠ i ∧ j ≠ j)
h_7 : j = 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 M j) + 1) * (card (M.A \ MultiPart.P M j) - 1) +
      (card (MultiPart.P M i) - 1) * (card (M.A \ MultiPart.P M i) + 1)

case neg
α : 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)
h : ¬(i ≠ i ∧ i ≠ j)
h_3 : ¬i = i
h_6 : ¬(j ≠ i ∧ j ≠ j)
h_7 : ¬j = 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 M j) + 1) * (card (M.A \ MultiPart.P M j) - 1) +
      (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1)