no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
⊢ Prepartition.iUnion (biUnion π πi) = ⋃ (J : Box ι) (_ : J ∈ π), Prepartition.iUnion (πi J)
simp [Prepartition.iUnion]