case refine'_1
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ (restrict (biUnion π πi) J).boxes

case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ Prepartition.iUnion (restrict (biUnion π πi) J) ⊆ Prepartition.iUnion (πi J)
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ restrict (biUnion π πi) J = πi J
refine' (eq_of_boxes_subset_iUnion_superset (fun J₁ h₁ => _) _).symm
case refine'_1
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ ↑J₁ ≤ ↑J
case refine'_1
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ J₁ ∈ (restrict (biUnion π πi) J).boxes
refine' (mem_restrict _).2 ⟨J₁, π.mem_biUnion.2 ⟨J, hJ, h₁⟩, (inf_of_le_right _).symm⟩
no goals
case refine'_1
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ (πi J).boxes
⊢ ↑J₁ ≤ ↑J
exact WithBot.coe_le_coe.2 (le_of_mem _ h₁)
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ∀ (x : ι → ℝ), (x ∈ ↑J ∧ ∃ i i_1, x ∈ Prepartition.iUnion (πi i)) → x ∈ Prepartition.iUnion (πi J)
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ Prepartition.iUnion (restrict (biUnion π πi) J) ⊆ Prepartition.iUnion (πi J)
simp only [iUnion_restrict, iUnion_biUnion, Set.subset_def, Set.mem_inter_iff, Set.mem_iUnion]
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ Prepartition.iUnion (πi J₁)
⊢ x ∈ Prepartition.iUnion (πi J)
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
⊢ ∀ (x : ι → ℝ), (x ∈ ↑J ∧ ∃ i i_1, x ∈ Prepartition.iUnion (πi i)) → x ∈ Prepartition.iUnion (πi J)
rintro x ⟨hxJ, J₁, h₁, hx⟩
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ Prepartition.iUnion (πi J₁)
⊢ J = J₁

case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ Prepartition.iUnion (πi J)
⊢ x ∈ Prepartition.iUnion (πi J)
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ Prepartition.iUnion (πi J₁)
⊢ x ∈ Prepartition.iUnion (πi J)
obtain rfl : J = J₁
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ Prepartition.iUnion (πi J)
⊢ x ∈ Prepartition.iUnion (πi J)
ι : Type u_1
I J J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
J₁ : Box ι
h₁ : J₁ ∈ π
hx : x ∈ Prepartition.iUnion (πi J₁)
⊢ J = J₁

case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ Prepartition.iUnion (πi J)
⊢ x ∈ Prepartition.iUnion (πi J)
exact π.eq_of_mem_of_mem hJ h₁ hxJ (iUnion_subset _ hx)
no goals
case refine'_2.intro.intro.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
hJ : J ∈ π
x : ι → ℝ
hxJ : x ∈ ↑J
h₁ : J ∈ π
hx : x ∈ Prepartition.iUnion (πi J)
⊢ x ∈ Prepartition.iUnion (πi J)
exact hx