feat: allow grind to unfold abs (#31935)

Following discussion on [zulip](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.22Missing.20Tactics.22.20list/near/558745339)[#general > "Missing Tactics" list @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.22Missing.20Tactics.22.20list/near/558745339).

Author: kim-em

Mathlib/Algebra/Order/Group/Unbundled/Abs.lean

@@ -34,7 +34,7 @@ section Group
 variable [Group α] {a b : α}
 
 /-- `mabs a`, denoted `|a|ₘ`, is the absolute value of `a`. -/
-@[to_additive /-- `abs a`, denoted `|a|`, is the absolute value of `a` -/]
+@[to_additive (attr := grind) /-- `abs a`, denoted `|a|`, is the absolute value of `a` -/]
 def mabs (a : α) : α := a ⊔ a⁻¹
 
 @[inherit_doc mabs]

MathlibTest/grind/linarith.lean

@@ -0,0 +1,8 @@
+import Mathlib
+
+example {α : Type*} [LinearOrder α] [CommRing α] [IsStrictOrderedRing α]
+    (a b c d : α) : |a - b| ≤ |a - c| + |c - d| + |b - d| := by
+  grind
+
+example (L : ℝ) : 0 < 1 + |L| := by
+  grind