From fa17cba0459830906e99f0a81fb0edc106220380 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 15 Dec 2023 17:55:34 +1100 Subject: [PATCH] feat: List.map_id' with lambda (#450) --- Std/Data/List/Init/Lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Std/Data/List/Init/Lemmas.lean b/Std/Data/List/Init/Lemmas.lean index 2e58f3d443..5ccffccb51 100644 --- a/Std/Data/List/Init/Lemmas.lean +++ b/Std/Data/List/Init/Lemmas.lean @@ -103,6 +103,8 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s @[simp] theorem map_id (l : List α) : map id l = l := by induction l <;> simp_all +@[simp] theorem map_id' (l : List α) : map (fun a => a) l = l := by induction l <;> simp_all + @[simp] theorem map_map (g : β → γ) (f : α → β) (l : List α) : map g (map f l) = map (g ∘ f) l := by induction l <;> simp_all