awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
x : ℝ
hx : x ∈ Set.Icc a b
h₁ : 0 ≤ |x - a| / 2
grw : |x - a| / 2 * ζ ≤ ζ / 2 * (x - a)
grw₁ : (x - a) / 2 * ζ ≤ ζ / 2 * (x - a)
grw₂ grw₃ : ζ / 2 * (x - a) ≤ ζ / 2 * (x - a)
⊢ |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)

Tactic:
grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_mul_comm]

Premises used: Iff.mpr, And.left, div_mul_comm, abs_of_nonneg, sub_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
⊢ ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1

Tactic:
have bound_ddg (x : ℝ) (hx : x ∈ Icc a b) : |ddg x| ≤ (ζ / 2) * ((x - a) ^ 1) := by
    simp_rw [pow_one, ddg, abs_mul, abs_div, abs_two]
    grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_mul_comm]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
x : ℝ
⊢ HasDerivAt ((fun (x : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) * (HSub.hSub (α := ℝ → ℝ) id fun (x : ℝ) ↦ a) ^ (n + 1))
    (0 * ((HSub.hSub (α := ℝ → ℝ) id fun (x : ℝ) ↦ a) ^ (n + 1)) x +
      c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
        ((↑(n + 1) : ℝ) * HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ a) x ^ (n + 1 - 1) *
          HSub.hSub (α := ℝ) 1 0))
    x

Tactic:
(hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1))

Premises used: HasDerivAt.pow, HasDerivAt.sub, hasDerivAt_const, HDiv.hDiv, Nat.cast, hasDerivAt_id, HAdd.hAdd, HasDerivAt.mul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
x : ℝ
h₁ :
  c * (x - a) ^ n =
    0 * ((HSub.hSub (α := ℝ → ℝ) id fun (x : ℝ) ↦ a) ^ (n + 1)) x +
      c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
        ((↑(n + 1) : ℝ) * HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ a) x ^ (n + 1 - 1) *
          HSub.hSub (α := ℝ) 1 0)
⊢ HasDerivAt (fun (y : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x

Tactic:
convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1

Premises used: HasDerivAt.pow, HasDerivAt.sub, hasDerivAt_const, HDiv.hDiv, Nat.cast, hasDerivAt_id, HAdd.hAdd, HasDerivAt.mul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
x : ℝ
⊢ c * (x - a) ^ n =
    0 * ((HSub.hSub (α := ℝ → ℝ) id fun (x : ℝ) ↦ a) ^ (n + 1)) x +
      c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 *
        ((↑(n + 1) : ℝ) * HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ a) x ^ (n + 1 - 1) *
          HSub.hSub (α := ℝ) 1 0)

Tactic:
simp [sub_eq_add_neg, field]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
⊢ ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x

Tactic:
have hB (x) : HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by
      convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1
      simp [sub_eq_add_neg, field]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
hB : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x
x : ℝ
hx : x ∈ Set.Ico a b
⊢ HasDerivWithinAt φ (φ' x) (Set.Ici x) x

Tactic:
grind [Icc_mem_nhdsGE_of_mem, mono_of_mem_nhdsWithin]

Premises used: Icc_mem_nhdsGE_of_mem, HasDerivWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
hB : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x
⊢ ‖φ a‖ ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (a - a) ^ (n + 1)

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
φ φ' : ℝ → ℝ
h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x
h0 : φ a = 0
c : ℝ
n : ℕ
h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n
t : ℝ
ht : t ∈ Set.Icc a b
hB : ∀ (x : ℝ), HasDerivAt (fun (y : ℝ) ↦ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x
⊢ |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)

Tactic:
simpa [Real.norm_eq_abs, h0] using image_norm_le_of_norm_deriv_right_le_deriv_boundary
      (fun x hx ↦ (h x hx).continuousWithinAt)
      (fun x hx ↦ by grind [Icc_mem_nhdsGE_of_mem, mono_of_mem_nhdsWithin])
      (by simp [h0]) hB (fun x hx ↦ h_bound x (Ico_subset_Icc_self hx)) ht

Premises used: Set.Ico_subset_Icc_self, image_norm_le_of_norm_deriv_right_le_deriv_boundary, HasDerivWithinAt.continuousWithinAt, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
⊢ ∀ {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) (h0 : φ a = 0) {c : ℝ} {n : ℕ}
    (h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n),
    ∀ t ∈ Set.Icc a b, |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)

Tactic:
have key {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Icc a b, HasDerivWithinAt φ (φ' x) (Icc a b) x) (h0 : φ a = 0)
      {c : ℝ} {n : ℕ} (h_bound : ∀ t ∈ Icc a b, |φ' t| ≤ c * (t - a) ^ n) :
      ∀ t ∈ Icc a b, |φ t| ≤ c / (n + 1) * (t - a) ^ (n + 1) := by
    intro t ht
    have hB (x) : HasDerivAt (fun y ↦ c / (n + 1) * (y - a) ^ (n + 1)) (c * (x - a) ^ n) x := by
      convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1
      simp [sub_eq_add_neg, field]
    simpa [Real.norm_eq_abs, h0] using image_norm_le_of_norm_deriv_right_le_deriv_boundary
      (fun x hx ↦ (h x hx).continuousWithinAt)
      (fun x hx ↦ by grind [Icc_mem_nhdsGE_of_mem, mono_of_mem_nhdsWithin])
      (by simp [h0]) hB (fun x hx ↦ h_bound x (Ico_subset_Icc_self hx)) ht
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
key :
  ∀ {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) (h0 : φ a = 0) {c : ℝ} {n : ℕ}
    (h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n),
    ∀ t ∈ Set.Icc a b, |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)
⊢ dg a = 0

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
key :
  ∀ {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) (h0 : φ a = 0) {c : ℝ} {n : ℕ}
    (h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n),
    ∀ t ∈ Set.Icc a b, |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)
⊢ ζ / 2 / HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) 1 *
      (b - a) ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) =
    ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3

