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

case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J) → π' ≤ biUnion π πi
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ π' ≤ biUnion π πi ↔ π' ≤ π ∧ ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
refine' ⟨fun H => ⟨H.trans (π.biUnion_le πi), fun J hJ => _⟩, _⟩
case refine'_1
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ biUnion π πi
J : Box ι
hJ : J ∈ π
⊢ restrict π' J ≤ restrict (biUnion π πi) J
case refine'_1
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ biUnion π πi
J : Box ι
hJ : J ∈ π
⊢ restrict π' J ≤ πi J
rw [← π.restrict_biUnion πi hJ]
no goals
case refine'_1
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ biUnion π πi
J : Box ι
hJ : J ∈ π
⊢ restrict π' J ≤ restrict (biUnion π πi) J
exact restrict_mono H
case refine'_2.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
case refine'_2
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
⊢ (π' ≤ π ∧ ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J) → π' ≤ biUnion π πi
rintro ⟨H, Hi⟩ J' hJ'
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
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
case refine'_2.intro
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
rcases H hJ' with ⟨J, hJ, hle⟩
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
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ restrict π' J
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
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
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
have : J' ∈ π'.restrict J :=
  π'.mem_restrict.2 ⟨J', hJ', (inf_of_le_right <| WithBot.coe_le_coe.2 hle).symm⟩
case refine'_2.intro.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ restrict π' J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
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
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ restrict π' J
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩
no goals
case refine'_2.intro.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ (J : Box ι), J ∈ π → restrict π' J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ restrict π' J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I', I' ∈ biUnion π πi ∧ J' ≤ I'
exact ⟨Ji, π.mem_biUnion.2 ⟨J, hJ, hJi⟩, hlei⟩