From 81719f94c9e7190e36206e999b895e1c8564caf4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 31 Jul 2024 13:03:52 +1000 Subject: [PATCH] chore: fix binder explicitness in List.map_subset (#4877) --- src/Init/Data/List/Sublist.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 27f0c2f4ce..63a0974599 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -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₂ :=