Commit 2024-03-02 00:03 37bc4aba
View on Github →refactor: optimize proofs with omega (#11093)
I ran tryAtEachStep on all files under Mathlib
to find all locations where omega
succeeds. For each that was a linarith
without an only
, I tried replacing it with omega
, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slow aesop
s along the way.