-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem find?_toArray (f : α → Bool) (l : List α) :
    l.toArray.find? f = l.find? f

Proof state:
α : Type u_1
f : α → Bool
l : List α
⊢ (match
      (forIn l ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f l

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
  by_cases f a <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → Bool
a : α
l : List α
ih :
  (match
      (forIn l ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f l
⊢ (match
      (match if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b =>
          forIn l b fun a r =>
            if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
            else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    match f a with
    | true => some a
    | false => find? f l

Tactic:
by_cases f a <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → Bool
⊢ (match
      (forIn [] ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → Bool
a : α
l : List α
ih :
  (match
      (forIn l ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f l
⊢ (match
      (forIn (a :: l) ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f (a :: l)

Tactic:
simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]

Result:
case cons
α : Type u_1
f : α → Bool
a : α
l : List α
ih :
  (match
      (forIn l ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f l
⊢ (match
      (match if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩ else ForInStep.yield ⟨none, PUnit.unit⟩ with
        | ForInStep.done b => b
        | ForInStep.yield b =>
          forIn l b fun a r =>
            if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
            else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    match f a with
    | true => some a
    | false => find? f l

Proof state:
α : Type u_1
f : α → Bool
l : List α
⊢ (do
        let r ←
          forIn l.toArray ⟨none, PUnit.unit⟩ fun a r =>
              let r := r.snd;
              if f a = 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 → Id (Option α) := fun y => pure none
        match r.fst with
          | none => do
            let y ← pure PUnit.unit
            __do_jp y
          | some a => pure a).run =
    find? f l

Tactic:
simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]

Result:
α : Type u_1
f : α → Bool
l : List α
⊢ (match
      (forIn l ⟨none, PUnit.unit⟩ fun a r =>
          if f a = true then ForInStep.done ⟨some (some a), PUnit.unit⟩
          else ForInStep.yield ⟨none, PUnit.unit⟩).fst with
    | none => none
    | some a => a) =
    find? f l

Proof state:
α : Type u_1
f : α → Bool
l : List α
⊢ Array.find? f l.toArray = find? f l

Tactic:
rw [Array.find?]

Result:
α : Type u_1
f : α → Bool
l : List α
⊢ (do
        let r ←
          forIn l.toArray ⟨none, PUnit.unit⟩ fun a r =>
              let r := r.snd;
              if f a = 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 → Id (Option α) := fun y => pure none
        match r.fst with
          | none => do
            let y ← pure PUnit.unit
            __do_jp y
          | some a => pure a).run =
    find? f l