simp_all only [Ne.def, not_false_iff, mem_erase, eq_self_iff_true]
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
no goals