diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index da68b803f3d3d..6f2e89b061e94 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -202,7 +202,7 @@ alias ⟨eq_nil_of_subset_nil, _⟩ := subset_nil theorem map_subset_iff {l₁ l₂ : List α} (f : α → β) (h : Injective f) : map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂ := by - refine ⟨?_, map_subset f⟩; intro h2 x hx + refine ⟨?_, Subset.map f⟩; intro h2 x hx rcases mem_map.1 (h2 (mem_map_of_mem f hx)) with ⟨x', hx', hxx'⟩ cases h hxx'; exact hx'