no goals
ι : Type u_1
M : Type ?u.43250
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.fst p.snd
rw [splitMany, Finset.inf_insert, inf_comm, splitMany]