feat: mark sizeOf theorems as grind theorems (#11265)

This PR marks the automatically generated `sizeOf` theorems as `grind`
theorems.

closes #11259

Note: Requested update stage0, we need it to be able to solve example in
the issue above.
```lean
example (a: Nat) (b: Nat): sizeOf a < sizeOf (a, b) := by
  grind
```

Author: leodemoura

src/Lean/Meta/SizeOf.lean

@@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.AddDecl
 public import Lean.Meta.AppBuilder
 public import Lean.DefEqAttrib
-
 public section
-
 namespace Lean.Meta
 
 /-- Create `SizeOf` local instances for applicable parameters, and execute `k` using them. -/
@@ -430,6 +427,8 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
   let ctorInfo ← getConstInfoCtor ctorName
   let us := ctorInfo.levelParams.map mkLevelParam
   let simpAttr ← ofExcept <| getAttributeImpl (← getEnv) `simp
+  let grindAttr ← ofExcept <| getAttributeImpl (← getEnv) `grind
+  let grindAttrStx ← `(attr| grind =)
   forallTelescopeReducing ctorInfo.type fun xs _ => do
     let params := xs[*...ctorInfo.numParams]
     let fields := xs[ctorInfo.numParams...*]
@@ -464,7 +463,8 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
         value       := thmValue
       }
       inferDefEqAttr thmName
-      simpAttr.add thmName default AttributeKind.global
+      simpAttr.add thmName default .global
+      grindAttr.add thmName grindAttrStx .global
 
 private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array Name) (recMap : NameMap Name) : MetaM Unit := do
   for indTypeName in indTypeNames do

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/lean/run/grind_11259.lean

@@ -0,0 +1,16 @@
+inductive Lst (α : Type u) where
+  | nil : Lst α
+  | cons (head : α) (tail : Lst α) : Lst α
+
+structure Prd (α : Type u) (β : Type v) where
+  fst : α
+  snd : β
+
+example : sizeOf (@Lst.nil Nat) < sizeOf (Lst.cons 10 .nil) := by
+  grind
+
+example (a b : Nat) : sizeOf a < sizeOf { fst := a, snd := b : Prd _ _ } := by
+  grind
+
+example (a : α) (b : β) : sizeOf a < sizeOf { fst := a, snd := b : Prd _ _ } := by
+  grind