Fix all the theorem statements too

Author: eric-wieser

src/Init/Control/Lawful/Basic.lean

@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
+import Init.Ext
 import Init.SimpLemmas
 import Init.Meta
 
@@ -241,13 +242,23 @@ theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
 
 namespace Id
 
-@[simp] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
-@[simp] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
-@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+@[ext] theorem ext {x y : Id α} (h : x.run = y.run) : x = y := h
 
 instance : LawfulMonad Id := by
   refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
+@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
+@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
+@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
+@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
+@[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
+
+-- These lemmas are bad as they abuse the defeq of `Id α` and `α`
+@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
+@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
+@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+
 end Id
 
 /-! # Option -/

src/Init/Data/Array/Lemmas.lean

@@ -612,13 +612,13 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st
 
 -- Auxiliary for `any_iff_exists`.
 theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
-    anyM.loop (m := Id) p as stop h start = true ↔
+    (anyM.loop (m := Id) (pure <| p ·) as stop h start).run = true ↔
       ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by
   unfold anyM.loop
   split <;> rename_i h₁
   · dsimp
     split <;> rename_i h₂
-    · simp only [true_iff]
+    · simp only [true_iff, Id.run_pure]
       refine ⟨start, by omega, by omega, by omega, h₂⟩
     · rw [anyM_loop_iff_exists]
       constructor
@@ -635,9 +635,9 @@ termination_by stop - start
 -- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
     as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] := by
-  dsimp [any, anyM, Id.run]
+  dsimp [any, anyM]
   split
-  · rw [anyM_loop_iff_exists]
+  · rw [anyM_loop_iff_exists (p := p)]
   · rw [anyM_loop_iff_exists]
     constructor
     · rintro ⟨i, hi, ge, _, h⟩
@@ -1369,17 +1369,17 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
 
 @[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
 theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
-    mapM.map (m := Id) f as i b = as.foldl (start := i) (fun acc a => acc.push (f a)) b := by
+    mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by
   unfold mapM.map
   split <;> rename_i h
-  · simp only [Id.bind_eq]
-    dsimp [foldl, Id.run, foldlM]
+  · ext : 1
+    dsimp [foldl, foldlM]
     rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
     -- Calling `split` here gives a bad goal.
     have : size as - i = Nat.succ (size as - i - 1) := by omega
     rw [this]
-    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
-  · dsimp [foldl, Id.run, foldlM]
+    simp [foldl, foldlM, Nat.sub_add_eq]
+  · dsimp [foldl, foldlM]
     rw [dif_pos (by omega), foldlM.loop, dif_neg h]
     rfl
 termination_by as.size - i
@@ -1601,8 +1601,8 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
     as.toList ++ List.filterMap f xs := ?_
   exact this #[]
   induction xs
-  · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
+  · simp_all
+  · simp_all [List.filterMap_cons]
     split <;> simp_all
 
 @[grind] theorem toList_filterMap {f : α → Option β} {xs : Array α} :
@@ -3214,18 +3214,16 @@ theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Array α} {a : α} {f : β 
   rw [foldr, foldrM_start_stop, ← foldrM_toList, List.foldrM_pure, foldr_toList, foldr, ← foldrM_start_stop]
 
 theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop : Nat} :
-    xs.foldl f b start stop = xs.foldlM (m := Id) f b start stop := by
-  simp [foldl, Id.run]
+    xs.foldl f b start stop = (xs.foldlM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
-    xs.foldr f b start stop = xs.foldrM (m := Id) f b start stop := by
-  simp [foldr, Id.run]
+    xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
 @[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Array α} {start stop : Nat} :
-    Id.run (xs.foldlM f b start stop) = xs.foldl f b start stop := foldl_eq_foldlM.symm
+    Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl
 
 @[simp] theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Array α} {start stop : Nat} :
-    Id.run (xs.foldrM f b start stop) = xs.foldr f b start stop := foldr_eq_foldrM.symm
+    Id.run (xs.foldrM f b start stop) = xs.foldr (f · · |>.run) b start stop := rfl
 
 /-- Variant of `foldlM_reverse` with a side condition for the `stop` argument. -/
 @[simp] theorem foldlM_reverse' [Monad m] {xs : Array α} {f : β → α → m β} {b} {stop : Nat}
