ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
⊢ Js ≤ J
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
H : ∀ (i : ι), {(i, Box.lower J i), (i, Box.upper J i)} ⊆ s
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
⊢ Js ≤ J
simp only [Finset.insert_subset, Finset.singleton_subset_iff] at H
case intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
⊢ Js ≤ J
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
⊢ Js ≤ J
rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩
case intro.intro.refine'_1
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ Box.lower J i < y i

case intro.intro.refine'_2
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ Box.upper J i
case intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
⊢ Js ≤ J
refine' fun y hy i => ⟨_, _⟩
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
⊢ Box.lower J i < y i
case intro.intro.refine'_1
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ Box.lower J i < y i
rcases splitMany_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
⊢ Box.lower J i < y i
have := Hle hxs
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : ↑Js ⊆ ↑I ∩ {y | Box.lower J i < y i}
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1] at Hle
no goals
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : ↑Js ⊆ ↑I ∩ {y | Box.lower J i < y i}
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
exact (Hle hy).2
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
⊢ y i ≤ Box.upper J i
case intro.intro.refine'_2
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ Box.upper J i
rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
⊢ y i ≤ Box.upper J i
have := Hle hxs
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : ↑Js ⊆ ↑I ∩ {y | y i ≤ Box.upper J i}
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle
no goals
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type ?u.47705
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : ↑Js ⊆ ↑I ∩ {y | y i ≤ Box.upper J i}
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
exact (Hle hy).2