Theorem: SimpleGraph.mp_deg_sum_move_help (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)
⊢ 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:
rw [move_Pcard hvi hj hvi.1, move_Pcard hvi hj hj.1, move_Pcard_sdiff hvi hj hvi.1,
  move_Pcard_sdiff hvi hj 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)
⊢ 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

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

State before:
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)
Tactic:
exfalso
State after:
case pos.h
α : 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
⊢ False

State before:
case pos.h
α : 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
⊢ False
Tactic:
exact h.1 rfl
State after:
no goals

State before:
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)
Tactic:
exfalso
State after:
case pos.h
α : 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
⊢ False

State before:
case pos.h
α : 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
⊢ False
Tactic:
exact h.1 rfl
State after:
no goals

State before:
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)
Tactic:
exfalso
State after:
case neg.h
α : 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
⊢ False

State before:
case neg.h
α : 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
⊢ False
Tactic:
exact h.1 rfl
State after:
no goals

State before:
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)
Tactic:
exfalso
State after:
case pos.h
α : 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
⊢ False

State before:
case pos.h
α : 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
⊢ False
Tactic:
apply h_4.2 rfl
State after:
no goals

State before:
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)
Tactic:
exfalso
State after:
case pos.h
α : 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
⊢ False

State before:
case pos.h
α : 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
⊢ False
Tactic:
exact hj.2 h_5
State after:
no goals

State before:
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)
Tactic:
rw [card_sdiff (sub_part hvi.1)]
State after:
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 - card (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 - card (MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1)

State before:
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 - card (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 - card (MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1)
Tactic:
rw [card_sdiff (sub_part hj.1)]
State after:
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 - card (MultiPart.P M i)) +
      card (MultiPart.P M j) * (card M.A - card (MultiPart.P M j)) <
    (card (MultiPart.P M i) - 1) * (card M.A - card (MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card M.A - card (MultiPart.P M j) - 1)

State before:
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 - card (MultiPart.P M i)) +
      card (MultiPart.P M j) * (card M.A - card (MultiPart.P M j)) <
    (card (MultiPart.P M i) - 1) * (card M.A - card (MultiPart.P M i) + 1) +
      (card (MultiPart.P M j) + 1) * (card M.A - card (MultiPart.P M j) - 1)
Tactic:
exact move_change hc (two_parts hvi.1 hj.1 hj.2.symm)
State after:
no goals

State before:
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)
Tactic:
exfalso
State after:
case pos.h
α : 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
⊢ False

State before:
case pos.h
α : 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
⊢ False
Tactic:
exact h_6.2 rfl
State after:
no goals

State before:
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)
Tactic:
contradiction
State after:
no goals

State before:
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)
Tactic:
contradiction
State after:
no goals