-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_filterMap' (f : α → Option β) (l : Array α) (w : stop = l.size) :
    (l.filterMap f 0 stop).toList = l.toList.filterMap f

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (filterMap f l).toList = List.filterMap f l.toList

Tactic:
dsimp only [filterMap, filterMapM]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l).run.toList =
    List.filterMap f l.toList

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
f : α → Option β
l : Array α
w : stop = l.size
⊢ (filterMap f l 0 stop).toList = List.filterMap f l.toList

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (filterMap f l).toList = List.filterMap f l.toList

Proof state:
case refine_2.nil
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a []).run.toList =
      a.toList ++ List.filterMap f []

Tactic:
simp_all [Id.run]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (List.foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l.toList).run.toList =
    List.filterMap f l.toList

Tactic:
generalize l.toList = l

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
⊢ (List.foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l).run.toList =
    List.filterMap f l

Proof state:
case refine_2.cons
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (a : Array β),
    (List.foldlM
          (fun bs a =>
            match f a with
            | some b => bs.push b
            | none => bs)
          a tail✝).toList =
      a.toList ++ List.filterMap f tail✝
⊢ ∀ (a : Array β),
    (match f head✝ with
          | some b => a.push b
          | none => a).toList ++
        List.filterMap f tail✝ =
      a.toList ++
        match f head✝ with
        | none => List.filterMap f tail✝
        | some b => b :: List.filterMap f tail✝

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
⊢ ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a l).run.toList =
      a.toList ++ List.filterMap f l

Tactic:
induction l

Result:
case refine_2.nil
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a []).run.toList =
      a.toList ++ List.filterMap f []

case refine_2.cons
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a tail✝).run.toList =
      a.toList ++ List.filterMap f tail✝
⊢ ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a (head✝ :: tail✝)).run.toList =
      a.toList ++ List.filterMap f (head✝ :: tail✝)

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l).run.toList =
    List.filterMap f l.toList

Tactic:
rw [← foldlM_toList]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (List.foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l.toList).run.toList =
    List.filterMap f l.toList

Proof state:
case refine_2.cons
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a tail✝).run.toList =
      a.toList ++ List.filterMap f tail✝
⊢ ∀ (a : Array β),
    (List.foldlM
            (fun bs a => do
              let __do_lift ← f a
              match __do_lift with
                | some b => pure (bs.push b)
                | none => pure bs)
            a (head✝ :: tail✝)).run.toList =
      a.toList ++ List.filterMap f (head✝ :: tail✝)

Tactic:
simp_all [Id.run, List.filterMap_cons]

Result:
case refine_2.cons
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (a : Array β),
    (List.foldlM
          (fun bs a =>
            match f a with
            | some b => bs.push b
            | none => bs)
          a tail✝).toList =
      a.toList ++ List.filterMap f tail✝
⊢ ∀ (a : Array β),
    (match f head✝ with
          | some b => a.push b
          | none => a).toList ++
        List.filterMap f tail✝ =
      a.toList ++
        match f head✝ with
        | none => List.filterMap f tail✝
        | some b => b :: List.filterMap f tail✝

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
⊢ (List.foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l).run.toList =
    List.filterMap f l

Tactic:
have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
  a.toList ++ List.filterMap f l := ?_

Result:
case refine_3
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
this : ∀ (a : Array β), (List.foldlM ?refine_1 a l).run.toList = a.toList ++ List.filterMap f l
⊢ (List.foldlM
          (fun bs a => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (bs.push b)
              | none => pure bs)
          #[] l).run.toList =
    List.filterMap f l

case refine_1
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
a : Array β
⊢ Array β → α → Id (Array β)

case refine_2
α : Type u_1
β : Type u_2
f : α → Option β
l✝ : Array α
l : List α
⊢ ∀ (a : Array β), (List.foldlM ?refine_1 a l).run.toList = a.toList ++ List.filterMap f l