MeasureTheory.lintegral_Ioc_partition

lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc : 0 ≤ c) :    ∫⁻ t in Ioc (a * c) (b * c), f t =    ∑ l ∈ Finset.Ico a b, ∫⁻ t in Ioc (l * c) ((l + 1 : ℕ) * c), f t := by  rcases lt_or_ge b a with h | h  · rw [Finset.Ico_eq_empty (by lia), Ioc_eq_empty (by rw [not_lt]; gcongr),      setLIntegral_empty, Finset.sum_empty]  induction b, h using Nat.le_induction with  | base =>    rw [Finset.Ico_self, Ioc_self, setLIntegral_empty, Finset.sum_empty]  | succ b h ih =>    have li : a * c ≤ b * c := by gcongr    rw [← Ioc_union_Ioc_eq_Ioc li (by gcongr; lia),      lintegral_union measurableSet_Ioc (Ioc_disjoint_Ioc_of_le le_rfl),      ← Order.succ_eq_add_one, ← Finset.insert_Ico_right_eq_Ico_succ h,      Finset.sum_insert Finset.right_notMem_Ico,      add_comm (lintegral ..), ih, Order.succ_eq_add_one]