case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (J ∈ biUnion π fun J => biUnion (πi J) (πi' J)) ↔ J ∈ biUnion (biUnion π πi) fun J => πi' (biUnionIndex π πi J) J
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
⊢ (biUnion π fun J => biUnion (πi J) (πi' J)) = biUnion (biUnion π πi) fun J => πi' (biUnionIndex π πi J) J
ext J
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1) ↔
    ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (J ∈ biUnion π fun J => biUnion (πi J) (πi' J)) ↔ J ∈ biUnion (biUnion π πi) fun J => πi' (biUnionIndex π πi J) J
simp only [mem_biUnion, exists_prop]
case h.mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1) →
    ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'

case h.mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J') →
    ∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1
case h
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1) ↔
    ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
constructor
case h.mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
case h.mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1) →
    ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
rintro ⟨J₁, hJ₁, J₂, hJ₂, hJ⟩
case h.mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ J ∈ πi' (biUnionIndex π πi J₂) J₂
case h.mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ ∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J'
refine' ⟨J₂, ⟨J₁, hJ₁, hJ₂⟩, _⟩
no goals
case h.mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ₁ : J₁ ∈ π
J₂ : Box ι
hJ₂ : J₂ ∈ πi J₁
hJ : J ∈ πi' J₁ J₂
⊢ J ∈ πi' (biUnionIndex π πi J₂) J₂
rwa [π.biUnionIndex_of_mem hJ₁ hJ₂]
case h.mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (biUnionIndex π πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ ∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1
case h.mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J : Box ι
⊢ (∃ J', (∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1) ∧ J ∈ πi' (biUnionIndex π πi J') J') →
    ∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1
rintro ⟨J₁, ⟨J₂, hJ₂, hJ₁⟩, hJ⟩
case h.mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (biUnionIndex π πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ J ∈ πi' J₂ J₁
case h.mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (biUnionIndex π πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ ∃ J', J' ∈ π ∧ ∃ J'_1, J'_1 ∈ πi J' ∧ J ∈ πi' J' J'_1
refine' ⟨J₂, hJ₂, J₁, hJ₁, _⟩
no goals
case h.mpr.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
πi' : Box ι → (J : Box ι) → Prepartition J
J J₁ : Box ι
hJ : J ∈ πi' (biUnionIndex π πi J₁) J₁
J₂ : Box ι
hJ₂ : J₂ ∈ π
hJ₁ : J₁ ∈ πi J₂
⊢ J ∈ πi' J₂ J₁
rwa [π.biUnionIndex_of_mem hJ₂ hJ₁] at hJ