diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean
index 052c003bb7..0fe2149a68 100644
--- a/src/Init/Data/Array/BasicAux.lean
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -36,3 +36,15 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
   apply propext; apply Iff.intro
   · intro h; simp [toArray] at h; have := of_toArrayAux_eq_toArrayAux h rfl; exact this.1
   · intro h; rw [h]
+
+def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=
+  go 0 ⟨mkEmpty as.size, rfl⟩ (by simp_arith)
+where
+  go (i : Nat) (acc : { bs : Array β // bs.size = i }) (hle : i ≤ as.size) : m { bs : Array β // bs.size = as.size } := do
+    if h : i = as.size then
+      return h ▸ acc
+    else
+      have hlt : i < as.size := Nat.lt_of_le_of_ne hle h
+      let b ← f as[i]
+      go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
+termination_by go i _ _ => as.size - i