let P := fun a₁ b₁ ↦ (∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x) →
  (ContinuousOn (deriv φ) [[a₁, b₁]]) →
  ∑ n in Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ n =
  (∫ x in a₁..b₁, φ x) + (⌊b₁⌋ + 1 / 2 - b₁) * φ b₁ - (⌊a₁⌋ + 1 / 2 - a₁) * φ a₁
    - ∫ x in a₁..b₁, (⌊x⌋ + 1 / 2 - x) * deriv φ x
φ : ℝ → ℂ
a b : ℝ
a_lt_b : a < b
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
φ : ℝ → ℂ
a b : ℝ
a_lt_b : a < b
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
P : ℝ → ℝ → Prop :=
  fun a₁ b₁ =>
    (∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x) →
      ContinuousOn (deriv φ) [[a₁, b₁]] →
        ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ ↑n =
          (∫ (x : ℝ) in a₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
            ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x