-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
    l.toArray.mapM f = List.toArray <$> l.mapM f

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 α
init : Array β
⊢ foldlM (fun bs a => bs.push <$> f a) init l.toArray = (fun x => init ++ x.toArray) <$> mapM' f l

Tactic:
induction l generalizing init with
| nil => simp
| cons a l ih =>
  simp only [foldlM_toArray] at ih
  rw [size_toArray, mapM'_cons, foldlM_toArray]
  simp [ih]

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 : List α
this :
  ∀ (init : Array β), foldlM (fun bs a => bs.push <$> f a) init l.toArray = (fun x => init ++ x.toArray) <$> mapM' f l
⊢ foldlM (fun bs a => bs.push <$> f a) #[] l.toArray = toArray <$> mapM' f l

Tactic:
simpa using this #[]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
l : List α
ih :
  ∀ (init : Array β), foldlM (fun bs a => bs.push <$> f a) init l.toArray = (fun x => init ++ x.toArray) <$> mapM' f l
init : Array β
⊢ foldlM (fun bs a => bs.push <$> f a) init (a :: l).toArray = (fun x => init ++ x.toArray) <$> mapM' f (a :: l)

Tactic:
simp only [foldlM_toArray] at ih

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
l : List α
init : Array β
ih : ∀ (init : Array β), List.foldlM (fun bs a => bs.push <$> f a) init l = (fun x => init ++ x.toArray) <$> mapM' f l
⊢ foldlM (fun bs a => bs.push <$> f a) init (a :: l).toArray = (fun x => init ++ x.toArray) <$> mapM' f (a :: 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 α
⊢ Array.mapM f l.toArray = toArray <$> mapM f l

Tactic:
simp only [← mapM'_eq_mapM, mapM_eq_foldlM]

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

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

Tactic:
simp

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
l : List α
init : Array β
ih : ∀ (init : Array β), List.foldlM (fun bs a => bs.push <$> f a) init l = (fun x => init ++ x.toArray) <$> mapM' f l
⊢ foldlM (fun bs a => bs.push <$> f a) init (a :: l).toArray = (fun x => init ++ x.toArray) <$> mapM' f (a :: l)

Tactic:
rw [size_toArray, mapM'_cons, foldlM_toArray]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
l : List α
init : Array β
ih : ∀ (init : Array β), List.foldlM (fun bs a => bs.push <$> f a) init l = (fun x => init ++ x.toArray) <$> mapM' f l
⊢ List.foldlM (fun bs a => bs.push <$> f a) init (a :: l) =
    (fun x => init ++ x.toArray) <$> do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f l
      pure (__do_lift :: __do_lift_1)

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 α
⊢ ∀ (init : Array β), foldlM (fun bs a => bs.push <$> f a) init l.toArray = (fun x => init ++ x.toArray) <$> mapM' f l

Tactic:
intro init

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
init : Array β
⊢ foldlM (fun bs a => bs.push <$> f a) init l.toArray = (fun x => init ++ x.toArray) <$> mapM' f l

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
l : List α
init : Array β
ih : ∀ (init : Array β), List.foldlM (fun bs a => bs.push <$> f a) init l = (fun x => init ++ x.toArray) <$> mapM' f l
⊢ List.foldlM (fun bs a => bs.push <$> f a) init (a :: l) =
    (fun x => init ++ x.toArray) <$> do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f l
      pure (__do_lift :: __do_lift_1)

Tactic:
simp [ih]

Result:
no goals