ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J') ∈ π
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ biUnionIndex π πi J ∈ π
rw [biUnionIndex, dif_pos hJ]
no goals
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
hJ : J ∈ biUnion π πi
⊢ Exists.choose (_ : ∃ J', J' ∈ π ∧ J ∈ πi J') ∈ π
exact (π.mem_biUnion.1 hJ).choose_spec.1