ext x
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ M.A = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : α
⊢ x ∈ M.A ↔ x ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i