-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
    mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[]

Proof state:
case mk.nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
k : List β
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k [] =
    List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray []

Tactic:
simp

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 β
l : Array α
⊢ mapM f l =
    foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (acc.push __do_lift))
      #[] l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM f { toList := l } =
    foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (acc.push __do_lift))
      #[] { toList := l }

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
this :
  ∀ (k : List β),
    (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) [] l =
    List.foldlM (fun x y => x.push <$> f y) #[] l

Tactic:
exact this []

Result:
no goals

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ List.toArray <$> List.mapM f l = List.foldlM (fun x y => x.push <$> f y) #[] l

Tactic:
rw [List.mapM_eq_reverse_foldlM_cons]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ List.toArray <$>
      List.reverse <$>
        List.foldlM
          (fun acc a => do
            let __do_lift ← f a
            pure (__do_lift :: acc))
          [] l =
    List.foldlM (fun x y => x.push <$> f y) #[] l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ ∀ (k : List β),
    (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l

Tactic:
intro k

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
k : List β
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
    List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) [] l =
    List.foldlM (fun x y => x.push <$> f y) #[] l

Tactic:
suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
    List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
  exact this []

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ ∀ (k : List β),
    (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l

Proof state:
case mk.cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
as : List α
ih :
  ∀ (k : List β),
    (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k as =
      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray as
k : List β
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k (a :: as) =
    List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray (a :: as)

Tactic:
simp [ih, List.foldlM_cons]

Result:
no goals

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ List.toArray <$>
      List.reverse <$>
        List.foldlM
          (fun acc a => do
            let __do_lift ← f a
            pure (__do_lift :: acc))
          [] l =
    List.foldlM (fun x y => x.push <$> f y) #[] l

Tactic:
simp only [bind_pure_comp, Functor.map_map]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) [] l =
    List.foldlM (fun x y => x.push <$> f y) #[] l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM f { toList := l } =
    foldlM
      (fun acc a => do
        let __do_lift ← f a
        pure (acc.push __do_lift))
      #[] { toList := l }

Tactic:
simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ List.toArray <$> List.mapM f l = List.foldlM (fun x y => x.push <$> f y) #[] l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
k : List β
⊢ (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
    List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l

Tactic:
induction l generalizing k with
| nil => simp
| cons a as ih =>
  simp [ih, List.foldlM_cons]

Result:
no goals