no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π : Prepartition I
⊢ IsPartition π ↔ Prepartition.iUnion π = ↑I
simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and_iff, Set.subset_def,
  mem_iUnion, Box.mem_coe]