rw [mem_biUnion] at hA
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 ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
hni : ¬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 : ∃ a, a ∈ range (M.t + 1) ∧ w ∈ MultiPart.P M a
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w