feat: List.map_id' with lambda (#450)

leanprover-community · Dec 15, 2023 · fa17cba · fa17cba
1 parent 75e75a5
commit fa17cba
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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