refine' ⟨nbhrs_imp h, _⟩
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A ∧ ¬a✝ ∈ MultiPart.P M i
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ ¬a✝ ∈ MultiPart.P M i