obtain ⟨har, b, hbr, abne, ab⟩ := ha
case intro
α : 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 : ℕ
ha :
  a ∈ range (M.t + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1) ∧
        a ≠ j ∧ (v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M a)
⊢ i ≠ j
case intro.intro.intro.intro.intro
α : 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 a ∧ w ∈ MultiPart.P M b ∨ v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j