no goals
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
⊢ J ∈ infPrepartition π₁ π₂.toPrepartition ↔ J ∈ infPrepartition π₂ π₁.toPrepartition
simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]