have bi := uniq_part hi hbr hvi ab.1
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
⊢ i ≠ j
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j