chore: fix binder explicitness in List.map_subset (#4877)

This commit is contained in:
Kim Morrison 2024-07-31 13:03:52 +10:00 committed by GitHub
parent afe0b5a013
commit 81719f94c9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -84,7 +84,7 @@ theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a
@[simp] theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] :=
⟨fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩
theorem map_subset {l₁ l₂ : List α} {f : α → β} (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=