We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9365fd4 commit 67e91aeCopy full SHA for 67e91ae
src/Init/Data/List/Find.lean
@@ -1106,7 +1106,7 @@ theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
1106
split <;> simp_all [BEq.comm]
1107
1108
@[simp]
1109
-theorem isNone_finIdxOf?' [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
+theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
1110
(l.finIdxOf? a).isNone = !l.contains a := by
1111
rw [← isSome_finIdxOf?, Option.not_isSome]
1112
0 commit comments