awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)
h₁ : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h₂ : (↑i : ℝ) ≤ x
⊢ f (↑i : ℝ) ≤ f x

Tactic:
apply hf
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : a ≤ i ∧ i ≤ b
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑i : ℝ)

Tactic:
simp only [mem_Icc, Nat.cast_le]

Premises used: Set.mem_Icc, Nat.cast_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ a ≤ i ∧ i ≤ b

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

Premises used: LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ a ≤ i ∧ i ≤ b

Tactic:
exact ⟨hi.1, hi.2.le⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

Tactic:
I2
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

Tactic:
exact I2
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑i : ℝ) ≤ x

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑i : ℝ) ≤ x

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
h₁ : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
h₂ : x - 1 ≤ (↑i : ℝ)
⊢ g (↑i : ℝ) ≤ g (x - 1)

Tactic:
apply hg
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)
⊢ x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simp only [mem_Icc, tsub_le_iff_right, sub_add_cancel]

Premises used: tsub_le_iff_right, Set.mem_Icc, sub_add_cancel
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)

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

Premises used: LT.lt.le, And.right, And.left, And.intro, LE.le.trans, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
⊢ (↑a : ℝ) ≤ x ∧ x ≤ (↑b : ℝ)

Tactic:
refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : i + 1 ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ i + 1 ≤ b

Tactic:
lia
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
I1
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
exact I1
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ x - 1 ≤ (↑i : ℝ)

Tactic:
simpa [sub_le_iff_le_add] using hx.2.le

Premises used: sub_le_iff_le_add, LT.lt.le, And.right
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : g (HSub.hSub (α := ℝ) (↑b : ℝ) 1) ≤ g (↑i : ℝ)
⊢ 0 ≤ g (↑i : ℝ)

Tactic:
apply gpos.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simp [hab]
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1) ≤ g (↑i : ℝ)

Tactic:
apply hg I1 (by simp [hab]) I0
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : f (↑a : ℝ) ≤ f x
⊢ 0 ≤ f x

Tactic:
apply fpos.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) (↑a : ℝ)

Tactic:
simp [hab]
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
h : (↑a : ℝ) ≤ x
⊢ f (↑a : ℝ) ≤ f x

Tactic:
apply hf (by simp [hab]) I2
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑a : ℝ) ≤ x

Tactic:
le_trans (mod_cast hi.1) hx.1

Premises used: And.left, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
i : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
I1 : (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
I2 : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
⊢ (↑a : ℝ) ≤ x

Tactic:
exact le_trans (mod_cast hi.1) hx.1

Premises used: And.left, le_trans
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
apply :
  @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
⊢ IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume

Tactic:
apply Integrable.mono_measure _ (Measure.restrict_mono_set _ Ico_subset_Icc_self)

Premises used: MeasureTheory.Integrable.mono_measure, Set.Ico_subset_Icc_self, MeasureTheory.Measure.restrict_mono_set
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hφ : @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
hf₁ :
  MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))
⊢ @Integrable ℝ _ _ _ toMeasurableSpace (fun (x : ℝ) ↦ f x * g (x - 1))
    (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
apply Integrable.mul_of_top_left

Premises used: MeasureTheory.Integrable.mul_of_top_left
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
hf.integrableOn_isCompact isCompact_Icc

Premises used: MeasureTheory.IntegrableOn, CompactIccSpace.isCompact_Icc, MonotoneOn.integrableOn_isCompact
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
⊢ @Integrable _ _ _ _ toMeasurableSpace f (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
exact hf.integrableOn_isCompact isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MonotoneOn.integrableOn_isCompact
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hf₁ : AntitoneOn (β := ℝ) (fun (x : ℝ) ↦ g (x - 1)) (Icc (↑a : ℝ) (↑b : ℝ))
⊢ MemLp (ε := ℝ) (m0 := toMeasurableSpace) (fun (x : ℝ) ↦ g (x - 1)) ⊤ (Measure.restrict volume (Icc (↑a : ℝ) (↑b : ℝ)))

Tactic:
apply AntitoneOn.memLp_isCompact isCompact_Icc

Premises used: AntitoneOn.memLp_isCompact, CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
hf₁ : x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hf₂ : y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
hf₃ : x - 1 ≤ y - 1
⊢ LE.le (α := ℝ) ((fun (x : ℝ) ↦ g (x - 1)) y) ((fun (x : ℝ) ↦ g (x - 1)) x)

Tactic:
apply hg
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
⊢ x - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
⊢ y - 1 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simpa using hy
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : AntitoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑a : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑b : ℝ) 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) y
hxy : x ≤ y
⊢ x - 1 ≤ y - 1

Tactic:
simpa using hxy
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
h :
  ∀ i ∈ Ico a b,
    ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x → f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)
hg₁ : IntegrableOn (ε := ℝ) (mα := toMeasurableSpace) (fun (x : ℝ) ↦ f x * g (x - 1)) (Ico (↑a : ℝ) (↑b : ℝ)) volume
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in (↑a : ℝ)..(↑b : ℝ), f x * g (x - 1)) (∑ i ∈ Finset.Ico a b, f (↑i : ℝ) * g (↑i : ℝ))

Tactic:
apply integral_le_sum_Ico_of_le (f := fun x ↦ f x * g x) hab

Premises used: integral_le_sum_Ico_of_le
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
⊢ (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

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

Premises used: Set.mem_Ico, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SumIntegralComparisons
Goal:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc (↑a : ℝ) (↑b : ℝ))
hg : MonotoneOn g (Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1))
fpos : 0 ≤ f (↑b : ℝ)
gpos : 0 ≤ g (HSub.hSub (α := ℝ) (↑a : ℝ) 1)
i : ℕ
hi : i ∈ Ico a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ico (↑i : ℝ) (↑(i + 1) : ℝ)) x
hx₁ : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ a ≤ i ∧ i < b

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

Premises used: Set.mem_Ico, Nat.cast_add, Nat.cast_one