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

Tactic:
simpa using 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
⊢ f (↑b : ℝ) ≤ f (↑i : ℝ)

Tactic:
apply hf ⟨mod_cast hi.1, mod_cast hi.2.le⟩ (by simpa using hab) (mod_cast hi.2.le)

Premises used: And.intro