case mp
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ π₁ ≤ π₂ →
    (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂

case mpr
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂ →
    π₁ ≤ π₂
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ π₁ ≤ π₂ ↔
    (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
constructor
case mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : Set.Nonempty (↑J ∩ ↑J')
⊢ J ≤ J'
case mp
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ π₁ ≤ π₂ →
    (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
refine' fun H => ⟨fun J hJ J' hJ' Hne => _, iUnion_mono H⟩
case mp.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : Set.Nonempty (↑J ∩ ↑J')
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
⊢ J ≤ J'
case mp
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : Set.Nonempty (↑J ∩ ↑J')
⊢ J ≤ J'
rcases H hJ with ⟨J'', hJ'', Hle⟩
case mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
x : ι → ℝ
hx : x ∈ ↑J
hx' : x ∈ ↑J'
⊢ J ≤ J'
case mp.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
Hne : Set.Nonempty (↑J ∩ ↑J')
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
⊢ J ≤ J'
rcases Hne with ⟨x, hx, hx'⟩
no goals
case mp.intro.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x✝ : ι → ℝ
H : π₁ ≤ π₂
J : Box ι
hJ : J ∈ π₁
J' : Box ι
hJ' : J' ∈ π₂
J'' : Box ι
hJ'' : J'' ∈ π₂
Hle : J ≤ J''
x : ι → ℝ
hx : x ∈ ↑J
hx' : x ∈ ↑J'
⊢ J ≤ J'
rwa [π₂.eq_of_mem_of_mem hJ' hJ'' hx' (Hle hx)]
case mpr.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
HU : Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₁
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
case mpr
ι : Type u_1
I J J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
⊢ (∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J') ∧
      Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂ →
    π₁ ≤ π₂
rintro ⟨H, HU⟩ J hJ
case mpr.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J, J ∈ π₁ ∧ x ∈ J) → ∃ J, J ∈ π₂ ∧ x ∈ J
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
case mpr.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
HU : Prepartition.iUnion π₁ ⊆ Prepartition.iUnion π₂
J : Box ι
hJ : J ∈ π₁
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
simp only [Set.subset_def, mem_iUnion] at HU
case mpr.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J, J ∈ π₁ ∧ x ∈ J) → ∃ J, J ∈ π₂ ∧ x ∈ J
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hx : J.upper ∈ J₂
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
case mpr.intro
ι : Type u_1
I J✝ J₁ J₂ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J, J ∈ π₁ ∧ x ∈ J) → ∃ J, J ∈ π₂ ∧ x ∈ J
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
rcases HU J.upper ⟨J, hJ, J.upper_mem⟩ with ⟨J₂, hJ₂, hx⟩
no goals
case mpr.intro.intro.intro
ι : Type u_1
I J✝ J₁ J₂✝ : Box ι
π π₁ π₂ : Prepartition I
x : ι → ℝ
H : ∀ (J : Box ι), J ∈ π₁ → ∀ (J' : Box ι), J' ∈ π₂ → Set.Nonempty (↑J ∩ ↑J') → J ≤ J'
J : Box ι
hJ : J ∈ π₁
HU : ∀ (x : ι → ℝ), (∃ J, J ∈ π₁ ∧ x ∈ J) → ∃ J, J ∈ π₂ ∧ x ∈ J
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hx : J.upper ∈ J₂
⊢ ∃ I', I' ∈ π₂ ∧ J ≤ I'
exact ⟨J₂, hJ₂, H _ hJ _ hJ₂ ⟨_, J.upper_mem, hx⟩⟩