no goals
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
by_cases i ∈ s <;> field_simp [splitCenterBox] <;> field_simp [mul_two, two_mul]