diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index bfb5adc8a8..a09c3986b5 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -631,6 +631,8 @@ structure Subtype {α : Sort u} (p : α → Prop) where
   -/
   property : p val
 
+grind_pattern Subtype.property => self.val
+
 set_option linter.unusedVariables.funArgs false in
 /--
 Gadget for optional parameter support.