intro hi hv
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
⊢ i ∈ range (M.t + 1) → v ∈ MultiPart.P M i → v ∈ M.A
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
⊢ v ∈ M.A