exact ⟨i, hi, hx⟩
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
x : α
hx : x ∈ MultiPart.P M i
⊢ ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
no goals