have l5 x (hx : x ∈ Ioc x₀ (x₀ + 1)) : (fun x ↦ f (x₀ + 1)) x ≤ f x := by
  rcases hx with ⟨hx1, hx2⟩
  refine hf ⟨hx1, by linarith⟩ ⟨by linarith, by linarith⟩ hx2
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x
case succ
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x₀ : ℝ
f : ℝ → ℝ
n : ℕ
hfi : IntegrableOn f (Icc x₀ (x₀ + ↑(n + 1))) volume
hf : AntitoneOn f (Ioc x₀ (x₀ + (↑n + 1)))
this : Finset.range (n + 1) = {0} ∪ Finset.Ico 1 (n + 1)
l4 : IntervalIntegrable f volume x₀ (x₀ + 1)
l5 : ∀ x ∈ Ioc x₀ (x₀ + 1), (fun x => f (x₀ + 1)) x ≤ f x
⊢ f (x₀ + 1) + ∑ x ∈ Finset.Ico 1 (n + 1), f (x₀ + (↑x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + (↑n + 1), f x