naming, and deprecations

Author: kim-em

src/Init/Data/Array/Monadic.lean

@@ -31,7 +31,11 @@ open Nat
     xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
   induction xs; simp_all
 
-@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : (xs.mapM f).run = xs.map (f · |>.run) :=
+@[simp] theorem idRun_mapM {xs : Array α} {f : α → Id β} : (xs.mapM f).run = xs.map (f · |>.run) :=
+  mapM_pure
+
+@[deprecated idRun_mapM (since := "2025-05-21")]
+theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
   mapM_pure
 
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {xs ys : Array α} :
@@ -181,12 +185,19 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
     {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
     (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
       xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
   forIn'_pure_yield_eq_foldl _ _
 
+@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
+    {xs : Array α} (f : (a : α) → a ∈ xs → β → β) (init : β) :
+    forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Array α} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
     forIn' (xs.map g) init f = forIn' xs init fun a h y => f (g a) (mem_map_of_mem h) y := by
@@ -222,12 +233,19 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
     {xs : Array α} (f : α → β → Id β) (init : β) :
     (forIn xs init (fun a b => .yield <$> f a b)).run =
       xs.foldl (fun b a => f a b |>.run) init :=
   forIn_pure_yield_eq_foldl _ _
 
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
+    {xs : Array α} (f : α → β → β) (init : β) :
+    forIn (m := Id) xs init (fun a b => .yield (f a b)) =
+      xs.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
+
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} :
     forIn (xs.map g) init f = forIn xs init fun a y => f (g a) y := by

src/Init/Data/List/Control.lean

@@ -348,10 +348,16 @@ theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List 
     | false => simp [ih]
 
 @[simp]
-theorem findM?_id (p : α → Id Bool) (as : List α) :
+theorem idRun_findM? (p : α → Id Bool) (as : List α) :
     (findM? p as).run = as.find? (p · |>.run) :=
   findM?_pure _ _
 
+@[deprecated idRun_findM? (since := "2025-05-21")]
+theorem findM?_id (p : α → Id Bool) (as : List α) :
+    findM? (m := Id) p as = as.find? p :=
+  findM?_pure _ _
+
+
 /--
 Returns the first non-`none` result of applying the monadic function `f` to each element of the
 list, in order. Returns `none` if `f` returns `none` for all elements.
@@ -395,10 +401,15 @@ theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : L
     | none   => simp [ih]
 
 @[simp]
-theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
+theorem idRun_findSomeM? (f : α → Id (Option β)) (as : List α) :
     (findSomeM? f as).run = as.findSome? (f · |>.run) :=
   findSomeM?_pure
 
+@[deprecated idRun_findSomeM? (since := "2025-05-21")]
+theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
+    findSomeM? (m := Id) f as = as.findSome? f :=
+  findSomeM?_pure
+
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :
     as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by
   induction as with

src/Init/Data/List/Lemmas.lean

@@ -2548,12 +2548,20 @@ theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
     l.foldr f b = (l.foldrM (m := Id) (pure <| f · ·) b).run := by
   simp
 
-theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+theorem idRun_foldlM {f : β → α → Id β} {b : β} {l : List α} :
     Id.run (l.foldlM f b) = l.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
 
-theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+@[deprecated idRun_foldlM (since := "2025-05-21")]
+theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+    Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm
+
+theorem idRun_foldrM {f : α → β → Id β} {b : β} {l : List α} :
     Id.run (l.foldrM f b) = l.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
 
+@[deprecated idRun_foldrM (since := "2025-05-21")]
+theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+    Id.run (l.foldrM f b) = l.foldr f b := foldr_eq_foldrM.symm
+
 @[simp] theorem foldlM_reverse [Monad m] {l : List α} {f : β → α → m β} {b : β} :
     l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b := rfl
 

src/Init/Data/List/Monadic.lean

@@ -66,7 +66,11 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α}
     l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
   induction l <;> simp_all
 
