-- 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.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)

Tactic:
simp only [↓reduceIte, ← reverse_cons, pure_bind, cond_true]

Result:
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 α
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      (x :: acc).reverse.toArray xs =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (x :: acc)

Proof state:
case cons
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 x_1 ← p x
      let init ← if x_1 = 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) =
    do
    let a ← p x
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif a then x :: acc else acc)

Tactic:
congr

Result:
case cons.e_a
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 α
⊢ (fun x_1 => do
      let init ← if x_1 = 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 => (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif a then x :: acc else acc)

Proof state:
case cons.e_a
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 α
⊢ (fun x_1 => do
      let init ← if x_1 = 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 => (fun a => a.reverse.toArray) <$> filterAuxM p xs (bif a then x :: acc else acc)

Tactic:
funext b

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

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 α
⊢ 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

Tactic:
exact ih acc

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ Array.filterM p l.toArray = toArray <$> filterM p l

Tactic:
simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map]

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)
      #[] l =
    (fun a => a.reverse.toArray) <$> filterAuxM p l []

Proof state:
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 α
⊢ List.foldlM
      (fun r a => do
        let __do_lift ← p a
        if __do_lift = true then pure (r.push a) else pure r)
      (x :: acc).reverse.toArray xs =
    (fun a => a.reverse.toArray) <$> filterAuxM p xs (x :: acc)

Tactic:
exact ih (x :: acc)

Result:
no goals