exact hjm
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j ≠ M.t + 1
⊢ a ∈ MultiPart.P M j
no goals