@@ -3483,17 +3481,16 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
 
 @[simp] theorem foldr_append' {f : α → β → β} {b} {xs ys : Array α} {start : Nat}
     (w : start = xs.size + ys.size) :
-    (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := by
-  subst w
-  simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) :=
+  foldrM_append' _ _ _ _ w
 
 @[grind _=_]theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
-    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by
-  simp [foldl_eq_foldlM]
+    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) :=
+  foldlM_append _ _ _ _
 
 @[grind _=_] theorem foldr_append {f : α → β → β} {b} {xs ys : Array α} :
-    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by
-  simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) :=
+  foldrM_append _ _ _ _
 
 @[simp] theorem foldl_flatten' {f : β → α → β} {b} {xss : Array (Array α)} {stop : Nat}
     (w : stop = xss.flatten.size) :
@@ -3522,21 +3519,22 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
 /-- Variant of `foldl_reverse` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_reverse' {xs : Array α} {f : β → α → β} {b} {stop : Nat}
     (w : stop = xs.size) :
-    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b := by
-  simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b 0 stop = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse' _ _ _ w
 
 /-- Variant of `foldr_reverse` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_reverse' {xs : Array α} {f : α → β → β} {b} {start : Nat}
     (w : start = xs.size) :
-    xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b := by
-  simp [w, foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldr f b start 0 = xs.foldl (fun x y => f y x) b :=
+  foldrM_reverse' _ _ _ w
 
 @[grind] theorem foldl_reverse {xs : Array α} {f : β → α → β} {b} :
-    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b :=
+  foldlM_reverse _ _ _
 
 @[grind] theorem foldr_reverse {xs : Array α} {f : α → β → β} {b} :
     xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
-  (foldl_reverse ..).symm.trans <| by simp
+  foldrM_reverse _ _ _
 
 theorem foldl_eq_foldr_reverse {xs : Array α} {f : β → α → β} {b} :
     xs.foldl f b = xs.reverse.foldr (fun x y => f y x) b := by simp
@@ -4600,12 +4598,12 @@ namespace Array
 @[simp] theorem findSomeRev?_eq_findSome?_reverse {f : α → Option β} {xs : Array α} :
     xs.findSomeRev? f = xs.reverse.findSome? f := by
   cases xs
-  simp [findSomeRev?, Id.run]
+  simp [findSomeRev?]
 
 @[simp] theorem findRev?_eq_find?_reverse {f : α → Bool} {xs : Array α} :
     xs.findRev? f = xs.reverse.find? f := by
   cases xs
-  simp [findRev?, Id.run]
+  simp [findRev?]
 
 /-! ### unzip -/
 

src/Init/Data/Array/Lex/Lemmas.lean

@@ -29,16 +29,16 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  simp [lex, Id.run]
+  simp [lex]
 
 @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
   simp only [lex, List.getElem_toArray, List.getElem_singleton]
-  cases lt a b <;> cases a != b <;> simp [Id.run]
+  cases lt a b <;> cases a != b <;> simp
 
 private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
-  simp only [lex, Id.run]
+  simp only [lex]
   simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton,
     Nat.add_comm 1]
   simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left,
@@ -51,10 +51,10 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
 @[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
-  | nil => cases l₂ <;> simp [lex, Id.run]
+  | nil => cases l₂ <;> simp [lex]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Id.run]
+    | nil => simp [lex]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

src/Init/Data/Array/MapIdx.lean

