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

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
l : List α
⊢ (do
      let r ←
        forIn l.toArray ⟨none, PUnit.unit⟩ fun a r =>
            let r := r.snd;
            do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => 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) =
    findSomeM? f l

Tactic:
simp only [bind_pure_comp, map_pure, forIn_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
l : List α
⊢ (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findSomeM? f l

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
⊢ (do
      let r ←
        forIn [] ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findSomeM? f []

Tactic:
simp

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findSomeM? f l
⊢ (do
      let x ← f a
      let x ←
        match x with
          | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
          | x => 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
              match __do_lift with
                | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
                | x => 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
      | some b => pure (some b)
      | none => findSomeM? f l

Tactic:
congr

Result:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findSomeM? f l
⊢ (fun x => do
      let x ←
        match x with
          | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
          | x => 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
              match __do_lift with
                | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
                | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    fun __do_lift =>
    match __do_lift with
    | some b => pure (some b)
    | none => findSomeM? f l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
l : List α
⊢ (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findSomeM? f l

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

Result:
no goals

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Option β)
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            match __do_lift with
              | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
              | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findSomeM? f l
⊢ (fun x => do
      let x ←
        match x with
          | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
          | x => 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
              match __do_lift with
                | some b => pure (ForInStep.done ⟨some (some b), PUnit.unit⟩)
                | x => pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    fun __do_lift =>
    match __do_lift with
    | some b => pure (some b)
    | none => findSomeM? f l

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

Result:
no goals