no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁✝ π₂✝ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
π₁ π₂ : Prepartition I
⊢ J ∈ π₁ ⊓ π₂ ↔ ∃ J₁, J₁ ∈ π₁ ∧ ∃ J₂, J₂ ∈ π₂ ∧ ↑J = ↑J₁ ⊓ ↑J₂
simp only [inf_def, mem_biUnion, mem_restrict]