m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] (List.reverse arr.data) =
    do
    let __do_lift ← List.mapM f arr.data
    pure { data := __do_lift }
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 = do
    let __do_lift ← List.mapM f arr.data
    pure { data := __do_lift }
rw [mapM, foldlM_eq_foldlM_data, ← List.foldrM_reverse, mkEmpty_eq]
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] (List.reverse arr.data) =
    do
    let __do_lift ← List.mapM f (List.reverse (List.reverse arr.data))
    pure { data := __do_lift }
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] (List.reverse arr.data) =
    do
    let __do_lift ← List.mapM f arr.data
    pure { data := __do_lift }
conv => rhs; rw [← List.reverse_reverse arr.data]
no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] (List.reverse arr.data) =
    do
    let __do_lift ← List.mapM f (List.reverse (List.reverse arr.data))
    pure { data := __do_lift }
induction arr.data.reverse with
| nil => simp; rfl
| cons a l ih => simp [ih]; simp [push]
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ pure #[] = pure { data := [] }
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] [] =
    do
    let __do_lift ← List.mapM f (List.reverse [])
    pure { data := __do_lift }
simp
no goals
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ pure #[] = pure { data := [] }
rfl
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
a : α
l : List α
ih :
  List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] l =
    do
    let __do_lift ← List.mapM f (List.reverse l)
    pure { data := __do_lift }
⊢ (do
      let x ← List.mapM f (List.reverse l)
      let b ← f a
      pure (push { data := x } b)) =
    do
    let x ← List.mapM f (List.reverse l)
    let x_1 ← f a
    pure { data := x ++ [x_1] }
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
a : α
l : List α
ih :
  List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] l =
    do
    let __do_lift ← List.mapM f (List.reverse l)
    pure { data := __do_lift }
⊢ List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] (a :: l) =
    do
    let __do_lift ← List.mapM f (List.reverse (a :: l))
    pure { data := __do_lift }
simp [ih]
no goals
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
a : α
l : List α
ih :
  List.foldrM
      (fun a bs => do
        let b ← f a
        pure (push bs b))
      #[] l =
    do
    let __do_lift ← List.mapM f (List.reverse l)
    pure { data := __do_lift }
⊢ (do
      let x ← List.mapM f (List.reverse l)
      let b ← f a
      pure (push { data := x } b)) =
    do
    let x ← List.mapM f (List.reverse l)
    let x_1 ← f a
    pure { data := x ++ [x_1] }
simp [push]