no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h : Disjoint (Prepartition.iUnion π₁) (Prepartition.iUnion π₂)
⊢ Prepartition.iUnion (disjUnion π₁ π₂ h) = Prepartition.iUnion π₁ ∪ Prepartition.iUnion π₂
simp [disjUnion, Prepartition.iUnion, iUnion_or, iUnion_union_distrib]