diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 0b684d2894..87f318b131 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -655,4 +655,10 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H)
 @[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp
 
+@[simp] theorem elim_pmap {p : α → Prop} (f : (a : α) → p a → β) (o : Option α)
+    (H : ∀ (a : α), a ∈ o → p a) (g : γ) (g' : β → γ) :
+    (o.pmap f H).elim g g' =
+       o.pelim g (fun a h => g' (f a (H a h))) := by
+  cases o <;> simp
+
 end Option