fix: missing condition at normalizePattern in grind (#11629)

This PR adds a missing condition in the pattern normalization code used
in `grind`. It should ignore support ground terms.

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -716,7 +716,7 @@ where
         pure dontCare
       else
         let arg ← expandOffsetPatterns arg
-        unless isEqBwdParent do
+        unless isEqBwdParent || inSupport do
           /-
           **Note**: We ignore symbols in ground patterns if the parent is the auxiliary ``Grind.eqBwdPattern
           We do that because we want to sign an error in examples such as:

tests/lean/run/grind_ground_pat_issue.lean

@@ -0,0 +1,43 @@
+/-!
+ Test for a regression introduced by #11589
+-/
+
+section Mathlib.Order.Defs.LinearOrder
+
+class LinearOrder (α : Type) extends Max α where
+
+end Mathlib.Order.Defs.LinearOrder
+section Mathlib.Data.Int.Order.Basic
+
+instance instLinearOrder : LinearOrder Int where
+
+end Mathlib.Data.Int.Order.Basic
+section Mathlib.Order.Lattice
+
+variable {α : Type}
+
+class SemilatticeSup (α : Type) where
+  sup : α → α → α
+
+instance SemilatticeSup.toMax [SemilatticeSup α] : Max α where max a b := SemilatticeSup.sup a b
+
+instance LinearOrder.toSemilatticeSup {α : Type} [LinearOrder α] : SemilatticeSup α where
+  sup := max
+
+end Mathlib.Order.Lattice
+
+section Mathlib.Algebra.Order.Group.Unbundled.Abs
+
+variable {α : Type} [SemilatticeSup α] [Neg α] {a b : α}
+
+@[grind]
+def abs (a : α) : α := max a (-a)
+
+end Mathlib.Algebra.Order.Group.Unbundled.Abs
+
+@[grind =] theorem max_def [Max α] [LE α] [DecidableLE α] (a b : α)
+    : max a b = if a ≤ b then b else a :=
+  sorry
+
+theorem abs_lt_one_iff {a : Int} : abs a < 1 ↔ a = 0 := by
+  grind