awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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 : ℝ)))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x) (∑ i ∈ Finset.range a, f (x₀ + (↑i : ℝ)))
have x₂ : Eq (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑i : ℝ)))
  (∑ 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
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x) (∑ x ∈ Finset.Ico a b, f (↑x : ℝ))
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
  (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
Tactic: rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
have a₁ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(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 : ℝ))
have a₂ : ∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
have a₁ : fun (x : ℝ) ↦ f x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : fun (x : ℝ) ↦ f x
| ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
have a₂ : (↑a : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : fun (x : ℝ) ↦ f x
a₂ : (↑a : ℝ)
| ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
have a₃ : HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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 : ℝ)
| ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
have a₄ : volume
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ)
have a₁ : HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| ∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ)
have a₁ : Finset.Ico a (b - a + a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : Finset.Ico a (b - a + a)
| ∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ)
have a₂ : fun (x : ℕ) ↦ f (↑x : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| Finset.Ico a (b - a + a)
have a₁ : a
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : a
| Finset.Ico a (b - a + a)
have a₂ : b - a + a
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| a
have a₁ : 0 + a
Tactic: rw [← zero_add a]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
have a₁ : 0 + a
Tactic: congr
    congr
    · skip
    · skip
    rw [add_comm]
    · skip
    · skip
    congr
    congr
    rw [← zero_add a]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : 0 + a
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
have a₂ : b - a + a
Tactic: congr
    congr
    · skip
    · skip
    rw [add_comm]
    · skip
    · skip
    congr
    congr
    rw [← zero_add a]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : 0 + a
a₂ : b - a + a
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
have a₃ : fun (x : ℕ) ↦ f (↑x : ℝ)
Tactic: congr
    congr
    · skip
    · skip
    rw [add_comm]
    · skip
    · skip
    congr
    congr
    rw [← zero_add a]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
    (∑ x ∈ Finset.Ico a (b - a + a), f (↑x : ℝ))
have conv : LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
  (∑ x ∈ Finset.Ico (0 + a) (b - a + a), f (↑x : ℝ))
Tactic: conv =>
    congr
    congr
    · skip
    · skip
    rw [add_comm]
    · skip
    · skip
    congr
    congr
    rw [← zero_add a]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.Ico (0 + a) (b - a + a), f (↑x : ℝ))
have rw : LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
  (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))
Tactic: rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))
have rhs : ∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ)
Tactic: rhs
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| ∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ)
have s : Finset.range (b - a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
s : Finset.range (b - a)
| ∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ)
have f₁ : fun (x : ℕ) ↦ f (↑(a + x) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| fun (x : ℕ) ↦ f (↑(a + x) : ℝ)
have f₁ : ∀ (x : ℕ), f (↑(a + x) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
x : ℕ
| f (↑(a + x) : ℝ)
have f₁ : f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ))
Tactic: rw [Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))
have f₁ : ∀ (x : ℕ), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ))
Tactic: rhs
    congr
    · skip
    ext
    rw [Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (↑(a + x) : ℝ))
have conv : LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
  (∑ x ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ)))
Tactic: conv =>
    rhs
    congr
    · skip
    ext
    rw [Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
    (∑ x ∈ Finset.range (b - a), f (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑x : ℝ)))
have hf₁ : AntitoneOn f (Icc (↑a : ℝ) (HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ)))
Tactic: apply AntitoneOn.integral_le_sum
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
have hint : ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ 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)
have 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)
Tactic: apply Finset.sum_le_sum fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (hypothesis)
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
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
have ia : i + 1 ≤ a
Tactic: have ia : i + 1 ≤ a := Finset.mem_range.1 hi
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f (x₀ + (↑(i + 1) : ℝ)))
    (∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
have refine : ∀ (x : ℝ) (hx : x ∈ Icc (x₀ + (↑i : ℝ)) (x₀ + (↑(i + 1) : ℝ))), f (x₀ + (↑(i + 1) : ℝ)) ≤ f x
Tactic: refine intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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) : ℝ))
⊢ f (x₀ + (↑(i + 1) : ℝ)) ≤ f x
have apply : x ∈ Icc x₀ (x₀ + (↑a : ℝ))
Tactic: apply hf _ _ hx.2
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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 : ℝ))
⊢ f (x₀ + (↑(i + 1) : ℝ)) ≤ f x
have apply₁ : x₀ + (↑(i + 1) : ℝ) ∈ Icc x₀ (x₀ + (↑a : ℝ))
Tactic: apply hf _ _ hx.2
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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 : ℝ))
have refine : x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
Tactic: refine mem_Icc.2 ⟨le_trans (le_add_of_nonneg_right (Nat.cast_nonneg _)) hx.1,
          le_trans hx.2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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 : ℝ))
have refine : x₀ + (↑(i + 1) : ℝ) ≤ x₀ + (↑a : ℝ)
Tactic: refine mem_Icc.2 ⟨le_add_of_nonneg_right (Nat.cast_nonneg _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + (↑a : ℝ)))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + (↑k : ℝ)) (x₀ + (↑(k + 1) : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
have 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) : ℝ)))
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]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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) : ℝ)))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
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)
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.range a, f (x₀ + (↑(i + 1) : ℝ))) (∫ (x : ℝ) in x₀..x₀ + (↑a : ℝ), f x)
have i₂ : Eq (α := ℝ) (∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + (↑i : ℝ)..x₀ + (↑(i + 1) : ℝ), f x)
  (∫ (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]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a b, f (↑(i + 1) : ℝ)) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x)
have rw : LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
  (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
Tactic: rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
have a₁ : ∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : ∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ)
| LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
have a₂ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| ∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ)
have a₁ : Finset.Ico a (b - a + a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
a₁ : Finset.Ico a (b - a + a)
| ∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ)
have a₂ : fun (i : ℕ) ↦ f (↑(i + 1) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x
have a₁ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
have a₁ : ∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x
Tactic: congr
    congr
    congr
    rw [← zero_add a]
    · skip
    · skip
    · skip
    rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico a (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑(b - a) : ℝ) (↑a : ℝ), f x)
have conv : LE.le (α := ℝ) (∑ i ∈ Finset.Ico (0 + a) (b - a + a), f (↑(i + 1) : ℝ))
  (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
Tactic: conv =>
    congr
    congr
    congr
    rw [← zero_add a]
    · skip
    · skip
    · skip
    rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
⊢ LE.le (α := ℝ) (∑ i ∈ Finset.Ico (0 + a) (b - a + a), f (↑(i + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
have rw : LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
  (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
Tactic: rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| LE.le (α := ℝ) (∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ))
    (∫ (x : ℝ) in (↑a : ℝ)..HAdd.hAdd (α := ℝ) (↑a : ℝ) (↑(b - a) : ℝ), f x)
have lhs : ∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Analysis.SumIntegralComparisons (goal)
Goal:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
| ∑ x ∈ Finset.range (b - a), f (↑(a + x + 1) : ℝ)
have s : Finset.range (b - a)
Tactic: congr