Theorem: SimpleGraph.mp_deg_sum_move_help2 (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
⊢ ∑ 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 _
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)

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

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

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

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

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

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

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

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

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

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