case inl
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ splitLower I i x ≠ splitUpper I i x

case inr
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ splitUpper I i x
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ splitLower I i x ≠ splitUpper I i x
cases' le_or_lt x (I.lower i) with h
case inl
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ ⊥ ≠ ↑I
case inl
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ splitLower I i x ≠ splitUpper I i x
rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
no goals
case inl
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ ⊥ ≠ ↑I
exact WithBot.bot_ne_coe
case inr
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ ⊥
case inr
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ splitUpper I i x
refine' (disjoint_splitLower_splitUpper I i x).ne _
no goals
case inr
ι : Type u_1
M : Type ?u.21476
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ ⊥
rwa [Ne.def, splitLower_eq_bot, not_le]