awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
simp : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
⊢ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
simp only [le_sub_iff_add_le]

Premises used: le_sub_iff_add_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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
norm_cast : i + 1 ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)

Tactic:
norm_cast
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ i + 1 ≤ b

Tactic:
lia
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
⊢ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
have I0 : (i : ℝ) ≤ b - 1 := by
      simp only [le_sub_iff_add_le]
      norm_cast
      lia
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
simp : (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ∧ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simp only [mem_Icc, tsub_le_iff_right]

Premises used: tsub_le_iff_right, Set.mem_Icc
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
norm_cast : a ≤ i + 1
⊢ (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
norm_cast
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ a ≤ i + 1

Tactic:
lia
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑a : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ∧ (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1

Tactic:
exact ⟨by norm_cast; lia, I0⟩
-- 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 : ℕ
x : ℝ
hx : (↑i : ℝ) ≤ x ∧ x < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hi : a ≤ i ∧ i < b
I0 : (↑i : ℝ) ≤ HSub.hSub (α := ℝ) (↑b : ℝ) 1
⊢ (↑i : ℝ) ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
have I1 : (i : ℝ) ∈ Icc (a - 1 : ℝ) (b - 1) := by
      simp only [mem_Icc, tsub_le_iff_right]
      exact ⟨by norm_cast; lia, I0⟩
-- 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 : ℕ
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)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

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

Premises used: Set.Mem, setOf, LT.lt.le, Set.Icc, And.right, And.left, And.intro, LE.le.trans, le_trans
-- 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 : ℕ
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)
refine : HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

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 : 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 : ℕ
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)
norm_cast : i + 1 ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ (↑b : ℝ)

Tactic:
norm_cast
-- 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 : ℕ
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)
⊢ i + 1 ≤ b

Tactic:
lia
-- 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 : ℕ
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)
⊢ Membership.mem (γ := Set ℝ) (Icc (↑a : ℝ) (↑b : ℝ)) x

Tactic:
have I2 : x ∈ Icc (a : ℝ) b := by
      refine ⟨le_trans (mod_cast hi.1) hx.1, hx.2.le.trans ?_⟩
      norm_cast
      lia
-- 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 : ℕ
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 x ≤ f (↑i : ℝ)
h₁ : g (x - 1) ≤ g (↑i : ℝ)
h₂ : 0 ≤ g (x - 1)
h₃ : 0 ≤ f (↑i : ℝ)
⊢ f x * g (x - 1) ≤ f (↑i : ℝ) * g (↑i : ℝ)

Tactic:
apply mul_le_mul

Premises used: mul_le_mul
-- 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 : ℕ
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 x ≤ f (↑i : ℝ)

Tactic:
apply hf
-- 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 (x - 1) ≤ g (↑i : ℝ)

Tactic:
apply hg
-- 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 : 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 : ℕ
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 (α := ℝ) (↑a : ℝ) 1) ≤ g (x - 1)
⊢ 0 ≤ g (x - 1)

Tactic:
apply gpos.trans

Premises used: LE.le.trans
-- 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 : ℕ
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 (α := ℝ) (↑a : ℝ) 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 : 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 : ℕ
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 ∈ Icc (HSub.hSub (α := ℝ) (↑a : ℝ) 1) (HSub.hSub (α := ℝ) (↑b : ℝ) 1)

Tactic:
simpa using I2
-- 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 : ℕ
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 (α := ℝ) (↑a : ℝ) 1 ≤ x - 1

Tactic:
simpa using I2.1

Premises used: And.left
-- 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 : ℕ
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 (α := ℝ) (↑a : ℝ) 1) ≤ g (x - 1)

Tactic:
apply hg (by simp [hab]) (by simpa using I2) (by simpa using I2.1)
-- 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 : ℕ
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 (↑b : ℝ) ≤ f (↑i : ℝ)
⊢ 0 ≤ f (↑i : ℝ)

Tactic:
apply fpos.trans

Premises used: LE.le.trans