Theorem: Turanpartition.move_p (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) →
    MultiPart.P (move M hvi hj) k =
      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)
Tactic:
intro _
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
a✝ : k ∈ range (M.t + 1)
⊢ MultiPart.P (move M hvi hj) k =
    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)

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
a✝ : k ∈ range (M.t + 1)
⊢ MultiPart.P (move M hvi hj) k =
    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)
Tactic:
rfl
State after:
no goals