From 26b435fa4d46dab0b2e7004f2b7468792db522d0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sat, 22 Nov 2025 13:23:09 +1100
Subject: [PATCH] feat: `grind_pattern` for `Subtype.property` (#11317)

This PR adds `grind_pattern Subtype.property => self.val`.
---
 src/Init/Prelude.lean | 2 ++
 1 file changed, 2 insertions(+)

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.