Commit 2025-02-14 12:41 93ad6eca

perf(Tactic/FieldSimp): exclude simp lemmas that don't apply for fields. (#21326) This PR excludes simp lemmas like div_self' from being used in the field_simp tactic. These lemmas have discrimination tree keys that commonly find a match when running field_simp, and if they do match then unification needs to fail, because the field is in fact not a Group/CommGroup/LeftCancelMonoid/RightCancelMonoid.