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| ≤ ζ
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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
norm_cast :
  ∑ x ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑x : ℝ) * h) (a + (↑(x + 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:
norm_cast
-- 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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range N, |trapezoidal_error f 1 (ak i) (ak (i + 1))|)
    (∑ k ∈ Finset.range N, ζ / 12 * HPow.hPow (β := ℕ) h 3)

Tactic:
sum_le_sum this

Premises used: Finset.sum_le_sum
-- 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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ ∑ k ∈ Finset.range N, ζ / 12 * HPow.hPow (β := ℕ) h 3 = (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3)

Tactic:
simp [sum_const]

Premises used: Finset.sum_const
-- 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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
push_cast :
  (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)

Tactic:
push_cast
-- 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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

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
hb : b = a + (↑N : ℝ) * h
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
_ : ∑ k ∈ Finset.range N, ζ / 12 * HPow.hPow (β := ℕ) h 3 = (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3)
_₁ :
  (↑N : ℝ) * (ζ / 12 * HPow.hPow (β := ℕ) h 3) =
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)
⊢ ∑ x ∈ Finset.range N, |trapezoidal_error f 1 (a + (↑x : ℝ) * h) (a + (↑(x + 1) : ℝ) * h)| ≤
    HPow.hPow (β := ℕ) (a + (↑N : ℝ) * h - a) 3 * ζ / (↑(12 * HPow.hPow (β := ℕ) N 2) : ℝ)

Tactic:
calc
      _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; field

Premises used: HMul.hMul, HDiv.hDiv, Finset.range, HPow.hPow, Finset.sum_le_sum, 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
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
suffices : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ ∑ 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:
suffices ∀ k ∈ range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ (ζ / 12) * h ^ 3 by
    norm_cast
    calc
      _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; 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
k : ℕ
hk : k ∈ Finset.range N
⊢ k < N

Tactic:
rw [Finset.mem_range] at hk

Premises used: Finset.mem_range
-- 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
k : ℕ
hk : k < N
simp : 0 ≤ (↑k : ℝ) * h
⊢ a ≤ ak k

Tactic:
simp only [ak, le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right
-- 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
k : ℕ
hk : k < N
⊢ 0 ≤ (↑k : ℝ) * 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
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
⊢ a ≤ ak k

Tactic:
have h1 : a ≤ ak k := by simp only [ak, le_add_iff_nonneg_right]; 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
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
simp : a + (↑(k + 1) : ℝ) * h ≤ a + (↑N : ℝ) * h
⊢ ak (k + 1) ≤ b

Tactic:
simp only [ak, hb]
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h₁ : 0 ≤ h
grw grw₁ : a + (↑N : ℝ) * h ≤ a + (↑N : ℝ) * h
⊢ a + (↑(k + 1) : ℝ) * h ≤ a + (↑N : ℝ) * h

Tactic:
grw [Nat.lt_iff_add_one_le.mp hk]

Premises used: Nat.lt_iff_add_one_le, Iff.mp
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
⊢ ak (k + 1) ≤ b

Tactic:
have h2 : ak (k + 1) ≤ b := by simp only [ak, hb]; grw [Nat.lt_iff_add_one_le.mp hk]
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
⊢ Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b

Tactic:
have h3 : Icc (ak k) (ak (k + 1)) ⊆ Icc a b := Icc_subset_Icc h1 h2
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
rwa : 0 < ak (k + 1) - ak k
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < h
⊢ ak k < ak (k + 1)

Tactic:
rwa [← sub_pos, h0]

Premises used: sub_pos
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
⊢ ak k < ak (k + 1)

Tactic:
have h4 : ak k < ak (k + 1) := by rwa [← sub_pos, 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| ≤ ζ
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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
rw rw₁ : _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x = _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x
⊢ _root_.derivWithin f (Set.Icc a b) x = _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]

Premises used: uniqueDiffOn_Icc, derivWithin_subset
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
⊢ EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))

Tactic:
have h5 : EqOn (derivWithin f (Icc a b))
      (derivWithin f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by
    intro x hx
    rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
simp :
  _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x
⊢ iteratedDerivWithin 2 f (Set.Icc a b) x = iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero]

Premises used: iteratedDerivWithin_zero, iteratedDerivWithin_succ'
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
rw :
  _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc (ak k) (ak (k + 1))) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x
⊢ _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_ddf x (h3 hx))]

Premises used: uniqueDiffOn_Icc, derivWithin_subset
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc (ak k) (ak (k + 1))) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
derivWithin_congr h5 (h5 hx)

Premises used: derivWithin_congr
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin (_root_.derivWithin f (Set.Icc a b)) (Set.Icc (ak k) (ak (k + 1))) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x

Tactic:
exact derivWithin_congr h5 (h5 hx)

Premises used: derivWithin_congr
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
⊢ EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))

Tactic:
have h6 : EqOn (iteratedDerivWithin 2 f (Icc a b))
    (iteratedDerivWithin 2 f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by
    intro x hx
    simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero]
    rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_ddf x (h3 hx))]
    exact derivWithin_congr h5 (h5 hx)
-- 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
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
pos : ∀ (hx : x ∈ Set.Icc (ak k) (ak (k + 1))), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
neg : ∀ (hx : x ∉ Set.Icc (ak k) (ak (k + 1))), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ

Tactic:
by_cases hx : x ∈ Icc (ak k) (ak (k + 1))

Premises used: Set.Icc, HAdd.hAdd, 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
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + (↑N : ℝ) * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
pos : |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
pos₁ pos₂ : ζ ≤ ζ
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ

Tactic:
grw [← h6 hx, fpp_bound]