-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
    l.toArray.findM? f = l.findM? f

Proof state:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
l : List α
⊢ (do
      let r ←
        forIn l.toArray ⟨none, PUnit.unit⟩ fun a r =>
            let r := r.snd;
            do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else do
                pure PUnit.unit
                pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      let __do_jp : PUnit → m (Option α) := fun y => pure none
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a) =
    findM? f l

Tactic:
simp only [bind_pure_comp, map_pure, forIn_toArray]

Result:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
l : List α
⊢ (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l

Proof state:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
l : List α
⊢ (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
  congr
  ext1 (_|_) <;> simp [ih]

Result:
no goals

Proof state:
case cons
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l
⊢ (do
      let r ←
        forIn (a :: l) ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f (a :: l)

Tactic:
simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]

Result:
case cons
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l
⊢ (do
      let x ← f a
      let x ←
        if x = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
          else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      let r ←
        match x with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            forIn l b fun a r => do
              let __do_lift ← f a
              if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
                else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    do
    let __do_lift ← f a
    match __do_lift with
      | true => pure (some a)
      | false => findM? f l

Proof state:
case cons.e_a
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l
⊢ (fun x => do
      let x ←
        if x = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
          else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      let r ←
        match x with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            forIn l b fun a r => do
              let __do_lift ← f a
              if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
                else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    fun __do_lift =>
    match __do_lift with
    | true => pure (some a)
    | false => findM? f l

Tactic:
ext1 (_|_) <;> simp [ih]

Result:
no goals

Proof state:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
l : List α
⊢ Array.findM? f l.toArray = findM? f l

Tactic:
rw [Array.findM?]

Result:
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
l : List α
⊢ (do
      let r ←
        forIn l.toArray ⟨none, PUnit.unit⟩ fun a r =>
            let r := r.snd;
            do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else do
                pure PUnit.unit
                pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      let __do_jp : PUnit → m (Option α) := fun y => pure none
      match r.fst with
        | none => do
          let y ← pure PUnit.unit
          __do_jp y
        | some a => pure a) =
    findM? f l