-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem filterM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
    l.toArray.filterM p = toArray <$> l.filterM p

Proof state:
case cons.e_a.h.false
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
x : α
xs : List α
ih :
  ∀ (acc : List α),
    List.foldlM
        (fun r a => do
          let __do_lift ← p a
          if __do_lift = true then pure (r.push a) else pure r)
        acc.reverse.toArray xs =
      (fun a => a.reverse.toArray) <$> filterAuxM p xs acc
acc : List α
⊢ (do
      let init ← if false = true then pure (acc.reverse ++ [x]).toArray else pure acc.reverse.toArray
      List.foldlM
          (fun r a => do
            let __do_lift ← p a
            if __do_lift = true then pure (r.push a) else pure r)
          init xs) =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif false then x :: acc else acc)

Tactic:
simp only [Bool.false_eq_true, ↓reduceIte, pure_bind, cond_false]

Result:
case cons.e_a.h.false
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
x : α
xs : List α
ih :
  ∀ (acc : List α),
    List.foldlM
        (fun r a => do
          let __do_lift ← p a
          if __do_lift = true then pure (r.push a) else pure r)
        acc.reverse.toArray xs =
      (fun a => a.reverse.toArray) <$> filterAuxM p xs acc
acc : List α
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      acc.reverse.toArray xs =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs acc

Proof state:
case cons.e_a.h
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
x : α
xs : List α
ih :
  ∀ (acc : List α),
    List.foldlM
        (fun r a => do
          let __do_lift ← p a
          if __do_lift = true then pure (r.push a) else pure r)
        acc.reverse.toArray xs =
      (fun a => a.reverse.toArray) <$> filterAuxM p xs acc
acc : List α
b : Bool
⊢ (do
      let init ← if b = true then pure (acc.reverse ++ [x]).toArray else pure acc.reverse.toArray
      List.foldlM
          (fun r a => do
            let __do_lift ← p a
            if __do_lift = true then pure (r.push a) else pure r)
          init xs) =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif b then x :: acc else acc)

Tactic:
cases b

Result:
case cons.e_a.h.false
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
x : α
xs : List α
ih :
  ∀ (acc : List α),
    List.foldlM
        (fun r a => do
          let __do_lift ← p a
          if __do_lift = true then pure (r.push a) else pure r)
        acc.reverse.toArray xs =
      (fun a => a.reverse.toArray) <$> filterAuxM p xs acc
acc : List α
⊢ (do
      let init ← if false = true then pure (acc.reverse ++ [x]).toArray else pure acc.reverse.toArray
      List.foldlM
          (fun r a => do
            let __do_lift ← p a
            if __do_lift = true then pure (r.push a) else pure r)
          init xs) =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif false then x :: acc else acc)

case cons.e_a.h.true
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
x : α
xs : List α
ih :
  ∀ (acc : List α),
    List.foldlM
        (fun r a => do
          let __do_lift ← p a
          if __do_lift = true then pure (r.push a) else pure r)
        acc.reverse.toArray xs =
      (fun a => a.reverse.toArray) <$> filterAuxM p xs acc
acc : List α
⊢ (do
      let init ← if true = true then pure (acc.reverse ++ [x]).toArray else pure acc.reverse.toArray
      List.foldlM
          (fun r a => do
            let __do_lift ← p a
            if __do_lift = true then pure (r.push a) else pure r)
          init xs) =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif true then x :: acc else acc)

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      #[] l =
    (fun a => a.reverse.toArray) <$> filterAuxM p l []

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

Result:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      [].reverse.toArray l =
    (fun a => a.reverse.toArray) <$> filterAuxM p l []

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      [].reverse.toArray l =
    (fun a => a.reverse.toArray) <$> filterAuxM p l []

Tactic:
generalize [] = acc

Result:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
acc : List α
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      acc.reverse.toArray l =
    (fun a => a.reverse.toArray) <$> filterAuxM p l acc