awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + (↑N : ℝ) * h)
k : ℕ
hk : k < N
inl : ∀ (h_neg : h ≤ 0) {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
⊢ ∀ {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
have inr : ∀ (h_pos : 0 ≤ h) {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
Tactic: rcases le_total h 0 with h_neg | h_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + (↑N : ℝ) * h)
k_1 : ℕ
hk_1 : k_1 < N
h_neg : h ≤ 0
k : ℕ
hk : k ≤ N
⊢ a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
have hk₁ : LE.le (α := ℝ) (↑k : ℝ) (↑N : ℝ)
Tactic: rw [← Nat.cast_le (α := ℝ)] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (hypothesis)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + (↑N : ℝ) * h)
k_1 : ℕ
hk_1 : k_1 < N
h_pos : 0 ≤ h
k : ℕ
hk : k ≤ N
⊢ a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
have hk₁ : LE.le (α := ℝ) (↑k : ℝ) (↑N : ℝ)
Tactic: rw [← Nat.cast_le (α := ℝ)] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + (↑N : ℝ) * h)
k_1 : ℕ
hk_1 : k_1 < N
h_pos : 0 ≤ h
k : ℕ
hk : LE.le (α := ℝ) (↑k : ℝ) (↑N : ℝ)
h₁ : 0 ≤ h
⊢ a + (↑k : ℝ) * h ≤ a + (↑N : ℝ) * h
have grw : a + (↑N : ℝ) * h ≤ a + (↑N : ℝ) * h
Tactic: grw [hk]
-- 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| ≤ ζ
⊢ |trapezoidal_error f 1 a b| ≤ HPow.hPow (β := ℕ) (b - a) 3 * ζ / 12
have rw : |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3
Tactic: rw [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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt g (dg y) (Set.Icc a b) y
have unfold : HasDerivWithinAt
  (fun (t : ℝ) ↦
    (t - a) / (↑1 : ℝ) *
        ((f a + f t) / 2 +
          ∑ k ∈ Finset.range (HSub.hSub (α := ℕ) 1 1), f (a + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (t - a) / (↑1 : ℝ))) -
      ∫ (x : ℝ) in a..t, f x)
  (dg y) (Set.Icc a b) y
Tactic: unfold g trapezoidal_error trapezoidal_integral
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      (t - a) / (↑1 : ℝ) *
          ((f a + f t) / 2 +
            ∑ k ∈ Finset.range (HSub.hSub (α := ℕ) 1 1), f (a + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (t - a) / (↑1 : ℝ))) -
        ∫ (x : ℝ) in a..t, f x)
    (dg y) (Set.Icc a b) y
have simp : HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) * ((f a + f t) / 2) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y
Tactic: simp only [Nat.cast_one, div_one, tsub_self, Finset.range_zero, sum_empty, add_zero]
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) * ((f a + f t) / 2) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y
have simp_rw : HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) / 2 * (f a + f t) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y
Tactic: simp_rw [← mul_comm_div]
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ (t - a) / 2 * (f a + f t) - ∫ (x : ℝ) in a..t, f x) (dg y) (Set.Icc a b) y
have refine : HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y
Tactic: refine fun_sub (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _)
      (const_add _ (h_df y hy).hasDerivWithinAt)) ?_
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y
have this : Fact (y ∈ Set.Icc a b)
Tactic: have := Fact.mk hy
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y
have hf : IntervalIntegrable f volume a y
Tactic: apply integral_hasDerivWithinAt_right
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
hf : IntervalIntegrable f volume a y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y
have hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (nhdsWithin y (Set.Icc a b)) volume
Tactic: apply integral_hasDerivWithinAt_right
-- 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| ≤ ζ
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
y : ℝ
hy : y ∈ Set.Icc a b
this : Fact (y ∈ Set.Icc a b)
hf : IntervalIntegrable f volume a y
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (nhdsWithin y (Set.Icc a b)) volume
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ ∫ (x : ℝ) in a..t, f x) (f y) (Set.Icc a b) y
have hb : ContinuousWithinAt f (Set.Icc a b) y
Tactic: apply integral_hasDerivWithinAt_right
-- 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| ≤ ζ
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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3
have h_dg : ∀ (y : ℝ) (hy : y ∈ Set.Icc a b), HasDerivWithinAt g (dg y) (Set.Icc a b) y
Tactic: have h_dg (y : ℝ) (hy : y ∈ Icc a b) : HasDerivWithinAt g (dg y) (Icc a b) y := by
    unfold g trapezoidal_error trapezoidal_integral
    simp only [Nat.cast_one, div_one, tsub_self, Finset.range_zero, sum_empty, add_zero]
    simp_rw [← mul_comm_div]
    refine fun_sub (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _)
      (const_add _ (h_df y hy).hasDerivWithinAt)) ?_
    have := Fact.mk hy -- Needed for integral_hasDerivWithinAt_right
    apply integral_hasDerivWithinAt_right
    · exact (h_df.continuousOn.mono (Icc_subset_Icc le_rfl hy.2)).intervalIntegrable_of_Icc hy.1
    · exact h_df.continuousOn.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc y
    · exact h_df.continuousOn.continuousWithinAt hy
