diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean
index 26b340f20c..c43fbc4907 100644
--- a/src/Init/Data/Array/OfFn.lean
+++ b/src/Init/Data/Array/OfFn.lean
@@ -82,7 +82,7 @@ theorem ofFnM_succ' {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       let a ← f 0
       let as ← ofFnM fun i => f i.succ
       pure (#[a] ++ as)) := by
-  simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
+  simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.foldlM_push_eq_append, List.finRange_succ, Function.comp_def]
 
 theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
     ofFnM f = (do
diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean
index 747132481c..30a23b472c 100644
--- a/src/Init/Data/List/FinRange.lean
+++ b/src/Init/Data/List/FinRange.lean
@@ -61,7 +61,7 @@ end List
 
 namespace Fin
 
-theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α) :
+theorem foldlM_eq_foldlM_finRange [Monad m] (f : α → Fin n → m α) (x : α) :
     foldlM n f x = (List.finRange n).foldlM f x := by
   induction n generalizing x with
   | zero => simp
@@ -71,7 +71,7 @@ theorem foldlM_eq_finRange_foldlM [Monad m] (f : α → Fin n → m α) (x : α)
     funext y
     simp [ih, List.foldlM_map]
 
-theorem foldrM_eq_finRange_foldrM [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
+theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) :
     foldrM n f x = (List.finRange n).foldrM f x := by
   induction n generalizing x with
   | zero => simp
@@ -101,7 +101,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       let a ← f 0
       let as ← ofFnM fun i => f i.succ
       pure (a :: as)) := by
-  simp [ofFnM, Fin.foldlM_eq_finRange_foldlM, List.finRange_succ, List.foldlM_cons_eq_append,
+  simp [ofFnM, Fin.foldlM_eq_foldlM_finRange, List.finRange_succ, List.foldlM_cons_eq_append,
     List.foldlM_map]
 
 end List