awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
refine : uIcc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
⊢ IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))

Tactic:
refine (hf.mono ?_).intervalIntegrable

Premises used: AntitoneOn.intervalIntegrable, AntitoneOn.mono
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
rw : Icc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))
rw₁ : x₀ + (↑k : ℝ) ≤ x₀ + (↑(k + 1) : ℝ)
⊢ uIcc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
rw [uIcc_of_le]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
ha : x₀ ≤ x₀ + (↑k : ℝ)
hb : x₀ + (↑(k + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
⊢ Icc (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ)) ⊆ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
apply Icc_subset_Icc

Premises used: Set.Icc_subset_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ x₀ ≤ x₀ + (↑k : ℝ)

Tactic:
simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]

Premises used: le_add_iff_nonneg_right, Nat.cast_nonneg
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ x₀ + (↑(k + 1) : ℝ) ≤ x₀ + (↑a : ℝ)

Tactic:
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]

Premises used: Nat.succ_le_of_lt, add_le_add_iff_left, Nat.cast_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
k : ℕ
hk : k < a
⊢ x₀ + (↑k : ℝ) ≤ x₀ + (↑(k + 1) : ℝ)

Tactic:
simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]

Premises used: add_le_add_iff_left, Nat.le_succ, Nat.cast_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))

Tactic:
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) := by
    intro k hk
    refine (hf.mono ?_).intervalIntegrable
    rw [uIcc_of_le]
    · apply Icc_subset_Icc
      · simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
      · simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
    · simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in x₀ + (↑0 : ℝ)..x₀ + (↑a : ℝ), f x)
    (∑ k ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑k : ℝ)..x₀ + (↑(k + 1) : ℝ), f x)

Tactic:
(intervalIntegral.sum_integral_adjacent_intervals hint).symm

Premises used: intervalIntegral.sum_integral_adjacent_intervals, Eq.symm
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
h : x₀ = x₀ + (↑0 : ℝ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)

Tactic:
convert! (intervalIntegral.sum_integral_adjacent_intervals hint).symm

Premises used: intervalIntegral.sum_integral_adjacent_intervals, Eq.symm
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ x₀ = x₀ + (↑0 : ℝ)

Tactic:
simp only [Nat.cast_zero, add_zero]

Premises used: Nat.cast_zero, add_zero
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
h :
  ∀ (i : ℕ) (hi : i ∈ Finset.range a),
    LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
      (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))

Tactic:
gcongr with i hi
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
⊢ i < a

Tactic:
have ia : i < a := Finset.mem_range.1 hi
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ x₀ + (↑i : ℝ) ≤ x₀ + (↑(i + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f (x₀ + (↑i : ℝ))) volume (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
h : ∀ (x : ℝ) (hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))), f x ≤ f (x₀ + (↑i : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))

Tactic:
refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_

Premises used: intervalIntegral.integral_mono_on
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
apply : x₀ + (↑i : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))
apply₁ : x ∈ Icc x₀ (x₀ + (↑a : ℝ))
⊢ f x ≤ f (x₀ + (↑i : ℝ))

Tactic:
apply hf _ _ hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x₀ + (↑i : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left,
          Nat.cast_le, and_self_iff]

Premises used: le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left, LT.lt.le, Set.mem_Icc, and_self_iff, Nat.cast_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x₀ ≤ x₀ + (↑i : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
refine : x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
⊢ x ∈ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
refine mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 ?_⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, Set.mem_Icc, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)

Tactic:
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]

Premises used: Nat.succ_le_of_lt, add_le_add_iff_left, Nat.cast_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ Eq (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
    (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
x :
  Eq (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
x₁ :
  LE.le (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
x₂ :
  Eq (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
    (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))

Tactic:
calc
    ∫ x in x₀..x₀ + a, f x = ∑ i ∈ Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x := by
      convert! (intervalIntegral.sum_integral_adjacent_intervals hint).symm
      simp only [Nat.cast_zero, add_zero]
    _ ≤ ∑ i ∈ Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) := by
      gcongr with i hi
      have ia : i < a := Finset.mem_range.1 hi
      refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_
      apply hf _ _ hx.1
      · simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left,
          Nat.cast_le, and_self_iff]
      · refine mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 ?_⟩
        simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
    _ = ∑ i ∈ Finset.range a, f (x₀ + i) := by simp

Premises used: Finset.range
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
rw :
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x) (∑ x ∈ Finset.Ico a b, f (↑x : ℝ))

Tactic:
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]

Premises used: Nat.cast_add, Nat.sub_add_cancel, Eq.symm
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
a₂ : ∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ)
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))

Tactic:
congr
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : fun (x : ℝ) ↦ f x
a₂ : (↑a : ℝ)
a₃ : HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ)
a₄ : volume
| ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x

Tactic:
congr
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| fun (x : ℝ) ↦ f x

Tactic:
· skip
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| (↑a : ℝ)

Tactic:
· skip
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)
| HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)

Tactic:
· skip
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| volume

Tactic:
· skip
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : Finset.Ico a (b - a + a)
a₂ : fun (x : ℕ) ↦ f (↑x : ℝ)
| ∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ)

