case pos
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ biUnion π πi
⊢ biUnionIndex π πi J ≤ I

case neg
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : ¬J ∈ biUnion π πi
⊢ biUnionIndex π πi J ≤ I
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
⊢ biUnionIndex π πi J ≤ I
by_cases hJ : J ∈ π.biUnion πi
no goals
case pos
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ biUnion π πi
⊢ biUnionIndex π πi J ≤ I
exact π.le_of_mem (π.biUnionIndex_mem hJ)
no goals
case neg
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : ¬J ∈ biUnion π πi
⊢ biUnionIndex π πi J ≤ I
rw [biUnionIndex, dif_neg hJ]