-- 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:
case cons.e_a
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 β
⊢ (fun x => do
      let init ←
        match x 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) =
    fun a =>
    toArray <$>
      match a with
      | none => filterMapM.loop f xs acc
      | some b => filterMapM.loop f xs (b :: acc)

Tactic:
funext o

Result:
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)

Proof state:
case cons
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 x ← f x
      let init ←
        match x 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) =
    do
    let a ← f x
    toArray <$>
        match a with
        | none => filterMapM.loop f xs acc
        | some b => filterMapM.loop f xs (b :: acc)

Tactic:
congr

Result:
case cons.e_a
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 β
⊢ (fun x => do
      let init ←
        match x 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) =
    fun a =>
    toArray <$>
      match a with
      | none => filterMapM.loop f xs acc
      | some b => filterMapM.loop f xs (b :: acc)

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✝ : β
⊢ (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)

Tactic:
simp only [pure_bind]

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)
      (acc.reverse ++ [val✝]).toArray xs =
    toArray <$> filterMapM.loop f xs (val✝ :: acc)

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)
      (val✝ :: acc).reverse.toArray xs =
    toArray <$> filterMapM.loop f xs (val✝ :: acc)

Tactic:
exact ih _

Result:
no goals

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)
      #[] l =
    toArray <$> filterMapM.loop f l []

Tactic:
conv => lhs; rw [← reverse_nil]

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)
      [].reverse.toArray l =
    toArray <$> filterMapM.loop f l []