diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index f07dde2df0..759f505d80 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/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
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..ad491b0de1 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {
diff --git a/tests/lean/run/grind_11259.lean b/tests/lean/run/grind_11259.lean
new file mode 100644
index 0000000000..699a5f8bc6
--- /dev/null
+++ b/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