From d0b947bf52c09c430f643c69a8a2e91e8ef39e7f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 28 Jan 2025 12:59:47 +1100 Subject: [PATCH] chore: add @[simp] to Option.not_mem_none (#6804) This PR improves simp lemma confluence. --- src/Init/Data/Option/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index 87f318b131..624cc14734 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -34,7 +34,7 @@ theorem get_mem : ∀ {o : Option α} (h : isSome o), o.get h ∈ o theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a | _, _, rfl => rfl -theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun +@[simp] theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x := by cases x; {contradiction}; rw [getD_some]