case h
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
J✝ : Box ι
⊢ (J✝ ∈ biUnion π fun x => ⊤) ↔ J✝ ∈ π
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
⊢ (biUnion π fun x => ⊤) = π
ext
no goals
case h
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
J✝ : Box ι
⊢ (J✝ ∈ biUnion π fun x => ⊤) ↔ J✝ ∈ π
simp