awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
⊢ c⁻¹ * HSub.hSub (α := ℝ) (∫ (x : ℝ) in b..b + c, f x) (∫ (x : ℝ) in a..a + c, f x) ≤ f (b + c) - f a
have fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
Tactic: have fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c) := by
    grw [intervalIntegral.integral_mono_on (g := fun _ ↦ f (b + c))
          (by linarith)
          (hf'.mono_set (by grind [uIcc]))
          (by simp)
          (by intros; apply hf <;> grind [uIcc])]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
⊢ a ≤ a + c
have linarith : a + c < a → 0 - c + (a + c - a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
x : ℝ
h : x ∈ Icc a (a + c)
⊢ (fun (x : ℝ) ↦ f a) x ≤ f x
have x : a ∈ uIcc a (b + c)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
x_1 : ℝ
h : x_1 ∈ Icc a (a + c)
x : a ∈ uIcc a (b + c)
⊢ (fun (x : ℝ) ↦ f a) x_1 ≤ f x_1
have x₁ : x_1 ∈ uIcc a (b + c)
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
x_1 : ℝ
h : x_1 ∈ Icc a (a + c)
x : a ∈ uIcc a (b + c)
x₁ : x_1 ∈ uIcc a (b + c)
⊢ (fun (x : ℝ) ↦ f a) x_1 ≤ f x_1
have a₁ : a ≤ x_1
Tactic: apply hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
⊢ c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
have grw : c * f a ≤ ∫ (u : ℝ) in a..a + c, f a
Tactic: grw [← intervalIntegral.integral_mono_on (f := fun _ ↦ f a)
            (by linarith)
            (by simp)
            (hf'.mono_set (by grind [uIcc]))
            (by intros; apply hf <;> grind [uIcc])]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (hypothesis)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
⊢ c⁻¹ * HSub.hSub (α := ℝ) (∫ (x : ℝ) in b..b + c, f x) (∫ (x : ℝ) in a..a + c, f x) ≤ f (b + c) - f a
have fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
Tactic: have fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x := by
    grw [← intervalIntegral.integral_mono_on (f := fun _ ↦ f a)
            (by linarith)
            (by simp)
            (hf'.mono_set (by grind [uIcc]))
            (by intros; apply hf <;> grind [uIcc])]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
⊢ c⁻¹ * HSub.hSub (α := ℝ) (∫ (x : ℝ) in b..b + c, f x) (∫ (x : ℝ) in a..a + c, f x) ≤ f (b + c) - f a
have inr : c⁻¹ * (c * f (b + c) - c * f a) ≤ f (b + c) - f a
Tactic: grw [fU, ← fL]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope (goal)
Goal:
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc_1 : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
⊢ c⁻¹ * (c * f (b + c) - c * f a) ≤ f (b + c) - f a
have inr : f (b + c) - f a ≤ f (b + c) - f a
Tactic: field_simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / (↑N : ℝ) *
      ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (b - a) / (↑N : ℝ))) =
    -((a - b) / (↑N : ℝ) *
        ((f b + f a) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ))))
have rw : (b - a) / (↑N : ℝ) *
    ((f a + f b) / 2 +
      ∑ j ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - j) : ℝ) 1 * (b - a) / (↑N : ℝ))) =
  (b - a) / (↑N : ℝ) *
    ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ)))
Tactic: rw [neg_mul_eq_neg_mul, neg_div', neg_sub, add_comm (f b) (f a), ← sum_range_reflect]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / (↑N : ℝ) *
      ((f a + f b) / 2 +
        ∑ j ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - j) : ℝ) 1 * (b - a) / (↑N : ℝ))) =
    (b - a) / (↑N : ℝ) *
      ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ)))
have e_a : Eq (α := ℝ) (∑ j ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - j) : ℝ) 1 * (b - a) / (↑N : ℝ)))
  (∑ k ∈ Finset.range (N - 1), f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ)))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ Eq (α := ℝ) (∑ j ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - j) : ℝ) 1 * (b - a) / (↑N : ℝ)))
    (∑ k ∈ Finset.range (N - 1), f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ)))
have e_a : ∀ x ∈ Finset.range (N - 1),
  f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - x) : ℝ) 1 * (b - a) / (↑N : ℝ)) =
    f (b + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * (a - b) / (↑N : ℝ))
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - k) : ℝ) 1 * (b - a) / (↑N : ℝ)) =
    f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ))
have e_a : f (a + (↑(N - 1 - 1 - k + 1) : ℝ) * (b - a) / (↑N : ℝ)) = f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ f (a + (↑(N - 1 - 1 - k + 1) : ℝ) * (b - a) / (↑N : ℝ)) = f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))
have e_a : f (a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ)) =
  f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))
