no goals
ι : Type u_2
M✝ : Type ?u.34450
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
M : Type u_1
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J in (split I i x).boxes, f J = Option.elim' 0 f (Box.splitLower I i x) + Option.elim' 0 f (Box.splitUpper I i x)
rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]