integral_deriv_mul_floor_add_one

lemma integral_deriv_mul_floor_add_one (ha : 0 ≤ a) (hab : a ≤ b)    (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (h_cont : ContinuousOn (deriv f) [[a, b]]) :    ∫ t in a..b, deriv f t * (⌊t⌋₊ + 1) = (b + 1 / 2) * f b - (a + 1 / 2) * f a - (∫ t in a..b, f t) - ∫ t in a..b, deriv f t * B1 t := by  calc  _ = ∫ t in a..b, (deriv f t * (t + 1 / 2) -deriv f t * B1 t) := by    congr    ext    simp only [B1]    push_cast    ring  _ = (∫ t in a..b, deriv f t * (t + 1 / 2)) - ∫ t in a..b, deriv f t * B1 t := by    exact intervalIntegral.integral_sub (ContinuousOn.intervalIntegrable (by fun_prop)) (intervalIntegrable_deriv_mul_B1 ha hab h_cont)  _ = _ := by    conv => lhs; arg 1; arg 1; ext; rw [mul_comm]    rw [integral_deriv_mul_add_const _ hab h_cont.intervalIntegrable hf_diff]