From 8d40cf5157b1d873c363afee0d17bf08ca6adfc2 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 27 Jun 2025 17:28:59 +1000
Subject: [PATCH] chore: missing Option lemma (#9028)

---
 src/Init/Data/Option/Lemmas.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index c4114b9823..19f1dbdfac 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -645,6 +645,10 @@ theorem get_none_eq_iff_true {h} : (none : Option α).get h = a ↔ True := by
   simp only [guard]
   split <;> simp
 
+@[grind =] theorem getD_guard : (guard p a).getD b = if p a then a else b := by
+  simp only [guard]
+  split <;> simp
+
 @[grind]
 theorem guard_def (p : α → Bool) :
     Option.guard p = fun x => if p x then some x else none := rfl