cases' hw with hA hni
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hw : w ∈ M.A ∧ ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w
case 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
hA : w ∈ M.A
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w