feat: add getD_comp_some lemma for Option type (#31828)

Adds a simp lemma that allows this expression to be simplified, even if it isn't applied to an argument.

Identified in google-deepmind/formal-conjectures#1120

Author: BoltonBailey

Mathlib/Data/Option/Basic.lean

@@ -233,4 +233,9 @@ lemma elim'_update {α : Type*} {β : Type*} [DecidableEq α]
     | _, _, some _, h => (h _ rfl).elim
     | _, _, none, _ => rfl) _ _ _
 
+@[simp]
+lemma getD_comp_some (d : α) : (fun x ↦ x.getD d) ∘ some = id := by
+  ext
+  simp only [Function.comp_apply, getD_some, id_eq]
+
 end Option