-- Mathlib/Analysis/SumIntegralComparisons.lean
lemma integral_le_sum_mul_Ico_of_antitone_monotone
    (hab : a ≤ b) (hf : AntitoneOn f (Icc a b)) (hg : MonotoneOn g (Icc (a - 1) (b - 1)))
    (fpos : 0 ≤ f b) (gpos : 0 ≤ g (a - 1)) :
    ∫ x in a..b, f x * g (x - 1) ≤ ∑ i ∈ Finset.Ico a b, f i * g i

Proof state:
case h.h₁
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ f x ≤ f ↑i

Tactic:
apply hf

Result:
case h.h₁.x
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑i ∈ Icc ↑a ↑b

case h.h₁.x
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ x ∈ Icc ↑a ↑b

case h.h₁.a
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑i ≤ x

Proof state:
case hf
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ MemLp (fun x => g (x - 1)) ⊤ (volume.restrict (Icc ↑a ↑b))

Tactic:
apply MonotoneOn.memLp_isCompact isCompact_Icc

Result:
case hf
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ MonotoneOn (fun x => g (x - 1)) (Icc ↑a ↑b)

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ i + 1 ≤ b

Tactic:
omega

Result:
no goals

Proof state:
case hf
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ MonotoneOn (fun x => g (x - 1)) (Icc ↑a ↑b)

Tactic:
intro x hx y hy hxy

Result:
case hf
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
x : ℝ
hx : x ∈ Icc ↑a ↑b
y : ℝ
hy : y ∈ Icc ↑a ↑b
hxy : x ≤ y
⊢ (fun x => g (x - 1)) x ≤ (fun x => g (x - 1)) y

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ x ∈ Icc ↑a ↑b

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

Result:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ ↑i + 1 ≤ ↑b

Proof state:
case h.c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ 0 ≤ g (x - 1)

Tactic:
apply gpos.trans

Result:
case h.c0
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ g (↑a - 1) ≤ g (x - 1)

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ a ≤ i + 1

Tactic:
omega

Result:
no goals

Proof state:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
have I0 : (i : ℝ) ≤ b - 1 := by
  simp only [le_sub_iff_add_le]
  norm_cast
  omega

Result:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

Proof state:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

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

Result:
case h
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

Proof state:
case h.h₁.a
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑i ≤ x

Tactic:
exact hx.1

Result:
no goals

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
I2 : x ∈ Icc ↑a ↑b
⊢ ↑b ∈ Icc ↑a ↑b

Tactic:
simpa using hab

Result:
no goals

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ ↑a ≤ ↑i + 1 ∧ ↑i ≤ ↑b - 1

Tactic:
exact ⟨by norm_cast; omega, I0⟩

Result:
no goals

Proof state:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ ↑a ≤ ↑i + 1

Tactic:
norm_cast

Result:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : a ≤ i ∧ i < b
I0 : ↑i ≤ ↑b - 1
⊢ a ≤ i + 1

Proof state:
case hφ
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ Integrable f (volume.restrict (Icc ↑a ↑b))

Tactic:
exact hf.integrableOn_isCompact isCompact_Icc

Result:
no goals

Proof state:
case hf.a
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
x : ℝ
hx : x ∈ Icc ↑a ↑b
y : ℝ
hy : y ∈ Icc ↑a ↑b
hxy : x ≤ y
⊢ x - 1 ≤ y - 1

Tactic:
simpa using hxy

Result:
no goals