Theorem: Turanpartition.move_Pcard (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
⊢ k ∈ range (M.t + 1) →
    card (MultiPart.P (move M hvi hj) k) =
      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
Tactic:
intro hk
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card (MultiPart.P (move M hvi hj) k) =
    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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card (MultiPart.P (move M hvi hj) k) =
    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
Tactic:
rw [move_p hvi hj hk]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card
      (if k ≠ i ∧ k ≠ j then MultiPart.P M k
      else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
⊢ card
      (if k ≠ i ∧ k ≠ j then MultiPart.P M k
      else if k = i then erase (MultiPart.P M i) v else insert v (MultiPart.P M j)) =
    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
Tactic:
split_ifs with h h_1
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : k ≠ i ∧ k ≠ j
⊢ card (MultiPart.P M k) = card (MultiPart.P M k)

case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ card (erase (MultiPart.P M i) v) = card (MultiPart.P M i) - 1

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ card (insert v (MultiPart.P M j)) = card (MultiPart.P M j) + 1

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : k ≠ i ∧ k ≠ j
⊢ card (MultiPart.P M k) = card (MultiPart.P M k)
Tactic:
rfl
State after:
no goals

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : k = i
⊢ card (erase (MultiPart.P M i) v) = card (MultiPart.P M i) - 1
Tactic:
exact card_erase_of_mem hvi.2
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j k : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hk : k ∈ range (M.t + 1)
h : ¬(k ≠ i ∧ k ≠ j)
h_1 : ¬k = i
⊢ card (insert v (MultiPart.P M j)) = card (MultiPart.P M j) + 1
Tactic:
apply card_insert_of_not_mem (uniq_part' hvi.1 hj.1 hj.2.symm hvi.2)
State after:
no goals