Commit 2025-08-28 01:28 d60062a6

feat(Tactic/FieldSimp): rewrite for performance and robustness (#28658) This is a rewrite from scratch of the field_simp tactic. The former implementation was a lightweight wrapper around simp (with a custom simp-set and discharger). Broadly speaking, the new implementation reduces expressions to an internal normal form x1 ^ k1 * ... * xn ^ kn, where x1, ... xn are atoms tracked by the AtomM monad and k1, ... kn are integers. This is more robust: the tactic now solves goals which were not in scope for the simp-set version, often to the confusion of users. For example, x ^ 2 / x is now reduced to x, and x / (x * y) is now reduced, given (hx : x ≠ 0), to 1 / y. It's also faster: on a typical large example taken from Mathlib, the heartbeat count reduces from 19983 heartbeats to 2979 heartbeats. There is a big diff: the old field_simp subsumed simp, and this was often exploited. We offer a simproc version of the new field_simp, and switching to a simp call with this simproc fixes about 80% of the cases that break; the rest are handled individually (typically by alternating simp and field_simp calls). Developed at Big Proof at the Isaac Newton Institute.