ι : Type u_1
M : Type ?u.36480
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
J : Box ι
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split I i x).boxes
ι : Type u_1
M : Type ?u.36480
n : ℕ
I J : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
⊢ split I i x = ⊤
refine' ((isPartitionTop I).eq_of_boxes_subset fun J hJ => _).symm
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes
ι : Type u_1
M : Type ?u.36480
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
J : Box ι
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split I i x).boxes
rcases mem_top.1 hJ with rfl
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ J ∈ (split J i x).boxes
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes
clear hJ
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ J ∈ (split J i x).boxes
rw [mem_boxes, mem_split_iff]
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : x ≤ Box.lower J i ∨ Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
rw [mem_Ioo, not_and_or, not_lt, not_lt] at h
case inl.h
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ Box.lower J i
⊢ ↑J = Box.splitUpper J i x

case inr.h
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : x ≤ Box.lower J i ∨ Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
cases h <;> [right; left]
no goals
case inl.h
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ Box.lower J i
⊢ ↑J = Box.splitUpper J i x
rwa [eq_comm, Box.splitUpper_eq_self]
no goals
case inr.h
ι : Type u_1
M : Type ?u.36480
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x
rwa [eq_comm, Box.splitLower_eq_self]