internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof 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
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof 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
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof 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
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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)]
Proof 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)
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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)]
Proof 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)
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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)
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof 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
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help2
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
⊢ ∑ 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) =
    ∑ y in erase (erase (range (M.t + 1)) j) i, card (MultiPart.P M y) * card (M.A \ MultiPart.P M y)
Tactic:
apply sum_congr rfl _
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
⊢ ∀ (x : ℕ),
    x ∈ 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 M x) * card (M.A \ MultiPart.P M x)
Theorem: SimpleGraph.mp_deg_sum_move_help2
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
⊢ ∀ (x : ℕ),
    x ∈ 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 M x) * card (M.A \ MultiPart.P M x)
Tactic:
intro k hk
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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ card (MultiPart.P (move M hvi hj) k) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)
Theorem: SimpleGraph.mp_deg_sum_move_help2
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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ card (MultiPart.P (move M hvi hj) k) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)
Tactic:
rw [move_Pcard 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ (if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
      card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)
Theorem: SimpleGraph.mp_deg_sum_move_help2
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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ (if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
      card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) k) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)
Tactic:
rw [move_Pcard_sdiff 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ ((if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
      if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
      else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)
Theorem: SimpleGraph.mp_deg_sum_move_help2
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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ ((if k ≠ i ∧ k ≠ j then card (MultiPart.P M k)
      else if k = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
      if k ≠ i ∧ k ≠ j then card (M.A \ MultiPart.P M k)
      else if k = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)
Tactic:
split_ifs with h h_1
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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : k ≠ i ∧ k ≠ j
⊢ card (MultiPart.P M k) * card (M.A \ MultiPart.P M k) = card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ (card (MultiPart.P M i) - 1) * (card (M.A \ MultiPart.P M i) + 1) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)

α : 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : k ≠ i ∧ k ≠ j
⊢ card (MultiPart.P M k) * card (M.A \ MultiPart.P M k) = card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ (card (MultiPart.P M i) - 1) * (card (M.A \ MultiPart.P M i) + 1) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)
Tactic:
exfalso
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ False
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ False
Tactic:
rw [h_1] at hk
Proof 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
k : ℕ
hk : i ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ False
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : i ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ False
Tactic:
exact not_mem_erase i _ hk
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ (card (MultiPart.P M j) + 1) * (card (M.A \ MultiPart.P M j) - 1) =
    card (MultiPart.P M k) * card (M.A \ MultiPart.P M k)
Tactic:
exfalso
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ False
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ False
Tactic:
push_neg at h
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h_1 : ¬k = i
h : k ≠ i → k = j
⊢ False
Theorem: SimpleGraph.mp_deg_sum_move_help2
Proof 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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
h_1 : ¬k = i
h : k ≠ i → k = j
⊢ False
Tactic:
simp_all only [Ne.def, not_false_iff, mem_erase, eq_self_iff_true]
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help2
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
k : ℕ
hk : k ∈ erase (erase (range (M.t + 1)) j) i
⊢ k ∈ range (M.t + 1)
Tactic:
exact mem_of_mem_erase (mem_of_mem_erase hk)
Proof state after:
no goals
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)
⊢ ∑ 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]
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 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)
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)
⊢ ∑ 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]
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 (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)