awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := ℝ) (∑ k ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑k : ℝ)..x₀ + (↑(k + 1) : ℝ), f x)
    (∫ (x : ℝ) in x₀ + (↑0 : ℝ)..x₀ + (↑a : ℝ), f x)

Tactic:
intervalIntegral.sum_integral_adjacent_intervals hint

Premises used: intervalIntegral.sum_integral_adjacent_intervals
-- 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 :
  Eq (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ)))
    (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))
i₁ :
  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)
i₂ :
  Eq (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
    (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)

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

Premises used: Nat.cast, Finset.range, HAdd.hAdd, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
rw :
  LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑(i + 1) : ℝ)) (∫ (x : ℝ) in (↑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₁ : ∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ)
a₂ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
| LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (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 : ℝ))
a₁ : Finset.Ico a (b - a + a)
a₂ : fun (i : ℕ) ↦ f (↑(i + 1) : ℝ)
| ∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ)

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

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

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

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

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 : ℝ))
a₁ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x
| LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)

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

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 (α := ℝ) (∑ i ∈ Finset.Ico (0 + a) (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)

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

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 ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico (0 + a) (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - 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 : ℝ))
lhs : ∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ)
| LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)

Tactic:
lhs
-- 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 + 1) : ℝ)
| ∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ)

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

Tactic:
congr
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| 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 + 1) : ℝ)
| fun (x : ℕ) ↦ f (↑(a + x + 1) : ℝ)

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 + 1) : ℝ))
| f (↑(a + x + 1) : ℝ)

Tactic:
rw [add_assoc, Nat.cast_add]

Premises used: add_assoc, 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 + 1) : ℝ))
| LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)

Tactic:
lhs
    congr
    congr
    · skip
    ext
    rw [add_assoc, Nat.cast_add]

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

Tactic:
conv =>
    lhs
    congr
    congr
    · skip
    ext
    rw [add_assoc, Nat.cast_add]

Premises used: add_assoc, 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 ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(x + 1) : ℝ)))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)

Tactic:
apply AntitoneOn.sum_le_integral

Premises used: AntitoneOn.sum_le_integral
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
rw : LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x) (∑ x ∈ Finset.range a, -f (x₀ + (↑x : ℝ)))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Premises used: Finset.sum_neg_distrib, intervalIntegral.integral_neg, neg_le_neg_iff
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x) (∑ x ∈ Finset.range a, -f (x₀ + (↑x : ℝ)))

Tactic:
hf.neg.integral_le_sum

Premises used: MonotoneOn.neg, AntitoneOn.integral_le_sum
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x) (∑ x ∈ Finset.range a, -f (x₀ + (↑x : ℝ)))

Tactic:
exact hf.neg.integral_le_sum

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

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Premises used: Finset.sum_neg_distrib, intervalIntegral.integral_neg, neg_le_neg_iff
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), -f x) (∑ x ∈ Finset.Ico a b, -f (↑x : ℝ))

Tactic:
hf.neg.integral_le_sum_Ico hab

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

Tactic:
exact hf.neg.integral_le_sum_Ico hab

Premises used: MonotoneOn.neg, AntitoneOn.integral_le_sum_Ico
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
rw : LE.le (α := ℝ) (∑ x ∈ Finset.range a, -f (x₀ + (↑(x + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ)))

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Premises used: Finset.sum_neg_distrib, intervalIntegral.integral_neg, neg_le_neg_iff
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range a, -f (x₀ + (↑(x + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x)

Tactic:
hf.neg.sum_le_integral

Premises used: MonotoneOn.neg, AntitoneOn.sum_le_integral
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.range a, -f (x₀ + (↑(x + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), -f x)

Tactic:
exact hf.neg.sum_le_integral

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

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Premises used: Finset.sum_neg_distrib, intervalIntegral.integral_neg, neg_le_neg_iff
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ x ∈ Finset.Ico a b, -f (↑(x + 1) : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), -f x)

Tactic:
hf.neg.sum_le_integral_Ico hab

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

Tactic:
exact hf.neg.sum_le_integral_Ico hab

Premises used: MonotoneOn.neg, AntitoneOn.sum_le_integral_Ico
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
h :
  ∀ i ∈ Ico a b,
    ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)
hg₁ : IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ) * g (↑i : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x * g (x - 1))

Tactic:
apply sum_Ico_le_integral_of_le (f := fun x ↦ f x * g x) hab

Premises used: sum_Ico_le_integral_of_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi

Premises used: Set.mem_Ico, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
hx₁ : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ a ≤ i ∧ i < b

Tactic:
simp only [Nat.cast_add, Nat.cast_one, mem_Ico] at hx hi

Premises used: Set.mem_Ico, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
simp : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
⊢ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
simp only [le_sub_iff_add_le]

Premises used: le_sub_iff_add_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
norm_cast : i + 1 ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ i + 1 ≤ b

Tactic:
lia
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
have I0 : (i : ℝ) ≤ b - 1 := by
      simp only [le_sub_iff_add_le]
      norm_cast
      lia
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
simp : (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ∧ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simp only [mem_Icc, tsub_le_iff_right]

Premises used: tsub_le_iff_right, Set.mem_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
norm_cast : a ≤ i + 1
⊢ (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ a ≤ i + 1

Tactic:
lia
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ∧ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
exact ⟨by norm_cast; lia, I0⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) := by
      simp only [mem_Icc, tsub_le_iff_right]
      exact ⟨by norm_cast; lia, I0⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

Tactic:
⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.Icc, And.right, And.left, And.intro, LE.le.trans, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
refine : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

Tactic:
refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
norm_cast : i + 1 ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ i + 1 ≤ b

Tactic:
lia
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

Tactic:
have I2 : x ∈ Icc (a : ℝ) b := by
      refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
      norm_cast
      lia
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f (↑i : ℝ) ≤ f x
h₁ : g (↑i : ℝ) ≤ g (x - 1)
h₂ : 0 ≤ g (↑i : ℝ)
h₃ : 0 ≤ f x
⊢ f (↑i : ℝ) * g (↑i : ℝ) ≤ f x * g (x - 1)

Tactic:
apply mul_le_mul

Premises used: mul_le_mul