Tactic:
congr
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : a
a₂ : b - a + a
| Finset.Ico a (b - a + a)

Tactic:
congr
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : 0 + a
| a

Tactic:
rw [← zero_add a]

Premises used: zero_add
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : 0 + a
a₂ : b - a + a
a₃ : fun (x : ℕ) ↦ f (↑x : ℝ)
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))

Tactic:
congr
    congr
    · skip
    · skip
    rw [add_comm]
    · skip
    · skip
    congr
    congr
    rw [← zero_add a]

Premises used: zero_add, add_comm
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
conv :
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.Ico (0 + a) (b - a + a), f (↑x : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))

Tactic:
conv =>
    congr
    congr
    · skip
    · skip
    rw [add_comm]
    · skip
    · skip
    congr
    congr
    rw [← zero_add a]

Premises used: zero_add, add_comm
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
rw :
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.Ico (0 + a) (b - a + a), f (↑x : ℝ))

Tactic:
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]

Premises used: Finset.sum_Ico_add, Nat.Ico_zero_eq_range
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
rhs : ∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ)
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))

Tactic:
rhs
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
s : Finset.range (b - a)
f₁ : fun (x : ℕ) ↦ f (↑(a + x) : ℝ)
| ∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ)

Tactic:
congr
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| Finset.range (b - a)

Tactic:
· skip
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
f₁ : ∀ (x : ℕ), f (↑(a + x) : ℝ)
| fun (x : ℕ) ↦ f (↑(a + x) : ℝ)

Tactic:
ext
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
x : ℕ
f₁ : f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ))
| f (↑(a + x) : ℝ)

Tactic:
rw [Nat.cast_add]

Premises used: Nat.cast_add
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
f₁ : ∀ (x : ℕ), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ))
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))

Tactic:
rhs
    congr
    · skip
    ext
    rw [Nat.cast_add]

Premises used: Nat.cast_add
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
conv :
  LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))

Tactic:
conv =>
    rhs
    congr
    · skip
    ext
    rw [Nat.cast_add]

Premises used: Nat.cast_add
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hf₁ : AntitoneOn f (Icc (↑a : ℝ) (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ)))

Tactic:
apply AntitoneOn.integral_le_sum

Premises used: AntitoneOn.integral_le_sum
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ AntitoneOn f (Icc (↑a : ℝ) (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)))

Tactic:
simp only [hf, hab, Nat.cast_sub, add_sub_cancel]

Premises used: Nat.cast_sub, add_sub_cancel
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ Eq (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ)))
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
apply :
  ∀ (i : ℕ) (hi : i ∈ Finset.range a),
    LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))
      (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)

Tactic:
apply Finset.sum_le_sum fun i hi => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
⊢ i + 1 ≤ a

Tactic:
have ia : i + 1 ≤ a := Finset.mem_range.1 hi
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ x₀ + (↑i : ℝ) ≤ x₀ + (↑(i + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f (x₀ + (↑(i + 1) : ℝ))) volume (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
refine : ∀ (x : ℝ) (hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))), f (x₀ + (↑(i + 1) : ℝ)) ≤ f x
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)

Tactic:
refine intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => ?_

Premises used: intervalIntegral.integral_mono_on
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
apply : x ∈ Icc x₀ (x₀ + (↑a : ℝ))
apply₁ : x₀ + (↑(i + 1) : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))
⊢ f (x₀ + (↑(i + 1) : ℝ)) ≤ f x

Tactic:
apply hf _ _ hx.2

Premises used: And.right
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x ∈ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
mem_Icc.2 ⟨le_trans (le_add_of_nonneg_right (Nat.cast_nonneg _)) hx.1,
          le_trans hx.2 ?_⟩

Premises used: Iff.mpr, Nat.cast_nonneg, le_add_of_nonneg_right, And.right, And.left, And.intro, Set.mem_Icc, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
refine : x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
⊢ x ∈ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
refine mem_Icc.2 ⟨le_trans (le_add_of_nonneg_right (Nat.cast_nonneg _)) hx.1,
          le_trans hx.2 ?_⟩

Premises used: Iff.mpr, le_add_of_nonneg_right, And.right, And.left, And.intro, Set.mem_Icc, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)

Tactic:
simp only [Nat.cast_le, add_le_add_iff_left, ia]

Premises used: add_le_add_iff_left, Nat.cast_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x₀ + (↑(i + 1) : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
mem_Icc.2 ⟨le_add_of_nonneg_right (Nat.cast_nonneg _), ?_⟩

Premises used: Iff.mpr, Nat.cast_nonneg, le_add_of_nonneg_right, And.intro, Set.mem_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
refine : x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
⊢ x₀ + (↑(i + 1) : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))

Tactic:
refine mem_Icc.2 ⟨le_add_of_nonneg_right (Nat.cast_nonneg _), ?_⟩

Premises used: Iff.mpr, le_add_of_nonneg_right, And.intro, Set.mem_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))
⊢ x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)

Tactic:
simp only [add_le_add_iff_left, Nat.cast_le, ia]

Premises used: add_le_add_iff_left, Nat.cast_le