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

chore: fix statement of List.filter_congr (#4524)

Browse source
This commit is contained in:
Kim Morrison 2024-06-21 12:35:43 +01:00 • committed by GitHub
parent d2ae678fbf
commit ee9996ec89
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Data/List/Lemmas.lean
View file

@ -923,12 +923,12 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
| a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
theorem filter_congr {p q : α → Bool} :
∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
| [], _ => rfl
| a :: l, h => by
rw [forall_mem_cons] at h; by_cases pa : p a
· simp [pa, h.1.1 pa, filter_congr h.2]
· simp [pa, mt h.1.2 pa, filter_congr h.2]
· simp [pa, h.1 ▸ pa, filter_congr h.2]
· simp [pa, h.1 ▸ pa, filter_congr h.2]
@[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr