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
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 rwa rwa₁ rwa₂ rwa₃ : x ∉ Set.Icc (ak k) (ak (k + 1))
⊢ x ∉ closure (Set.Icc (ak k) (ak (k + 1)))

Tactic:
rwa [closure_Icc]

Premises used: closure_Icc
-- 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))
neg : 0 ≤ ζ
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ

Tactic:
rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure
        (by rwa [closure_Icc]), abs_zero]

Premises used: derivWithin_zero_of_notMem_closure, abs_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)))
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))
⊢ 0 ≤ ζ

Tactic:
(abs_nonneg _).trans (fpp_bound 0)

Premises used: LE.le.trans, OfNat.ofNat, abs_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| ≤ ζ
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))
⊢ 0 ≤ ζ

Tactic:
exact (abs_nonneg _).trans (fpp_bound 0)

Premises used: LE.le.trans, OfNat.ofNat, abs_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| ≤ ζ
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 : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ

Tactic:
have h7 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by
    by_cases hx : x ∈ Icc (ak k) (ak (k + 1))
    · grw [← h6 hx, fpp_bound]
    · rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure
        (by rwa [closure_Icc]), abs_zero]
      exact (abs_nonneg _).trans (fpp_bound 0)
-- 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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3

Tactic:
(trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_

Premises used: LE.le.trans_eq, _private.0.trapezoidal_error_le_of_lt', DifferentiableOn.mono
-- 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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
refine_1 : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1)))
refine_2 : HPow.hPow (β := ℕ) (ak (k + 1) - ak k) 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3

Tactic:
refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_

Premises used: LE.le.trans_eq, _private.0.trapezoidal_error_le_of_lt', DifferentiableOn.mono
-- 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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
⊢ DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1)))

Tactic:
h_ddf.congr_mono (fun x hx ↦ ?_) h3

Premises used: DifferentiableOn.congr_mono
-- 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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
refine_1 :
  ∀ (x : ℝ) (hx : x ∈ Set.Icc (ak k) (ak (k + 1))),
    _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x = _root_.derivWithin f (Set.Icc a b) x
⊢ DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1)))

Tactic:
refine h_ddf.congr_mono (fun x hx ↦ ?_) h3

Premises used: DifferentiableOn.congr_mono
-- 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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x = _root_.derivWithin f (Set.Icc a b) x

Tactic:
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)
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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x = _root_.derivWithin f (Set.Icc a b) x

Tactic:
exact 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)
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)))
h7 : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
refine_2 : HPow.hPow (β := ℕ) h 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
refine_2₁ : HPow.hPow (β := ℕ) h 3 * (ζ / 12) = ζ / 12 * HPow.hPow (β := ℕ) h 3
refine_2₂ refine_2₃ : ζ / 12 * HPow.hPow (β := ℕ) h 3 = ζ / 12 * HPow.hPow (β := ℕ) h 3
⊢ HPow.hPow (β := ℕ) (ak (k + 1) - ak k) 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3

Tactic:
rw [h0, mul_div_assoc, mul_comm]

Premises used: mul_div_assoc, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
inl :
  ∀ (h_lt : a < b),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
inr :
  ∀ (h_eq : a = b),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
inr₁ :
  ∀ (h_gt : b < a),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
rcases lt_trichotomy a b with h_lt | h_eq | h_gt

Premises used: lt_trichotomy
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_lt : a < b
inl :
  ∀ (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_lt : a < b),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - 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 [uIcc_of_lt h_lt] at *

Premises used: Set.uIcc_of_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
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_lt : a < b
inl : |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - 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 [abs_of_pos (sub_pos.mpr h_lt)]

Premises used: Iff.mpr, sub_pos, abs_of_pos
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
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_lt : a < b
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
trapezoidal_error_le_of_lt h_lt h_df h_ddf fpp_bound N_nonzero

Premises used: _private.0.trapezoidal_error_le_of_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
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_lt : a < b
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
exact trapezoidal_error_le_of_lt h_lt h_df h_ddf fpp_bound N_nonzero

Premises used: _private.0.trapezoidal_error_le_of_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_eq : a = b
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
simp [h_eq]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f [[a, b]]
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
inr :
  ∀ (h_df : DifferentiableOn ℝ f (Set.Icc b a))
    (h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc b a)) (Set.Icc b a)) {ζ : ℝ}
    (fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc b a) x| ≤ ζ) {N : ℕ} (N_nonzero : 0 < N) (h_gt : b < a),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - 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 [uIcc_of_gt h_gt] at *

Premises used: Set.uIcc_of_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f (Set.Icc b a)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc b a)) (Set.Icc b a)
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc b a) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
inr : |trapezoidal_error f N b a| ≤ HPow.hPow (β := ℕ) (a - b) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
rw [abs_of_neg (sub_neg.mpr h_gt), neg_sub, trapezoidal_error_symm f N_nonzero a b, abs_neg]

Premises used: sub_neg, Iff.mpr, abs_neg, neg_sub, abs_of_neg, trapezoidal_error_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f (Set.Icc b a)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc b a)) (Set.Icc b a)
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc b a) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
⊢ |trapezoidal_error f N b a| ≤ HPow.hPow (β := ℕ) (a - b) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
trapezoidal_error_le_of_lt h_gt h_df h_ddf fpp_bound N_nonzero

Premises used: _private.0.trapezoidal_error_le_of_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f (Set.Icc b a)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc b a)) (Set.Icc b a)
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc b a) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
⊢ |trapezoidal_error f N b a| ≤ HPow.hPow (β := ℕ) (a - b) 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
exact trapezoidal_error_le_of_lt h_gt h_df h_ddf fpp_bound N_nonzero

Premises used: _private.0.trapezoidal_error_le_of_lt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
inl :
  ∀ (h_eq : a = b),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
inr :
  ∀ (h_ne : a ≠ b),
    |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
rcases eq_or_ne a b with h_eq | h_ne

Premises used: eq_or_ne
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_eq : a = b
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)

Tactic:
simp [h_eq]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
⊢ UniqueDiffOn ℝ [[a, b]]

Tactic:
have ud : UniqueDiffOn ℝ [[a, b]] := uniqueDiffOn_Icc (inf_lt_sup.mpr h_ne)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
⊢ DifferentiableOn ℝ f [[a, b]]

Tactic:
have h_df : DifferentiableOn ℝ f [[a, b]] := ContDiffOn.differentiableOn h_f_c2 two_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
h_df : DifferentiableOn ℝ f [[a, b]]
rw : DifferentiableOn ℝ (iteratedDerivWithin 1 f [[a, b]]) [[a, b]]
⊢ DifferentiableOn ℝ (_root_.derivWithin f [[a, b]]) [[a, b]]

Tactic:
rw [← iteratedDerivWithin_one]

Premises used: iteratedDerivWithin_one
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
h_f_c2 : ContDiffOn ℝ 2 f [[a, b]]
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f [[a, b]] x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_ne : a ≠ b
ud : UniqueDiffOn ℝ [[a, b]]
h_df : DifferentiableOn ℝ f [[a, b]]
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LT.lt (α := ℕ) 1 2
⊢ LT.lt (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 2

Tactic:
norm_cast