no goals
ι : Type ?u.21918495
𝕜 : Type ?u.21918498
E : Type u_1
F : Type ?u.21918504
A : Type ?u.21918507
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
μ : MeasureTheory.Measure ℝ
f : ℝ → E
hfi : Integrable f
⊢ HasSum (fun n => ∫ (x : ℝ) in 0 ..1, f (x + ↑n)) (∫ (x : ℝ), f x)
simpa only [integral_comp_add_right, zero_add, add_comm (1:ℝ)] using hfi.hasSum_intervalIntegral 0