case intro
ι : Type u_1
M : Type ?u.49727
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
ι : Type u_1
M : Type ?u.49727
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
cases nonempty_fintype ι
case intro
ι : Type u_1
M : Type ?u.49727
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : t ≥ Finset.biUnion s fun J => Finset.biUnion Finset.univ fun i => {(i, Box.lower J i), (i, Box.upper J i)}
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, Box.lower J i), (i, Box.upper J i)} ⊆ t
case intro
ι : Type u_1
M : Type ?u.49727
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
refine' eventually_atTop.2
  ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
    fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => _) hJ'⟩
no goals
case intro
ι : Type u_1
M : Type ?u.49727
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : t ≥ Finset.biUnion s fun J => Finset.biUnion Finset.univ fun i => {(i, Box.lower J i), (i, Box.upper J i)}
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, Box.lower J i), (i, Box.upper J i)} ⊆ t
exact fun p hp =>
  ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)