no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
h₁ : IsPartition π₁
h₂ : IsPartition π₂
⊢ Prepartition.iUnion (π₁ ⊓ π₂) = ↑I
simp [h₁.iUnion_eq, h₂.iUnion_eq]