no goals
ι : Type u_3
I J J₁ J₂ : Box ι
π✝ π₁ π₂ : Prepartition I
x : ι → ℝ
πi πi₁ πi₂ : (J : Box ι) → Prepartition J
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ ∑ y in Finset.image f π.boxes, ∑ J in (filter π fun J => f J = y).boxes, g J = ∑ J in π.boxes, g J
convert sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g