Tactic: rw [tsub_tsub, add_comm 1, Nat.cast_add, Nat.cast_sub (mem_range.mp hk), Nat.cast_sub N_nonzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ f (a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ)) =
    f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))
have e_a : a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ) =
  b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ)
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ trapezoidal_integral f N a b - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
have rw : -trapezoidal_integral f N b a - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
Tactic: rw [trapezoidal_integral_symm f N_nonzero a b, integral_symm, neg_sub_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
rw : -trapezoidal_integral f N b a - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
⊢ trapezoidal_integral f N a b - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
have rw₁ : -trapezoidal_integral f N b a - -∫ (x : ℝ) in b..a, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
Tactic: rw [trapezoidal_integral_symm f N_nonzero a b, integral_symm, neg_sub_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
rw : -trapezoidal_integral f N b a - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
rw₁ : -trapezoidal_integral f N b a - -∫ (x : ℝ) in b..a, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
⊢ trapezoidal_integral f N a b - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
have rw₂ : (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
Tactic: rw [trapezoidal_integral_symm f N_nonzero a b, integral_symm, neg_sub_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
rw : -trapezoidal_integral f N b a - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
rw₁ : -trapezoidal_integral f N b a - -∫ (x : ℝ) in b..a, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
rw₂ : (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
⊢ trapezoidal_integral f N a b - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
have rw₃ : (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a = (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a
Tactic: rw [trapezoidal_integral_symm f N_nonzero a b, integral_symm, neg_sub_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) =
    trapezoidal_integral f N a (a + (↑N : ℝ) * h)
have simp_rw : h / 2 * ∑ i ∈ Finset.range N, (f (a + (↑i : ℝ) * h) + f (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)) =
  h * ((f a + f (a + (↑N : ℝ) * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))
Tactic: simp_rw [trapezoidal_integral_one, add_sub_add_left_eq_sub, ← sub_mul, trapezoidal_integral,
    add_sub_cancel_left, one_mul, ← mul_sum, ← mul_div, show N * (h / N) = h by field]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 * ∑ i ∈ Finset.range N, (f (a + (↑i : ℝ) * h) + f (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)) =
    h * ((f a + f (a + (↑N : ℝ) * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))
have rw : h / 2 *
    (f (a + (↑0 : ℝ) * h) + f (a + HAdd.hAdd (α := ℝ) (↑(N - 1) : ℝ) 1 * h) +
      ∑ x ∈ Finset.range (N - 1), (f (a + (↑(x + 1) : ℝ) * h) + f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))) =
  h * ((f a + f (a + (↑N : ℝ) * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))
Tactic: rw [sum_add_distrib, ← Nat.sub_one_add_one_eq_of_pos N_nonzero, sum_range_succ', sum_range_succ,
    add_add_add_comm, ← sum_add_distrib, add_comm, Nat.sub_one_add_one_eq_of_pos N_nonzero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 *
      (f (a + (↑0 : ℝ) * h) + f (a + HAdd.hAdd (α := ℝ) (↑(N - 1) : ℝ) 1 * h) +
        ∑ x ∈ Finset.range (N - 1), (f (a + (↑(x + 1) : ℝ) * h) + f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))) =
    h * ((f a + f (a + (↑N : ℝ) * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))
have simp_rw : h / 2 *
    (f (a + (↑0 : ℝ) * h) + f (a + (HSub.hSub (α := ℝ) (↑N : ℝ) 1 + 1) * h) +
      HMul.hMul (α := ℝ) 2 (∑ i ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h))) =
  h * ((f a + f (a + (↑N : ℝ) * h)) / 2 + ∑ x ∈ Finset.range (N - 1), f (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h))
Tactic: simp_rw [Nat.cast_sub N_nonzero, Nat.cast_add, Nat.cast_one, ← two_mul, ← mul_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h) =
    trapezoidal_integral f (N + 1) a (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
have rw : trapezoidal_integral f N a (a + (↑N : ℝ) * h) + trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
  trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
Tactic: rw [← Nat.cast_add_one, ← sum_trapezoidal_integral_adjacent_intervals N_nonzero,
      ← sum_trapezoidal_integral_adjacent_intervals (Nat.add_pos_left N_nonzero 1),
      sum_range_succ, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
rw :
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) + trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h) =
    trapezoidal_integral f (N + 1) a (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
have rw₁ : ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
    trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
  trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
Tactic: rw [← Nat.cast_add_one, ← sum_trapezoidal_integral_adjacent_intervals N_nonzero,
      ← sum_trapezoidal_integral_adjacent_intervals (Nat.add_pos_left N_nonzero 1),
      sum_range_succ, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
rw :
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) + trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
rw₁ :
  ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h) =
    trapezoidal_integral f (N + 1) a (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
have rw₂ : ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
    trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
  ∑ i ∈ Finset.range (N + 1), trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)
Tactic: rw [← Nat.cast_add_one, ← sum_trapezoidal_integral_adjacent_intervals N_nonzero,
      ← sum_trapezoidal_integral_adjacent_intervals (Nat.add_pos_left N_nonzero 1),
      sum_range_succ, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
rw :
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) + trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
rw₁ :
  ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
rw₂ :
  ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    ∑ i ∈ Finset.range (N + 1), trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h) =
    trapezoidal_integral f (N + 1) a (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
have rw₃ : ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
    trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
  ∑ x ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑x : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h) +
    trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
Tactic: rw [← Nat.cast_add_one, ← sum_trapezoidal_integral_adjacent_intervals N_nonzero,
      ← sum_trapezoidal_integral_adjacent_intervals (Nat.add_pos_left N_nonzero 1),
      sum_range_succ, Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule (goal)
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
rw :
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) + trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
rw₁ :
  ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    trapezoidal_integral f (N + 1) a (a + (↑(N + 1) : ℝ) * h)
rw₂ :
  ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    ∑ i ∈ Finset.range (N + 1), trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h)
rw₃ :
  ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + (↑(N + 1) : ℝ) * h) =
    ∑ x ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑x : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) +
      trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h) =
    trapezoidal_integral f (N + 1) a (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
have rw₄ : ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) +
    trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h) =
  ∑ x ∈ Finset.range N, trapezoidal_integral f 1 (a + (↑x : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h) +
    trapezoidal_integral f 1 (a + (↑N : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * h)
Tactic: rw [← Nat.cast_add_one, ← sum_trapezoidal_integral_adjacent_intervals N_nonzero,
      ← sum_trapezoidal_integral_adjacent_intervals (Nat.add_pos_left N_nonzero 1),
      sum_range_succ, Nat.cast_add_one]
-- 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)
⊢ ∑ i ∈ Finset.range N,
      (trapezoidal_integral f 1 (a + (↑i : ℝ) * h) (a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h) -
        ∫ (x : ℝ) in a + (↑i : ℝ) * h..a + HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * h, f x) =
    trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
have rw : trapezoidal_integral f N a (a + (↑N : ℝ) * h) -
    ∑ x ∈ Finset.range N, ∫ (x : ℝ) in a + (↑x : ℝ) * h..a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h, f x =
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
Tactic: rw [sum_sub_distrib, sum_trapezoidal_integral_adjacent_intervals N_nonzero]
-- 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)
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) -
      ∑ x ∈ Finset.range N, ∫ (x : ℝ) in a + (↑x : ℝ) * h..a + HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 * h, f x =
    trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
have norm_cast : trapezoidal_integral f N a (a + (↑N : ℝ) * h) -
    ∑ x ∈ Finset.range N, ∫ (x : ℝ) in a + (↑x : ℝ) * h..a + (↑(x + 1) : ℝ) * h, f x =
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
Tactic: norm_cast
-- 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)
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) -
      ∑ x ∈ Finset.range N, ∫ (x : ℝ) in a + (↑x : ℝ) * h..a + (↑(x + 1) : ℝ) * h, f x =
    trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
