no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
⊢ Prepartition.iUnion (π₁ ⊓ π₂) = Prepartition.iUnion π₁ ∩ Prepartition.iUnion π₂
simp only [inf_def, iUnion_biUnion, iUnion_restrict, ← iUnion_inter, ← iUnion_def]