-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem AntitoneOn.sum_le_integral (hf : AntitoneOn f (Icc x₀ (x₀ + a))) :
    (∑ i ∈ Finset.range a, f (x₀ + (i + 1 : ℕ))) ≤ ∫ x in x₀..x₀ + a, f x

Proof state:
case h₂
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]

Result:
no goals

Proof state:
case h₁
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]

Result:
no goals

Proof state:
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]

Result:
no goals

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x = ∫ (x : ℝ) in x₀..x₀ + ↑a, f x

Tactic:
convert intervalIntegral.sum_integral_adjacent_intervals hint

Result:
case h.e'_3.h.e'_5
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ x₀ = x₀ + ↑0

Proof state:
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:
refine mem_Icc.2 ⟨le_add_of_nonneg_right (Nat.cast_nonneg _), ?_⟩

Result:
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

Proof state:
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]

Result:
no goals

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)

Tactic:
rw [uIcc_of_le]

Result:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)

x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑k ≤ x₀ + ↑(k + 1)

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∀ k < a, IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))

Tactic:
intro k hk

Result:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))

Proof state:
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
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x

Tactic:
have ia : i + 1 ≤ a := Finset.mem_range.1 hi

Result:
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 : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x

Proof state:
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 : ℝ) 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 => ?_

Result:
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

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))

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

Result:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)

Proof state:
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]

Result:
no goals

Proof state:
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:
refine mem_Icc.2 ⟨le_trans (le_add_of_nonneg_right (Nat.cast_nonneg _)) hx.1,
  le_trans hx.2 ?_⟩

Result:
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

Proof state:
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

Result:
no goals

Proof state:
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

Result:
no goals

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ 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 => ?_

Result:
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
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ 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

Result:
no goals

Proof state:
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

Tactic:
apply hf _ _ hx.2

Result:
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)

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)