@@ -27,7 +27,7 @@ theorem mapFinIdx_induction (xs : Array α) (f : (i : Nat) → α → (h : i < x
     motive xs.size ∧ ∃ eq : (Array.mapFinIdx xs f).size = xs.size,
       ∀ i h, p i ((Array.mapFinIdx xs f)[i]) h := by
   let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p i bs[i] h) (hm : motive j) :
-    let as : Array β := Array.mapFinIdxM.map (m := Id) xs f i j h bs
+    let as : Array β := Id.run <| Array.mapFinIdxM.map xs (pure <| f · · ·) i j h bs
     motive xs.size ∧ ∃ eq : as.size = xs.size, ∀ i h, p i as[i] h := by
     induction i generalizing j bs with simp [mapFinIdxM.map]
     | zero =>

src/Init/Data/Array/Monadic.lean

@@ -31,7 +31,7 @@ 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 = xs.map f :=
+@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : (xs.mapM f).run = xs.map (f · |>.run) :=
   mapM_pure
 
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {xs ys : Array α} :
@@ -182,11 +182,10 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
 
 @[simp] 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 := by
-  rcases xs with ⟨xs⟩
-  simp [List.foldl_map]
+    {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 _ _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {xs : Array α} (g : α → β) (f : (b : β) → b ∈ xs.map g → γ → m (ForInStep γ)) :
@@ -224,11 +223,10 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
 
 @[simp] 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 := by
-  rcases xs with ⟨xs⟩
-  simp [List.foldl_map]
+    {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 _ _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} :

src/Init/Data/Fin/Fold.lean

@@ -190,7 +190,7 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
   | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
-    foldl n f x = foldlM (m:=Id) n f x := by
+    foldl n f x = (foldlM (m := Id) n (pure <| f · ·) x).run := by
   induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
 
 /-! ### foldr -/
@@ -223,7 +223,7 @@ theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
   | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
-    foldr n f x = foldrM (m:=Id) n f x := by
+    foldr n f x = (foldrM (m := Id) n (pure <| f · ·) x).run := by
   induction n <;> simp [foldr_succ, foldrM_succ, *]
 
 theorem foldl_rev (f : Fin n → α → α) (x) :

src/Init/Data/List/Control.lean

@@ -348,7 +348,8 @@ theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List 
     | false => simp [ih]
 
 @[simp]
-theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
+theorem findM?_id (p : α → Id Bool) (as : List α) :
+    (findM? p as).run = as.find? (p · |>.run) :=
   findM?_pure _ _
 
 /--
@@ -394,7 +395,8 @@ theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : L
     | none   => simp [ih]
 
 @[simp]
-theorem findSomeM?_id {f : α → Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f :=
+theorem findSomeM?_id (f : α → Id (Option β)) (as : List α) :
+    (findSomeM? f as).run = as.findSome? (f · |>.run) :=
   findSomeM?_pure
 
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :

src/Init/Data/List/Lemmas.lean

@@ -2541,18 +2541,18 @@ theorem flatten_reverse {L : List (List α)} :
   induction l generalizing b <;> simp [*]
 
 theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} :
-    l.foldl f b = l.foldlM (m := Id) f b := by
-  induction l generalizing b <;> simp [*, foldl]
+    l.foldl f b = (l.foldlM (m := Id) (pure <| f · ·) b).run := by
+  simp
 
 theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
-    l.foldr f b = l.foldrM (m := Id) f b := by
-  induction l <;> simp [*, foldr]
+    l.foldr f b = (l.foldrM (m := Id) (pure <| f · ·) b).run := by
+  simp
 
-@[simp] theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
-    Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm
+theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
+    Id.run (l.foldlM f b) = l.foldl (f · · |>.run) b := (foldl_eq_foldlM f b l).symm
 
-@[simp] theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
-    Id.run (l.foldrM f b) = l.foldr f b := foldr_eq_foldrM.symm
+theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
+    Id.run (l.foldrM f b) = l.foldr (f · · |>.run) b := (foldr_eq_foldrM f b l).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
@@ -2641,10 +2641,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction l <;> simp [*]
 
 @[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} :
-    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
+    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM, -foldlM_pure]
 
 @[simp, grind _=_] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
-    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
+    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, -foldrM_pure]
 
 @[grind] theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
     (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
@@ -2655,7 +2655,8 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction L <;> simp_all
 
 @[simp, grind] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
-    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
+    l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by
+  simp [foldl_eq_foldlM, foldr_eq_foldrM, -foldrM_pure]
 
 @[simp, grind] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=

src/Init/Data/List/Monadic.lean

@@ -66,7 +66,7 @@ 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 = l.map f :=
+@[simp] 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 α} :
@@ -340,11 +340,10 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
   induction l.attach generalizing init <;> simp_all
 
 @[simp] 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 := by
-  simp only [forIn'_eq_foldlM]
-  induction l.attach generalizing init <;> simp_all
+    (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 _ _ _
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
@@ -393,11 +392,10 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
   induction l generalizing init <;> simp_all
 
 @[simp] 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 := by
-  simp only [forIn_eq_foldlM]
-  induction l generalizing init <;> simp_all
+    (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 _ _ _
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :