ι : 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 : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J', J' ∈ π ∧ J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
ι : 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 : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
have : ∀ J : Box ι, ↑J ∈ boxes → ∃ J' ∈ π, J ≤ J' := fun J hJ => by
  simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot
no goals
ι : 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 : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
this : ∀ (J : Box ι), ↑J ∈ boxes → ∃ J', J' ∈ π ∧ J ≤ J'
⊢ ofWithBot boxes le_of_mem pairwise_disjoint ≤ π
simpa [ofWithBot, le_def]
no goals
ι : 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 : WithBot (Box ι)), J ∈ boxes → J ≠ ⊥ → ∃ J', J' ∈ π ∧ J ≤ ↑J'
J : Box ι
hJ : ↑J ∈ boxes
⊢ ∃ J', J' ∈ π ∧ J ≤ J'
simpa only [WithBot.coe_le_coe] using H J hJ WithBot.coe_ne_bot