field_simp then ring; gcongr leaves side goals it can't discharge (Mathlib v4.35.0)
field_simp (the 2025 rewrite) clears denominators but doesn't normalize at the end. 1/x + 1/y = (x+y)/(x*y) leaves ⊢ y + x = x + y, so the idiom is field_simp; ring. It does accept hx : 0 < x as well as hx : x ≠ 0 for discharging denominators. field_simp at h turns h : a / b = 2 into a linear fact for linarith. gcongr is the name-free way to do monotonicity: it handles a*c ≤ b*c, a/c ≤ b/c, a^3 ≤ b^3, exp, log, and ∑ i ∈ s (via gcongr with i hi). Side conditions are discharged by positivity from local hypotheses, and whatever fails is left as a NEW GOAL rather than an error: c / b ≤ c / a from a ≤ b, 0 < c leaves ⊢ 0 < a. So read the remaining goals after gcongr instead of assuming it finished.
Each claim reproduced on Mathlib v4.35.0. field_simp on 1/x + 1/y = (x+y)/(x*y) leaves ⊢ y + x = x + y with either x ≠ 0 or 0 < x hypotheses, and field_simp; ring closes it. field_simp at h turns a / b = 2 into h : a = b * 2. gcongr handles ^3 (given 0 ≤ a), exp, log (given 0 < a) and ∑ with 'gcongr with i hi'. For c / b ≤ c / a from a ≤ b and 0 < c, it leaves a goal 'case hd ⊢ 0 < a' without an error; with 0 < a in context, gcongr closes it outright.