Tactic:
ring_nf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ trapezoidal_error f 1 a t
dg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
bound_ddg : ∀ (x : ℝ) (hx : x ∈ Set.Icc a b), |ddg x| ≤ ζ / 2 * HPow.hPow (β := ℕ) (x - a) 1
key :
  ∀ {φ φ' : ℝ → ℝ} (h : ∀ x ∈ Set.Icc a b, HasDerivWithinAt φ (φ' x) (Set.Icc a b) x) (h0 : φ a = 0) {c : ℝ} {n : ℕ}
    (h_bound : ∀ t ∈ Set.Icc a b, |φ' t| ≤ c * (t - a) ^ n),
    ∀ t ∈ Set.Icc a b, |φ t| ≤ c / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (t - a) ^ (n + 1)
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3

Tactic:
exact (key h_dg (trapezoidal_error_eq f 1 a) (key h_ddg (by ring) bound_ddg) b
    ⟨a_lt_b.le, le_rfl⟩).trans_eq (by ring_nf)

Premises used: le_rfl, LE.le.trans_eq, trapezoidal_error_eq, LT.lt.le, And.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
⊢ ∀ (k : ℕ), ak (k + 1) - ak k = h

Tactic:
simp [ak, ← sub_mul]

Premises used: sub_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
⊢ ∀ (k : ℕ), ak (k + 1) - ak k = h

Tactic:
have h0 : ∀ k : ℕ, ak (k + 1) - ak k = h := by simp [ak, ← sub_mul]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
⊢ 0 < b - a

Tactic:
have hab : 0 < b - a := sub_pos.mpr a_lt_b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
⊢ 0 < h

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
⊢ 0 < h

Tactic:
have hpos : 0 < h := by positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
⊢ b = a + (↑N : ℝ) * h

Tactic:
field
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
⊢ b = a + (↑N : ℝ) * h

Tactic:
have hb : b = a + N * h := by field
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
rw :
  |∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
rw [hb, ← sum_trapezoidal_error_adjacent_intervals N_nonzero
    (hb ▸ h_df.continuousOn.intervalIntegrable_of_Icc a_lt_b.le)]

Premises used: sum_trapezoidal_error_adjacent_intervals
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / (↑N : ℝ)
ak : (k : ℕ) → ℝ := fun (k : ℕ) ↦ a + (↑k : ℝ) * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
grw :
  ∑ i ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ |∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
grw [abs_sum_le_sum_abs]

Premises used: Finset.abs_sum_le_sum_abs