rw [sum_eq_int_deriv_aux2 (k + 1 / 2) φDiff derivφCont]
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)