-- 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| ≤ ζ
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
have rw : HasDerivWithinAt dg (1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky) (Set.Icc a b) y
Tactic: rw [(by ring : ddg y = (1 / 2) * dfaky + ((1 / 2) * dfaky + ddg y) - dfaky)]
-- 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| ≤ ζ
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ HasDerivWithinAt dg (1 / 2 * dfaky + (1 / 2 * dfaky + ddg y) - dfaky) (Set.Icc a b) y
have refine : HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc a b) y) (Set.Icc a b) y
Tactic: refine fun_sub (fun_add (const_mul _ (const_add _ (h_df y hx).hasDerivWithinAt))
      (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _) ?_))
      (h_df y hx).hasDerivWithinAt
-- 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| ≤ ζ
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
y : ℝ
hx : y ∈ Set.Icc a b
dfaky : ℝ := _root_.derivWithin f (Set.Icc a b) y
⊢ HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc a b) y) (Set.Icc a b) y
have rw : HasDerivWithinAt (_root_.derivWithin f (Set.Icc a b)) ((fun (g : ℝ → ℝ) ↦ _root_.derivWithin g (Set.Icc a b))^[2] f y)
  (Set.Icc a b) y
Tactic: rw [iteratedDerivWithin_eq_iterate]
-- 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| ≤ ζ
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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3
have h_ddg : ∀ (y : ℝ) (hx : y ∈ Set.Icc a b), HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
Tactic: have h_ddg (y : ℝ) (hx : y ∈ Icc a b) : HasDerivWithinAt dg (ddg y) (Icc a b) y := by
    -- The eventual expression for g'' has several terms that cancel, which we have to undo here
    -- so that the various HasDerivWithinAt theorems will have everything they need.
    let dfaky := derivWithin f (Icc a b) y
    rw [(by ring : ddg y = (1 / 2) * dfaky + ((1 / 2) * dfaky + ddg y) - dfaky)]
    refine fun_sub (fun_add (const_mul _ (const_add _ (h_df y hx).hasDerivWithinAt))
      (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _) ?_))
      (h_df y hx).hasDerivWithinAt
    rw [iteratedDerivWithin_eq_iterate]
    exact (h_ddf y hx).hasDerivWithinAt
-- 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| ≤ ζ
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
have simp_rw : |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
Tactic: simp_rw [pow_one, ddg, abs_mul, abs_div, abs_two]
-- 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| ≤ ζ
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
⊢ |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
have h₁ : 0 ≤ |x - a| / 2
Tactic: grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_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| ≤ ζ
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
⊢ |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
have grw : |x - a| / 2 * ζ ≤ ζ / 2 * (x - a)
Tactic: grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_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| ≤ ζ
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)
⊢ |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
have grw₁ : (x - a) / 2 * ζ ≤ ζ / 2 * (x - a)
Tactic: grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_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| ≤ ζ
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)
⊢ |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
have grw₂ : ζ / 2 * (x - a) ≤ ζ / 2 * (x - a)
Tactic: grw [fpp_bound x, abs_of_nonneg (sub_nonneg.mpr hx.1), div_mul_comm]
-- 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| ≤ ζ
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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * HPow.hPow (β := ℕ) (b - a) 3
have bound_ddg : ∀ (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]
-- 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| ≤ ζ
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
have 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)
Tactic: convert!
        (hasDerivAt_const x (c / (n + 1))).mul
          (((hasDerivAt_id x).sub (hasDerivAt_const x a)).pow (n + 1)) using 1