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

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

Tactic:
simp [Array.filterMapM, filterMapM]

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Option β)
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      #[] l =
    toArray <$> filterMapM.loop f l []

Proof state:
case cons.e_a.h.some
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
val✝ : β
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      (acc.reverse ++ [val✝]).toArray xs =
    toArray <$> filterMapM.loop f xs (val✝ :: acc)

Tactic:
rw [← List.reverse_cons]

Result:
case cons.e_a.h.some
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
val✝ : β
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      (val✝ :: acc).reverse.toArray xs =
    toArray <$> filterMapM.loop f xs (val✝ :: acc)

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Option β)
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      [].reverse.toArray l =
    toArray <$> filterMapM.loop f l []

Tactic:
generalize [] = acc

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → m (Option β)
acc : List β
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      acc.reverse.toArray l =
    toArray <$> filterMapM.loop f l acc

Proof state:
case cons.e_a.h.none
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
⊢ List.foldlM
      (fun x y => do
        let __do_lift ← f y
        match __do_lift with
          | some b => pure (x.push b)
          | none => pure x)
      acc.reverse.toArray xs =
    toArray <$> filterMapM.loop f xs acc

Tactic:
exact ih acc

Result:
no goals

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
o : Option β
⊢ (do
      let init ←
        match o with
          | some b => pure (acc.reverse ++ [b]).toArray
          | none => pure acc.reverse.toArray
      List.foldlM
          (fun x y => do
            let __do_lift ← f y
            match __do_lift with
              | some b => pure (x.push b)
              | none => pure x)
          init xs) =
    toArray <$>
      match o with
      | none => filterMapM.loop f xs acc
      | some b => filterMapM.loop f xs (b :: acc)

Tactic:
cases o

Result:
case cons.e_a.h.none
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
⊢ (do
      let init ←
        match none with
          | some b => pure (acc.reverse ++ [b]).toArray
          | none => pure acc.reverse.toArray
      List.foldlM
          (fun x y => do
            let __do_lift ← f y
            match __do_lift with
              | some b => pure (x.push b)
              | none => pure x)
          init xs) =
    toArray <$>
      match none with
      | none => filterMapM.loop f xs acc
      | some b => filterMapM.loop f xs (b :: acc)

case cons.e_a.h.some
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
x : α
xs : List α
ih :
  ∀ (acc : List β),
    List.foldlM
        (fun x y => do
          let __do_lift ← f y
          match __do_lift with
            | some b => pure (x.push b)
            | none => pure x)
        acc.reverse.toArray xs =
      toArray <$> filterMapM.loop f xs acc
acc : List β
val✝ : β
⊢ (do
      let init ←
        match some val✝ with
          | some b => pure (acc.reverse ++ [b]).toArray
          | none => pure acc.reverse.toArray
      List.foldlM
          (fun x y => do
            let __do_lift ← f y
            match __do_lift with
              | some b => pure (x.push b)
              | none => pure x)
          init xs) =
    toArray <$>
      match some val✝ with
      | none => filterMapM.loop f xs acc
      | some b => filterMapM.loop f xs (b :: acc)