have rw : trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a + (↑0 : ℝ) * h..a + (↑N : ℝ) * h, f x =
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
Tactic: rw [sum_integral_adjacent_intervals]
-- 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)
rw :
  trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a + (↑0 : ℝ) * h..a + (↑N : ℝ) * h, f x =
    trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
⊢ trapezoidal_integral f N a (a + (↑N : ℝ) * h) -
      ∑ x ∈ Finset.range N, ∫ (x : ℝ) in a + (↑x : ℝ) * h..a + (↑(x + 1) : ℝ) * h, f x =
    trapezoidal_integral f N a (a + (↑N : ℝ) * h) - ∫ (x : ℝ) in a..a + (↑N : ℝ) * h, f x
have rw₁ : ∀ k < N, IntervalIntegrable f volume (a + (↑k : ℝ) * h) (a + (↑(k + 1) : ℝ) * h)
Tactic: rw [sum_integral_adjacent_intervals]
-- 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
⊢ IntervalIntegrable f volume (a + (↑k : ℝ) * h) (a + (↑(k + 1) : ℝ) * h)
have suffices : ∀ {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
Tactic: suffices ∀ {k : ℕ}, k ≤ N → a + k * h ∈ [[a, a + N * h]] from
      IntervalIntegrable.mono h_f_int (Set.uIcc_subset_uIcc (this hk.le) (this hk)) le_rfl
-- 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
⊢ ∀ {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
have inl : ∀ (h_neg : h ≤ 0) {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
Tactic: rcases le_total h 0 with h_neg | h_pos