fix: lia should not generate instances from hypotheses (#14159)

This PR fixes an oversight in the introduction of `@[lia]` that allowed
`lia` to create instances
based on quantified hypotheses. This in turn can cause explosive
performance regressions if bad
hypotheses are in scope.

Author: hargoniX

src/Init/Grind/Config.lean

@@ -286,6 +286,9 @@ structure CutsatConfig extends NoopConfig where
   -- Re-enable E-matching, so the `@[lia]` lemma set is instantiated.
   -- The active theorem set is restricted to lemmas tagged `@[lia]`, not the full `@[grind]` set.
   ematch := ({} : Config).ematch
+  -- despite having e-matching for @[lia] we do not want (potentially runaway) local theorem
+  -- instantiation
+  genLocal := 0
 
 /--
 A `grind` configuration that only uses `linarith`.