no goals
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : x ∈ ↑Box.Icc I
⊢ (∀ (J' : Box ι), J' ∈ single I J hJ x h → p (tag (single I J hJ x h) J') J') ↔ p x J
simp