case mp
ι : 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 ∈ π
⊢ πi J ≤ restrict π' J

case mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J : Box ι
hJ : J ∈ biUnion π πi
⊢ ∃ I', I' ∈ π' ∧ J ≤ 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 ∈ π → πi J ≤ restrict π' J
constructor <;> intro H J hJ
case mp
ι : 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 (biUnion π πi) J ≤ restrict π' J
case mp
ι : 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 ∈ π
⊢ πi J ≤ restrict π' J
rw [← π.restrict_biUnion πi hJ]
no goals
case mp
ι : 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 (biUnion π πi) J ≤ restrict π' J
exact restrict_mono H
case mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J : Box ι
hJ : ∃ J', J' ∈ π ∧ J ∈ πi J'
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
case mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J : Box ι
hJ : J ∈ biUnion π πi
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
rw [mem_biUnion] at hJ
case mpr.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
case mpr
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J : Box ι
hJ : ∃ J', J' ∈ π ∧ J ∈ πi J'
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
rcases hJ with ⟨J₁, h₁, hJ⟩
case mpr.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 : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ restrict π' J₁
Hle : J ≤ J₂
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
case mpr.intro.intro
ι : Type u_1
I J✝ J₁✝ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
rcases H J₁ h₁ hJ with ⟨J₂, h₂, Hle⟩
case mpr.intro.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✝ : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ restrict π' J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : ↑J₂ = ↑J₁ ⊓ ↑J₃
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
case mpr.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 : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ restrict π' J₁
Hle : J ≤ J₂
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
rcases π'.mem_restrict.mp h₂ with ⟨J₃, h₃, H⟩
no goals
case mpr.intro.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✝ : ∀ (J : Box ι), J ∈ π → πi J ≤ restrict π' J
J J₁ : Box ι
h₁ : J₁ ∈ π
hJ : J ∈ πi J₁
J₂ : Box ι
h₂ : J₂ ∈ restrict π' J₁
Hle : J ≤ J₂
J₃ : Box ι
h₃ : J₃ ∈ π'
H : ↑J₂ = ↑J₁ ⊓ ↑J₃
⊢ ∃ I', I' ∈ π' ∧ J ≤ I'
exact ⟨J₃, h₃, Hle.trans <| WithBot.coe_le_coe.1 <| H.trans_le inf_le_right⟩