rw [eq] at cne
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
eq : j = i
⊢ False
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M i)
eq : j = i
⊢ False