refine' mp_imp_adj hi hj1 hv hj2 _
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
⊢ Adj (mp M) v w
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
⊢ i ≠ j