-@[simp] theorem mapM_id {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
+@[simp] theorem idRun_mapM {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
+  mapM_pure
+
+@[deprecated idRun_mapM (since := "2025-05-21")]
+theorem mapM_id {l : List α} {f : α → Id β} : (l.mapM f).run = l.map (f · |>.run) :=
   mapM_pure
 
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {l₁ l₂ : List α} :
@@ -339,12 +343,19 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   simp only [forIn'_eq_foldlM]
   induction l.attach generalizing init <;> simp_all
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
     (l : List α) (f : (a : α) → a ∈ l → β → Id β) (init : β) :
     (forIn' l init (fun a m b => .yield <$> f a m b)).run =
       l.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
   forIn'_pure_yield_eq_foldl _ _
 
+@[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
+    {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
     forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem h) y := by
@@ -391,12 +402,19 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   simp only [forIn_eq_foldlM]
   induction l generalizing init <;> simp_all
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
     (l : List α) (f : α → β → Id β) (init : β) :
     (forIn l init (fun a b => .yield <$> f a b)).run =
       l.foldl (fun b a => f a b |>.run) init :=
   forIn_pure_yield_eq_foldl _ _
 
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
+    {l : List α} (f : α → β → β) (init : β) :
+    forIn (m := Id) l init (fun a b => .yield (f a b)) =
+      l.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
+
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :
     forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by

src/Init/Data/Option/Monadic.lean

@@ -86,12 +86,19 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
       pure (f := m) (o.pelim b (fun a h => f a h b)) := by
   cases o <;> simp
 
-@[simp] theorem forIn'_id_yield_eq_pelim
+@[simp] theorem idRun_forIn'_yield_eq_pelim
     (o : Option α) (f : (a : α) → a ∈ o → β → Id β) (b : β) :
     (forIn' o b (fun a m b => .yield <$> f a m b)).run =
       o.pelim b (fun a h => f a h b |>.run) :=
   forIn'_pure_yield_eq_pelim _ _ _
 
+@[deprecated idRun_forIn'_yield_eq_pelim (since := "2025-05-21")]
+theorem forIn'_id_yield_eq_pelim
+    (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) :
+    forIn' (m := Id) o b (fun a m b => .yield (f a m b)) =
+      o.pelim b (fun a h => f a h b) :=
+  forIn'_pure_yield_eq_pelim _ _ _
+
 @[simp, grind] theorem forIn'_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) :
     forIn' (o.map g) init f = forIn' o init fun a h y => f (g a) (mem_map_of_mem g h) y := by
@@ -115,12 +122,19 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
       pure (f := m) (o.elim b (fun a => f a b)) := by
   cases o <;> simp
 
-@[simp] theorem forIn_id_yield_eq_elim
+@[simp] theorem idRun_forIn_yield_eq_elim
     (o : Option α) (f : (a : α) → β → Id β) (b : β) :
     (forIn o b (fun a b => .yield <$> f a b)).run =
       o.elim b (fun a => f a b |>.run) :=
   forIn_pure_yield_eq_elim _ _ _
 
+@[deprecated idRun_forIn_yield_eq_elim (since := "2025-05-21")]
+theorem forIn_id_yield_eq_elim
+    (o : Option α) (f : (a : α) → β → β) (b : β) :
+    forIn (m := Id) o b (fun a b => .yield (f a b)) =
+      o.elim b (fun a => f a b) :=
+  forIn_pure_yield_eq_elim _ _ _
+
 @[simp, grind] theorem forIn_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
     forIn (o.map g) init f = forIn o init fun a y => f (g a) y := by

src/Init/Data/Vector/Lemmas.lean

@@ -2390,12 +2390,20 @@ theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Vector α n} :
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Vector α n} :
     xs.foldr f b = (xs.foldrM (m := Id) (pure <| f · ·) b).run := rfl
 
-@[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Vector α n} :
+@[simp] theorem idRun_foldlM {f : β → α → Id β} {b} {xs : Vector α n} :
     Id.run (xs.foldlM f b) = xs.foldl (f · · |>.run) b := foldl_eq_foldlM.symm
 
-@[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
+@[deprecated idRun_foldlM (since := "2025-05-21")]
+theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Vector α n} :
+    Id.run (xs.foldlM f b) = xs.foldl f b := foldl_eq_foldlM.symm
+
+@[simp] theorem idRun_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
     Id.run (xs.foldrM f b) = xs.foldr (f · · |>.run) b := foldr_eq_foldrM.symm
 
+@[deprecated idRun_foldrM (since := "2025-05-21")]
+theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
+    Id.run (xs.foldrM f b) = xs.foldr f b := foldr_eq_foldrM.symm
+
 @[simp] theorem foldlM_reverse [Monad m] {xs : Vector α n} {f : β → α → m β} {b} :
     xs.reverse.foldlM f b = xs.foldrM (fun x y => f y x) b := by
   rcases xs with ⟨xs, rfl⟩

src/Init/Data/Vector/Monadic.lean

@@ -143,12 +143,19 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]
 
-@[simp] theorem forIn'_yield_eq_foldl
+@[simp] theorem idRun_forIn'_yield_eq_foldl
     {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
     (forIn' xs init (fun a m b => .yield <$> f a m b)).run =
       xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init :=
   forIn'_pure_yield_eq_foldl _ _
 
+@[deprecated forIn'_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn'_yield_eq_foldl
+    {xs : Vector α n} (f : (a : α) → a ∈ xs → β → β) (init : β) :
+    forIn' (m := Id) xs init (fun a m b => .yield (f a m b)) =
+      xs.attach.foldl (fun b ⟨a, h⟩ => f a h b) init :=
+  forIn'_pure_yield_eq_foldl _ _
+
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Vector α n} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
     forIn' (xs.map g) init f = forIn' xs init fun a h y => f (g a) (mem_map_of_mem h) y := by
@@ -184,12 +191,19 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]
 
-@[simp] theorem forIn_yield_eq_foldl
+@[simp] theorem idRun_forIn_yield_eq_foldl
     {xs : Vector α n} (f : α → β → Id β) (init : β) :
     (forIn xs init (fun a b => .yield <$> f a b)).run =
       xs.foldl (fun b a => f a b |>.run) init :=
   forIn_pure_yield_eq_foldl _ _
 
+@[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
+theorem forIn_yield_eq_foldl
+    {xs : Vector α n} (f : α → β → β) (init : β) :
+    forIn (m := Id) xs init (fun a b => .yield (f a b)) =
+      xs.foldl (fun b a => f a b) init :=
+  forIn_pure_yield_eq_foldl _ _
+
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)) :
     forIn (xs.map g) init f = forIn xs init fun a y => f (g a) y := by