no goals
ι : Type u_1
M : Type u_2
n : ℕ
N : Type ?u.40368
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
I₀ : WithTop (Box ι)
I J : Box ι
i✝ : ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
i : ι
x : ℝ
⊢ Option.elim' 0 (↑f) (splitLower I i x) + Option.elim' 0 (↑f) (splitUpper I i x) = ↑f I
rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]