-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem flatMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Array β)) :
    l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Array β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) #[] l =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) l []

Tactic:
conv => lhs; arg 2; change [].reverse.flatten.toArray

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Array β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) [].reverse.flatten.toArray l =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) l []

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Array β)
⊢ Array.flatMapM f l.toArray = toArray <$> flatMapM (fun a => Array.toList <$> f a) l

Tactic:
simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Array β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) #[] l =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) l []

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
a : Array β
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) (acc.reverse.flatten.toArray ++ a) xs =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

Tactic:
conv => lhs; rw [Array.toArray_append, ← flatten_concat, ← reverse_cons]

Result:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
a : Array β
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) (a.toList :: acc).reverse.flatten.toArray xs =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Array β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) [].reverse.flatten.toArray l =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) l []

Tactic:
generalize [] = acc

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Array β)
acc : List (List β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray l =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) l acc

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
a : Array β
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) (a.toList :: acc).reverse.flatten.toArray xs =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

Tactic:
exact 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
l : List α
f : α → m (Array β)
acc : List (List β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray l =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) l acc

Tactic:
induction l generalizing acc with
| nil => simp only [foldlM_nil, flatMapM.loop, map_pure]
| cons x xs ih =>
  simp only [foldlM_cons, bind_map_left, flatMapM.loop, _root_.map_bind]
  congr; funext a
  conv => lhs; rw [Array.toArray_append, ← flatten_concat, ← reverse_cons]
  exact ih _

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 (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
⊢ (do
      let a ← f x
      List.foldlM (fun x y => HAppend.hAppend x <$> f y) (acc.reverse.flatten.toArray ++ a) xs) =
    do
    let a ← f x
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

Tactic:
congr

Result:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
⊢ (fun a => List.foldlM (fun x y => HAppend.hAppend x <$> f y) (acc.reverse.flatten.toArray ++ a) xs) = fun a =>
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

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 (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray (x :: xs) =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) (x :: xs) acc

Tactic:
simp only [foldlM_cons, bind_map_left, flatMapM.loop, _root_.map_bind]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
⊢ (do
      let a ← f x
      List.foldlM (fun x y => HAppend.hAppend x <$> f y) (acc.reverse.flatten.toArray ++ a) xs) =
    do
    let a ← f x
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
⊢ (fun a => List.foldlM (fun x y => HAppend.hAppend x <$> f y) (acc.reverse.flatten.toArray ++ a) xs) = fun a =>
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)

Tactic:
funext a

Result:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
x : α
xs : List α
ih :
  ∀ (acc : List (List β)),
    List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray xs =
      toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs acc
acc : List (List β)
a : Array β
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) (acc.reverse.flatten.toArray ++ a) xs =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) xs (a.toList :: acc)