-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Control.lean
theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
    as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none

Proof state:
case nil
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
⊢ findM? p [] =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      []

Tactic:
rfl

Result:
no goals

Proof state:
case cons.e_a
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ (fun __do_lift =>
      match __do_lift with
      | true => pure (some a)
      | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
    fun a_1 =>
    match if a_1 = true then some a else none with
    | some b => pure (some b)
    | none => findSomeM? (fun a => (fun a_2 => if a_2 = true then some a else none) <$> p a) as

Tactic:
apply funext

Result:
case cons.e_a.h
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ ∀ (x : Bool),
    (match x with
      | true => pure (some a)
      | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
      match if x = true then some a else none with
      | some b => pure (some b)
      | none => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as

Proof state:
case cons.e_a.h
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ ∀ (x : Bool),
    (match x with
      | true => pure (some a)
      | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
      match if x = true then some a else none with
      | some b => pure (some b)
      | none => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as

Tactic:
intro b

Result:
case cons.e_a.h
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
b : Bool
⊢ (match b with
    | true => pure (some a)
    | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
    match if b = true then some a else none with
    | some b => pure (some b)
    | none => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
as : List α
⊢ findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as

Tactic:
induction as with
| nil => rfl
| cons a as ih =>
  simp only [findM?, findSomeM?]
  simp [ih]
  congr
  apply funext
  intro b
  cases b <;> simp

Result:
no goals

Proof state:
case cons
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => findM? p as) =
    do
    let __do_lift ←
      do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none)
    match __do_lift with
      | some b => pure (some b)
      | none =>
        findSomeM?
          (fun a => do
            let __do_lift ← p a
            pure (if __do_lift = true then some a else none))
          as

Tactic:
simp [ih]

Result:
case cons
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
    do
    let a_1 ← p a
    match if a_1 = true then some a else none with
      | some b => pure (some b)
      | none => findSomeM? (fun a => (fun a_2 => if a_2 = true then some a else none) <$> p a) as

Proof state:
case cons
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ findM? p (a :: as) =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      (a :: as)

Tactic:
simp only [findM?, findSomeM?]

Result:
case cons
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => findM? p as) =
    do
    let __do_lift ←
      do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none)
    match __do_lift with
      | some b => pure (some b)
      | none =>
        findSomeM?
          (fun a => do
            let __do_lift ← p a
            pure (if __do_lift = true then some a else none))
          as

Proof state:
case cons
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ (do
      let __do_lift ← p a
      match __do_lift with
        | true => pure (some a)
        | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
    do
    let a_1 ← p a
    match if a_1 = true then some a else none with
      | some b => pure (some b)
      | none => findSomeM? (fun a => (fun a_2 => if a_2 = true then some a else none) <$> p a) as

Tactic:
congr

Result:
case cons.e_a
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
⊢ (fun __do_lift =>
      match __do_lift with
      | true => pure (some a)
      | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
    fun a_1 =>
    match if a_1 = true then some a else none with
    | some b => pure (some b)
    | none => findSomeM? (fun a => (fun a_2 => if a_2 = true then some a else none) <$> p a) as