feat: Option.elim_pmap, improving simp confluence (#6802)

This PR adds the simp lemma `Option.elim_pmap`. This is one of many
small PRs that will improve simp lemma confluence.

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