-- 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 hf.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)
x : ℝ
hx : x ∈ Icc ↑a ↑b
y : ℝ
hy : y ∈ Icc ↑a ↑b
hxy : x ≤ y
⊢ y - 1 ∈ Icc (↑a - 1) (↑b - 1)

Tactic:
simpa using hy

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
⊢ ↑a - 1 ∈ Icc (↑a - 1) (↑b - 1)

Tactic:
simp [hab]

Result:
no goals

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

Tactic:
exact I2

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
⊢ ↑a - 1 ≤ x - 1

Tactic:
simpa using I2.1

Result:
no goals

Proof state:
case hf.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)
x : ℝ
hx : x ∈ Icc ↑a ↑b
y : ℝ
hy : y ∈ Icc ↑a ↑b
hxy : x ≤ y
⊢ x - 1 ∈ Icc (↑a - 1) (↑b - 1)

Tactic:
simpa using hx

Result:
no goals

Proof state:
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
⊢ a ≤ i ∧ i ≤ b

Tactic:
exact ⟨hi.1, hi.2.le⟩

Result:
no goals

Proof state:
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 + 1 ≤ ↑b

Tactic:
norm_cast

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 + 1 ≤ b

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

Tactic:
simp only [mem_Icc, Nat.cast_le]

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
⊢ a ≤ i ∧ i ≤ b

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 ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
intro i hi x hx

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 : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : x ∈ Ico ↑i ↑(i + 1)
⊢ f x * g (x - 1) ≤ 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
⊢ g (x - 1) ≤ g ↑i

Tactic:
apply hg

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
⊢ x - 1 ∈ Icc (↑a - 1) (↑b - 1)

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 - 1) (↑b - 1)

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
⊢ x - 1 ≤ ↑i

Proof state:
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 + 1 ≤ b

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
I0 : ↑i ≤ ↑b - 1
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

Tactic:
have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) := by
  simp only [mem_Icc, tsub_le_iff_right]
  exact ⟨by norm_cast; omega, I0⟩

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
I1 : ↑i ∈ Icc (↑a - 1) (↑b - 1)
⊢ f x * g (x - 1) ≤ f ↑i * g ↑i

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:
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
⊢ i + 1 ≤ b

Proof state:
case h.b0
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 ≤ f ↑i

Tactic:
apply fpos.trans

Result:
case h.b0
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 ↑b ≤ f ↑i

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
⊢ g (↑a - 1) ≤ g (x - 1)

Tactic:
apply hg (by simp [hab]) (by simpa using I2) (by simpa using I2.1)

Result:
no goals