ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), J ∈ biUnionTagged π πi → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
simp only [mem_biUnionTagged]
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'

case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
refine' ⟨fun H J hJ J' hJ' => _, fun H J' ⟨J, hJ, hJ'⟩ => _⟩
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
rw [← π.tag_biUnionTagged hJ hJ']
no goals
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
exact H J' ⟨J, hJ, hJ'⟩
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
rw [π.tag_biUnionTagged hJ hJ']
no goals
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
exact H J hJ J' hJ'