rw [M.uni]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ M.A
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
M : MultiPart α
hi : i ∈ range (M.t + 1)
⊢ MultiPart.P M i ⊆ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i