Commit 2025-09-23 15:40 8f2d1c4d
View on Github →feat(Tactic/FieldSimp): handle inequalities (#29364)
This PR extends the field_simp tactic to cancel positive denominators in inequalities, by analogy with the existing behaviour of cancelling nonzero denominators in equalities. For example, field_simp now reduces the following goal (from Mathlib.Analysis.Convex.Mul):
x y a b : ℚ
hx : 0 < x
hy : 0 < y
ha : 0 < a
hb : 0 < b
⊢ (a * x + b * y)⁻¹ ≤ a * x⁻¹ + b * y⁻¹
to ⊢ x * y ≤ (a * x + b * y) * (a * y + x * b).