awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
x : ℝ
h : x ∈ Icc b (b + c)
⊢ x ≤ b + c

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
grw : ∫ (u : ℝ) in b..b + c, f (b + c) ≤ c * f (b + c)
⊢ ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)

Tactic:
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])]

Premises used: intervalIntegral.integral_mono_on, IntervalIntegrable.mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ ∫ (u : ℝ) in b..b + c, f (b + c) ≤ c * f (b + c)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ ∫ (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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
linarith : a + c < a → 0 - c + (a + c - a) = 0
⊢ a ≤ a + c

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f a) volume a (a + c)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ uIcc a (a + c) ⊆ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
a₁ : a ≤ x_1
⊢ (fun (x : ℝ) ↦ f a) x_1 ≤ f x_1

Tactic:
apply hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ a ∈ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ x ∈ uIcc a (b + c)

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
⊢ a ≤ x

Tactic:
grind [uIcc]

Premises used: Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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)
grw : c * f a ≤ ∫ (u : ℝ) in a..a + c, f a
⊢ c * f a ≤ ∫ (x : ℝ) in a..a + c, f x

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])]

Premises used: intervalIntegral.integral_mono_on, IntervalIntegrable.mono_set
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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 ≤ ∫ (u : ℝ) in a..a + c, f a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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

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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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
inr : c⁻¹ * (c * f (b + c) - c * f a) ≤ f (b + c) - f a
⊢ c⁻¹ * HSub.hSub (α := ℝ) (∫ (x : ℝ) in b..b + c, f x) (∫ (x : ℝ) in a..a + c, f x) ≤ f (b + c) - f a

Tactic:
grw [fU, ← fL]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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
inr : f (b + c) - f a ≤ f (b + c) - f a
⊢ c⁻¹ * (c * f (b + c) - c * f a) ≤ f (b + c) - f a

Tactic:
field_simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
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
⊢ f (b + c) - f a ≤ f (b + c) - f a

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
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 : ℝ)))
⊢ (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 : ℝ))))

Tactic:
rw [neg_mul_eq_neg_mul, neg_div', neg_sub, add_comm (f b) (f a), ← sum_range_reflect]

Premises used: neg_div', neg_sub, Finset.sum_range_reflect, add_comm, neg_mul_eq_neg_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
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 : ℝ)))
⊢ (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:
congr 2
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
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 : ℝ))
⊢ 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:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
e_a : f (a + (↑(N - 1 - 1 - k + 1) : ℝ) * (b - a) / (↑N : ℝ)) = f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))
⊢ f (a + HAdd.hAdd (α := ℝ) (↑(N - 1 - 1 - k) : ℝ) 1 * (b - a) / (↑N : ℝ)) =
    f (b + HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (a - b) / (↑N : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
e_a :
  f (a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ)) =
    f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))
⊢ f (a + (↑(N - 1 - 1 - k + 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]

Premises used: Nat.cast_sub, Finset.mem_range, add_comm, Nat.cast_add, Iff.mp, tsub_tsub, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
e_a :
  a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ) =
    b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ)
⊢ f (a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ)) =
    f (b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
k : ℕ
hk : k ∈ Finset.range (N - 1)
⊢ a + (HSub.hSub (α := ℝ) (↑N : ℝ) (↑(Nat.succ 0) : ℝ) - (↑k.succ : ℝ) + (↑1 : ℝ)) * (b - a) / (↑N : ℝ) =
    b + (↑(k + 1) : ℝ) * (a - b) / (↑N : ℝ)

Tactic:
field
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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)
rw₃ 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
⊢ trapezoidal_integral f N a b - ∫ (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]

Premises used: neg_sub, intervalIntegral.integral_symm, neg_sub_neg, trapezoidal_integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a : ℝ
⊢ trapezoidal_integral f N a a = 0

Tactic:
simp [trapezoidal_integral]

Premises used: trapezoidal_integral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a : ℝ
⊢ trapezoidal_error f N a a = 0

Tactic:
simp [trapezoidal_error]

