max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove @[simp] from mem_of_find?_eq_some (#5105)

Browse source
This commit is contained in:
Kim Morrison 2024-08-21 13:16:22 +10:00 • committed by GitHub
parent 0203cb091d
commit 4dbd20343f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/List/Find.lean
View file

@ -34,7 +34,7 @@ theorem find?_some : ∀ {l}, find? p l = some a → p a
· exact H ▸ h
· exact find?_some H
@[simp] theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
| b :: l, H => by
by_cases h : p b <;> simp [find?, h] at H
· exact H ▸ .head _