no goals
ι : Type u_1
M : Type ?u.18967
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (lower I i) (upper I i)
h' : optParam (∀ (j : ι), update I.lower i x j < upper I j) (_ : ∀ (x_1 : ι), update I.lower i x x_1 < upper I x_1)
⊢ splitUpper I i x = ↑{ lower := update I.lower i x, upper := I.upper, lower_lt_upper := h' }
simp only [splitUpper, mk'_eq_coe, max_eq_left h.1.le, update]