no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ J₁ ∈ restrict π J ↔ ∃ J', J' ∈ π ∧ ↑J₁ = ↑J ∩ ↑J'
simp only [mem_restrict, ← Box.withBotCoe_inj, Box.coe_inf, Box.coe_coe]