exact fun _ _ _ k₁_le_a₁ a₁_lt_b₁ b₁_le_k₁ φDiff₁ derivφCont₁ ↦
  sum_eq_int_deriv_aux ⟨k₁_le_a₁, a₁_lt_b₁⟩ b₁_le_k₁ φDiff₁ derivφCont₁
case base
φ : ℝ → ℂ
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
⊢ ∀ (a b : ℝ) (k : ℤ), ↑k ≤ a → a < b → b ≤ ↑k + 1 → P a b
no goals