awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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 a b) x =
    _root_.derivWithin (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1))) x
have 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
Tactic: rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_ddf x (h3 hx))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
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)))
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have 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)))
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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| ≤ ζ
have pos : ∀ (hx : x ∈ Set.Icc (ak k) (ak (k + 1))), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
Tactic: by_cases hx : x ∈ Icc (ak k) (ak (k + 1))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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| ≤ ζ
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
have neg : ∀ (hx : x ∉ Set.Icc (ak k) (ak (k + 1))), |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
Tactic: by_cases hx : x ∈ Icc (ak k) (ak (k + 1))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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))
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
have pos : |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
Tactic: grw [← h6 hx, fpp_bound]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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| ≤ ζ
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
have pos₁ : ζ ≤ ζ
Tactic: grw [← h6 hx, fpp_bound]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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))
⊢ |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ
have neg : 0 ≤ ζ
Tactic: rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure
        (by rwa [closure_Icc]), abs_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
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)))
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have h7 : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
have refine_1 : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1)))) (Set.Icc (ak k) (ak (k + 1)))
Tactic: refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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)))
⊢ |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * HPow.hPow (β := ℕ) h 3
have refine_2 : HPow.hPow (β := ℕ) (ak (k + 1) - ak k) 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
Tactic: refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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)))
have 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
Tactic: refine h_ddf.congr_mono (fun x hx ↦ ?_) h3
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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| ≤ ζ
⊢ HPow.hPow (β := ℕ) (ak (k + 1) - ak k) 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
have refine_2 : HPow.hPow (β := ℕ) h 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
Tactic: rw [h0, mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
⊢ HPow.hPow (β := ℕ) (ak (k + 1) - ak k) 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
have refine_2₁ : HPow.hPow (β := ℕ) h 3 * (ζ / 12) = ζ / 12 * HPow.hPow (β := ℕ) h 3
Tactic: rw [h0, mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
⊢ HPow.hPow (β := ℕ) (ak (k + 1) - ak k) 3 * ζ / 12 = ζ / 12 * HPow.hPow (β := ℕ) h 3
have refine_2₂ : ζ / 12 * HPow.hPow (β := ℕ) h 3 = ζ / 12 * HPow.hPow (β := ℕ) h 3
Tactic: rw [h0, mul_div_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have inl : ∀ (h_lt : a < b),
  |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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have inr : ∀ (h_eq : a = b),
  |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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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)
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have inr₁ : ∀ (h_gt : b < a),
  |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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have 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)
Tactic: rw [uIcc_of_lt h_lt] at *
Cleared hypotheses: h_df, h_ddf, ζ, fpp_bound, N, N_nonzero, h_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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)
have inl : |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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have 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)
Tactic: rw [uIcc_of_gt h_gt] at *
Cleared hypotheses: h_df, h_ddf, ζ, fpp_bound, N, N_nonzero, h_gt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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 a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have inr : |trapezoidal_error f N b a| ≤ HPow.hPow (β := ℕ) (a - b) 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
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
⊢ |trapezoidal_error f N a b| ≤ HPow.hPow (β := ℕ) |b - a| 3 * ζ / (12 * HPow.hPow (α := ℝ) (β := ℕ) (↑N : ℝ) 2)
have inl : ∀ (h_eq : a = b),
  |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