exact (sub_part hj) hv.1
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A
no goals