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`.

Author: JovanGerb

Mathlib/Tactic/FieldSimp.lean

@@ -86,6 +86,26 @@ partial def discharge (prop : Expr) : SimpM (Option Expr) :=
 @[inherit_doc discharge]
 elab "field_simp_discharge" : tactic => wrapSimpDischarger Mathlib.Tactic.FieldSimp.discharge
 
+/-- The list of lemma's that aren't used in `field_simp`.
+
+`one_div`, `mul_eq_zero` and `one_divp` are excluded because we don't want those rewrites.
+
+The remaining constants are excluded for efficiency. These are lemmas consisting of just
+`*`, `/` and `=` that are applicable in a typeclass that can't be a field. -/
+def fieldSimpExcluded : List Name := [
+  ``one_div, ``mul_eq_zero, ``one_divp,
+
+  ``div_self', ``div_div_cancel, ``div_div_cancel_left,
+  ``div_mul_cancel, ``div_mul_cancel_left, ``div_mul_cancel_right,
+  ``mul_div_cancel, ``mul_div_cancel_left, ``mul_div_cancel_right,
+  ``div_div_div_cancel_left, ``div_div_div_cancel_right,
+  ``div_mul_div_cancel, ``div_mul_div_cancel', ``div_mul_mul_cancel,
+  ``mul_div_div_cancel, ``mul_mul_div_cancel,
+
+  ``div_eq_self,
+  ``mul_left_eq_self, ``mul_right_eq_self, ``self_eq_mul_left, ``self_eq_mul_right,
+  ``div_left_inj, ``div_right_inj, ``mul_left_inj, ``mul_right_inj]
+
 /--
 The goal of `field_simp` is to reduce an expression in a field to an expression of the form `n / d`
 where neither `n` nor `d` contains any division symbol, just using the simplifier (with a carefully
@@ -169,9 +189,7 @@ elab_rules : tactic
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else do
     let thms0 ← getSimpTheorems
-    let thms0 ← thms0.erase (.decl ``one_div)
-    let thms0 ← thms0.erase (.decl `mul_eq_zero)
-    thms0.erase (.decl ``one_divp)
+    fieldSimpExcluded.foldlM (init := thms0) fun thms0 name => thms0.erase (.decl name)
 
   let some ext ← getSimpExtension? `field_simps | throwError "field_simps not found"
   let thms ← ext.getTheorems