Theorem: sum_eq_int_deriv (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
φ : ℝ → ℂ
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
Tactic:
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
State after:
φ : ℝ → ℂ
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

State before:
φ : ℝ → ℂ
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
Tactic:
apply interval_induction P ?base ?step a b a_lt_b φDiff derivφCont
State after:
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

case step
φ : ℝ → ℂ
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 : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b

State before:
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
Tactic:
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₁
State after:
no goals

State before:
case step
φ : ℝ → ℂ
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 : ℝ) (k : ℤ) (b : ℝ), a < ↑k → ↑k < b → P a ↑k → P (↑k) b → P a b
Tactic:
intro a₁ k₁ b₁ a₁_lt_k₁ k₁_lt_b₁ ih₁ ih₂ φDiff₁ derivφCont₁
State after:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) 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

State before:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) 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
Tactic:
have subs := uIcc_subsets ⟨a₁_lt_k₁.le, k₁_lt_b₁.le⟩
State after:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[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

State before:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[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
Tactic:
have s₁ := ih₁ (fun x hx ↦ φDiff₁ x <| subs.1 hx) <| derivφCont₁.mono subs.1
State after:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊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

State before:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊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
Tactic:
have s₂ := ih₂ (fun x hx ↦ φDiff₁ x <| subs.2 hx) <| derivφCont₁.mono subs.2
State after:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..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

State before:
case step
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..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
Tactic:
convert Mathlib.Tactic.LinearCombination.add_pf s₁ s₂ using 1
State after:
case h.e'_2
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ ↑n = ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n + ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n

case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ (∫ (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 =
    ((∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      ((∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)

State before:
case h.e'_2
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊b₁⌋, φ ↑n = ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n + ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n
Tactic:
rw [← Finset.sum_Ioc_add_sum_Ioc]
State after:
case h.e'_2.hb
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ⌊↑k₁⌋ ∈ Finset.Icc ⌊a₁⌋ ⌊b₁⌋

State before:
case h.e'_2.hb
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ⌊↑k₁⌋ ∈ Finset.Icc ⌊a₁⌋ ⌊b₁⌋
Tactic:
simp only [Finset.mem_Icc, Int.floor_intCast, Int.le_floor]
State after:
case h.e'_2.hb
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ⌊a₁⌋ ≤ k₁ ∧ ↑k₁ ≤ b₁

State before:
case h.e'_2.hb
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ ⌊a₁⌋ ≤ k₁ ∧ ↑k₁ ≤ b₁
Tactic:
exact ⟨Int.cast_le.mp <| le_trans (Int.floor_le a₁) a₁_lt_k₁.le, k₁_lt_b₁.le⟩
State after:
no goals

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ (∫ (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 =
    ((∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      ((∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)
Tactic:
set I₁ := ∫ (x : ℝ) in a₁..b₁, φ x
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x =
    ((∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      ((∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    (∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x =
    ((∫ (x : ℝ) in a₁..↑k₁, φ x) + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      ((∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)
Tactic:
set I₂ := ∫ (x : ℝ) in a₁..k₁, φ x
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x =
    (I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      ((∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    (∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x =
    (I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      ((∫ (x : ℝ) in ↑k₁..b₁, φ x) + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)
Tactic:
set I₃ := ∫ (x : ℝ) in k₁..b₁, φ x
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x =
    (I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x =
    (I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)
Tactic:
set J₁ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    (I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
s₁ :
  ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
      ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    (I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ -
        ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x) +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)
Tactic:
set J₂ := ∫ (x : ℝ) in a₁..k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
s₂ :
  ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n =
    I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
      ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ -
        ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x)
Tactic:
set J₃ := ∫ (x : ℝ) in k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
hJ : J₂ + J₃ = J₁
⊢ I₁ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₁ =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)
Tactic:
rw [← hI, ← hJ]
State after:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
hJ : J₂ + J₃ = J₁
⊢ I₂ + I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - (J₂ + J₃) =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)

State before:
case h.e'_3
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
hJ : J₂ + J₃ = J₁
⊢ I₂ + I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - (J₂ + J₃) =
    I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂ +
      (I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃)
Tactic:
ring
State after:
no goals

State before:
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
⊢ I₂ + I₃ = I₁
Tactic:
apply intervalIntegral.integral_add_adjacent_intervals <;>
apply (HasDerivAt.continuousOn <| fun x hx ↦ φDiff₁ x ?_ ).intervalIntegrable
State after:
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
x : ℝ
hx : x ∈ [[a₁, ↑k₁]]
⊢ x ∈ [[a₁, b₁]]

φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
x : ℝ
hx : x ∈ [[↑k₁, b₁]]
⊢ x ∈ [[a₁, b₁]]

State before:
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
x : ℝ
hx : x ∈ [[a₁, ↑k₁]]
⊢ x ∈ [[a₁, b₁]]
Tactic:
exact subs.1 hx
State after:
no goals

State before:
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
x : ℝ
hx : x ∈ [[↑k₁, b₁]]
⊢ x ∈ [[a₁, b₁]]
Tactic:
exact subs.2 hx
State after:
no goals

State before:
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
⊢ J₂ + J₃ = J₁
Tactic:
apply intervalIntegral.integral_add_adjacent_intervals <;>
refine integrability_aux.mul_continuousOn <| derivφCont₁.mono ?_
State after:
case hab
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
⊢ [[a₁, ↑k₁]] ⊆ [[a₁, b₁]]

case hbc
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
⊢ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]

State before:
case hab
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
⊢ [[a₁, ↑k₁]] ⊆ [[a₁, b₁]]
Tactic:
exact subs.1
State after:
no goals

State before:
case hbc
φ : ℝ → ℂ
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₁ : ℝ
k₁ : ℤ
b₁ : ℝ
a₁_lt_k₁ : a₁ < ↑k₁
k₁_lt_b₁ : ↑k₁ < b₁
ih₁ : P a₁ ↑k₁
ih₂ : P (↑k₁) b₁
φDiff₁ : ∀ x ∈ [[a₁, b₁]], HasDerivAt φ (deriv φ x) x
derivφCont₁ : ContinuousOn (deriv φ) [[a₁, b₁]]
subs : [[a₁, ↑k₁]] ⊆ [[a₁, b₁]] ∧ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
I₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, φ x
I₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, φ x
I₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, φ x
J₁ : ℂ := ∫ (x : ℝ) in a₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
J₂ : ℂ := ∫ (x : ℝ) in a₁..↑k₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₁ : ∑ n ∈ Finset.Ioc ⌊a₁⌋ ⌊↑k₁⌋, φ ↑n = I₂ + (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - (↑⌊a₁⌋ + 1 / 2 - ↑a₁) * φ a₁ - J₂
J₃ : ℂ := ∫ (x : ℝ) in ↑k₁..b₁, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
s₂ : ∑ n ∈ Finset.Ioc ⌊↑k₁⌋ ⌊b₁⌋, φ ↑n = I₃ + (↑⌊b₁⌋ + 1 / 2 - ↑b₁) * φ b₁ - (↑⌊↑k₁⌋ + 1 / 2 - ↑↑k₁) * φ ↑k₁ - J₃
hI : I₂ + I₃ = I₁
⊢ [[↑k₁, b₁]] ⊆ [[a₁, b₁]]
Tactic:
exact subs.2
State after:
no goals