Premises used: trapezoidal_error
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
a b : ℝ
⊢ trapezoidal_integral f 1 a b = (b - a) / 2 * (f a + f b)

Tactic:
simp [trapezoidal_integral, mul_comm_div]

Premises used: trapezoidal_integral, mul_comm_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ (↑N : ℝ) * (h / (↑N : ℝ)) = h

Tactic:
field
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
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))
⊢ ∑ 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)

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]

Premises used: mul_div, Finset.mul_sum, trapezoidal_integral, add_sub_cancel_left, add_sub_add_left_eq_sub, sub_mul, trapezoidal_integral_one, one_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
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))
⊢ 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:
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]

Premises used: Finset.sum_add_distrib, Nat.sub_one_add_one_eq_of_pos, add_comm, add_add_add_comm, Finset.sum_range_succ', Finset.sum_range_succ
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
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))
⊢ 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:
simp_rw [Nat.cast_sub N_nonzero, Nat.cast_add, Nat.cast_one, ← two_mul, ← mul_sum]

Premises used: Finset.mul_sum, Nat.cast_sub, two_mul, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ 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:
ring_nf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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)
rw₄ 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)
⊢ 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)

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]

Premises used: Nat.add_pos_left, OfNat.ofNat, Nat.cast_add_one, Finset.sum_range_succ, sum_trapezoidal_integral_adjacent_intervals
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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 ∈ 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
⊢ ∑ 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

Tactic:
rw [sum_sub_distrib, sum_trapezoidal_integral_adjacent_intervals N_nonzero]

Premises used: Finset.sum_sub_distrib, sum_trapezoidal_integral_adjacent_intervals
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + (↑N : ℝ) * h)
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
⊢ 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:
norm_cast
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
rw₁ : ∀ k < N, IntervalIntegrable f volume (a + (↑k : ℝ) * h) (a + (↑(k + 1) : ℝ) * 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

Tactic:
rw [sum_integral_adjacent_intervals]

Premises used: intervalIntegral.sum_integral_adjacent_intervals
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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 : ℝ) 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:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
Goal:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + (↑N : ℝ) * h)
k : ℕ
hk : k < N
suffices : ∀ {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
⊢ IntervalIntegrable f volume (a + (↑k : ℝ) * h) (a + (↑(k + 1) : ℝ) * 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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]]
inr : ∀ (h_pos : 0 ≤ h) {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]
⊢ ∀ {k : ℕ}, k ≤ N → a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]

Tactic:
rcases le_total h 0 with h_neg | h_pos

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
⊢ LE.le (α := ℝ) (↑k : ℝ) (↑N : ℝ)

Tactic:
rw [← Nat.cast_le (α := ℝ)] at hk

Premises used: Nat.cast_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
⊢ LE.le (α := ℝ) (↑k : ℝ) (↑N : ℝ)

Tactic:
rw [← Nat.cast_le (α := ℝ)] at hk

Premises used: Nat.cast_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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 : LE.le (α := ℝ) (↑k : ℝ) (↑N : ℝ)
⊢ a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]

Tactic:
simpa [Set.mem_uIcc] using .inr
        ⟨mul_le_mul_of_nonpos_right hk h_neg, mul_nonpos_of_nonneg_of_nonpos k.cast_nonneg h_neg⟩

Premises used: Set.mem_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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 : ℝ)
⊢ 0 ≤ (↑k : ℝ) * h

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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
grw grw₁ : a + (↑N : ℝ) * h ≤ a + (↑N : ℝ) * h
⊢ a + (↑k : ℝ) * h ≤ a + (↑N : ℝ) * h

Tactic:
grw [hk]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
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 : ℝ)
⊢ a + (↑k : ℝ) * h ∈ [[a, a + (↑N : ℝ) * h]]

Tactic:
exact Set.mem_uIcc_of_le (le_add_of_nonneg_right (by positivity)) (by grw [hk])

Premises used: Set.mem_uIcc_of_le, le_add_of_nonneg_right