-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
    arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[]

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : i < arr.size
⊢ (do
      let __do_lift ← f arr[i]
      List.foldlM
          (fun bs a => do
            let a ← f a
            pure (bs.push a))
          (r.push __do_lift) (List.drop (i + 1) arr.toList)) =
    do
    let x ← f arr.toList[i]
    List.foldlM
        (fun bs a => do
          let a ← f a
          pure (bs.push a))
        (r.push x) (List.drop (i + 1) arr.toList)

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : i < arr.size
⊢ (do
      let __do_lift ← f arr[i]
      mapM.map f arr (i + 1) (r.push __do_lift)) =
    List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

Tactic:
rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : i < arr.size
⊢ (do
      let __do_lift ← f arr[i]
      mapM.map f arr (i + 1) (r.push __do_lift)) =
    List.foldlM (fun bs a => bs.push <$> f a) r (arr.toList[i] :: List.drop (i + 1) arr.toList)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldlM (fun bs a => bs.push <$> f a) (mkEmpty arr.size) (List.drop 0 arr.toList) =
    List.foldlM (fun bs a => bs.push <$> f a) #[] arr.toList

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : i < arr.size
⊢ (do
      let __do_lift ← f arr[i]
      mapM.map f arr (i + 1) (r.push __do_lift)) =
    List.foldlM (fun bs a => bs.push <$> f a) r (arr.toList[i] :: List.drop (i + 1) arr.toList)

Tactic:
simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
  pure_bind]

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : i < arr.size
⊢ (do
      let __do_lift ← f arr[i]
      List.foldlM
          (fun bs a => do
            let a ← f a
            pure (bs.push a))
          (r.push __do_lift) (List.drop (i + 1) arr.toList)) =
    do
    let x ← f arr.toList[i]
    List.foldlM
        (fun bs a => do
          let a ← f a
          pure (bs.push a))
        (r.push x) (List.drop (i + 1) arr.toList)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
x✝ : (_ : Nat) ×' Array β
a✝¹ :
  ∀ (y : (_ : Nat) ×' Array β),
    (invImage (fun x => PSigma.casesOn x fun i r => arr.size - i) instWellFoundedRelationOfSizeOf).1 y x✝ →
      mapM.map f arr y.1 y.2 = List.foldlM (fun bs a => bs.push <$> f a) y.2 (List.drop y.1 arr.toList)
i : Nat
r✝ : Array β
a✝ :
  ∀ (y : (_ : Nat) ×' Array β),
    (invImage (fun x => PSigma.casesOn x fun i r => arr.size - i) instWellFoundedRelationOfSizeOf).1 y ⟨i, r✝⟩ →
      mapM.map f arr y.1 y.2 = List.foldlM (fun bs a => bs.push <$> f a) y.2 (List.drop y.1 arr.toList)
h✝ : i < arr.size
r : Array β
⊢ arr.size - (i + 1) < arr.size - i

Tactic:
decreasing_trivial_pre_omega

Result:
no goals

Proof state:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : ¬i < arr.size
⊢ pure r = List.foldlM (fun bs a => bs.push <$> f a) r []

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
⊢ mapM.map f arr i r = List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

Tactic:
unfold mapM.map

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
⊢ (if hlt : i < arr.size then do
      let __do_lift ← f arr[i]
      mapM.map f arr (i + 1) (r.push __do_lift)
    else pure r) =
    List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
⊢ (if hlt : i < arr.size then do
      let __do_lift ← f arr[i]
      mapM.map f arr (i + 1) (r.push __do_lift)
    else pure r) =
    List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

Tactic:
split

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : i < arr.size
⊢ (do
      let __do_lift ← f arr[i]
      mapM.map f arr (i + 1) (r.push __do_lift)) =
    List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : ¬i < arr.size
⊢ pure r = List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

Proof state:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : ¬i < arr.size
⊢ pure r = List.foldlM (fun bs a => bs.push <$> f a) r (List.drop i arr.toList)

Tactic:
rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]

Result:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
i : Nat
r : Array β
h✝ : ¬i < arr.size
⊢ pure r = List.foldlM (fun bs a => bs.push <$> f a) r []

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ mapM f arr = foldlM (fun bs a => bs.push <$> f a) #[] arr

Tactic:
rw [mapM, aux, ← foldlM_toList]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldlM (fun bs a => bs.push <$> f a) (mkEmpty arr.size) (List.drop 0 arr.toList) =
    List.foldlM (fun bs a => bs.push <$> f a) #[] arr.toList