diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 786bb371c7..d7f07a3db6 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -374,9 +374,15 @@ end choice
 
 -- See `Init.Data.Option.List` for lemmas about `toList`.
 
-@[simp] theorem or_some : (some a).or o = some a := rfl
+@[simp] theorem some_or : (some a).or o = some a := rfl
 @[simp] theorem none_or : none.or o = o := rfl
 
+@[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
+
+/-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
+@[simp] theorem or_some' {o : Option α} : o.or (some a) = o.getD a := by
+  cases o <;> rfl
+
 theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
   cases o <;> rfl