ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
⊢ π ≤ ofWithBot boxes le_of_mem pairwise_disjoint
intro J hJ
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : ↑J ≤ J'
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
rcases H J hJ with ⟨J', J'mem, hle⟩
case intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : ↑J' ∈ boxes
hle : ↑J ≤ ↑J'
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
case intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : ↑J ≤ J'
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
lift J' to Box ι using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle
no goals
case intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ (J : WithBot (Box ι)), J ∈ boxes → J ≤ ↑I
pairwise_disjoint : Set.Pairwise (↑boxes) Disjoint
H : ∀ (J : Box ι), J ∈ π → ∃ J', J' ∈ boxes ∧ ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : ↑J' ∈ boxes
hle : ↑J ≤ ↑J'
⊢ ∃ I', I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint ∧ J ≤ I'
exact ⟨J', mem_ofWithBot.2 J'mem, WithBot.coe_le_coe.1 hle⟩