ι : Type u_1
M : Type ?u.51952
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
⊢ π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
refine' (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => _
case refine'_1
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ restrict (splitMany I t) J ≤ restrict (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π) J

case refine'_2
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
⊢ π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
refine' le_antisymm ((biUnion_le_iff _).2 fun J hJ => _) (le_inf (fun J hJ => _) (filter_le _ _))
case refine'_1
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    J_1 ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (splitMany I t).boxes →
      J_1 ≠ ⊥ →
        ∃ J',
          J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π).boxes ∧
            J_1 ≤ J'
case refine'_1
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ restrict (splitMany I t) J ≤ restrict (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π) J
refine' ofWithBot_mono _
case refine'_1
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    (∃ a, a ∈ splitMany I t ∧ ↑J ⊓ ↑a = J_1) →
      J_1 ≠ ⊥ → ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ J_1 ≤ J'
case refine'_1
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    J_1 ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (splitMany I t).boxes →
      J_1 ≠ ⊥ →
        ∃ J',
          J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π).boxes ∧
            J_1 ≤ J'
simp only [Finset.mem_image, exists_prop, mem_boxes, mem_filter]
case refine'_1.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ ↑J ⊓ ↑J₁ ≤ J'
case refine'_1
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    (∃ a, a ∈ splitMany I t ∧ ↑J ⊓ ↑a = J_1) →
      J_1 ≠ ⊥ → ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ J_1 ≤ J'
rintro _ ⟨J₁, h₁, rfl⟩ hne
case refine'_1.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ↑J₁ ⊆ ↑J
case refine'_1.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ ↑J ⊓ ↑J₁ ≤ J'
refine' ⟨_, ⟨J₁, ⟨h₁, Subset.trans _ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
no goals
case refine'_1.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ↑J₁ ⊆ ↑J
exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)
case refine'_2
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
case refine'_2
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
rw [mem_filter] at hJ
case refine'_2.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
case refine'_2
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩
case refine'_2.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ Set.Nonempty (↑J' ∩ ↑J)
case refine'_2.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
refine' ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 _⟩
no goals
case refine'_2.intro.intro
ι : Type u_1
M : Type ?u.51952
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ Set.Nonempty (↑J' ∩ ↑J)
exact ⟨J.upper, hmem, J.upper_mem⟩