obtain ⟨i, hi, hi2⟩ := hA
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
hA : ∃ a, a ∈ range (M.t + 1) ∧ x ∈ MultiPart.P M a
⊢ x ∈ M.A
case a.mpr.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
i : ℕ
hi : i ∈ range (M.t + 1)
hi2 : x ∈ MultiPart.P M i
⊢ x ∈ M.A