From f8660485d7baf532a214df9c351ece6091efb269 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 28 Jan 2025 11:21:10 +1100 Subject: [PATCH] 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 | 6 ++++++ 1 file changed, 6 insertions(+) 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