-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_guard (l : List α) : findSome? (Option.guard fun x => p x) l = find? p l

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
⊢ (match Option.guard (fun x => p x = true) x with
    | some b => some b
    | none => findSome? (Option.guard fun x => p x = true) xs) =
    match p x with
    | true => some x
    | false => find? p xs

Tactic:
split <;> rename_i h

Result:
case cons.h_1
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
b✝ : α
h : Option.guard (fun x => p x = true) x = some b✝
⊢ some b✝ =
    match p x with
    | true => some x
    | false => find? p xs

case cons.h_2
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
h : Option.guard (fun x => p x = true) x = none
⊢ findSome? (Option.guard fun x => p x = true) xs =
    match p x with
    | true => some x
    | false => find? p xs

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
⊢ findSome? (Option.guard fun x => p x = true) (x :: xs) = find? p (x :: xs)

Tactic:
simp [guard, findSome?, find?]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
⊢ (match Option.guard (fun x => p x = true) x with
    | some b => some b
    | none => findSome? (Option.guard fun x => p x = true) xs) =
    match p x with
    | true => some x
    | false => find? p xs

Proof state:
case cons.h_1.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
h : p x = true
⊢ some x =
    match p x with
    | true => some x
    | false => find? p xs

Tactic:
simp [h]

Result:
no goals

Proof state:
case cons.h_2
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
h : Option.guard (fun x => p x = true) x = none
⊢ findSome? (Option.guard fun x => p x = true) xs =
    match p x with
    | true => some x
    | false => find? p xs

Tactic:
simp only [Option.guard_eq_none] at h

Result:
case cons.h_2
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
h : ¬p x = true
⊢ findSome? (Option.guard fun x => p x = true) xs =
    match p x with
    | true => some x
    | false => find? p xs

Proof state:
case cons.h_1
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
b✝ : α
h : Option.guard (fun x => p x = true) x = some b✝
⊢ some b✝ =
    match p x with
    | true => some x
    | false => find? p xs

Tactic:
simp only [Option.guard_eq_some] at h

Result:
case cons.h_1
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
b✝ : α
h : x = b✝ ∧ p x = true
⊢ some b✝ =
    match p x with
    | true => some x
    | false => find? p xs

Proof state:
case cons.h_1
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
b✝ : α
h : x = b✝ ∧ p x = true
⊢ some b✝ =
    match p x with
    | true => some x
    | false => find? p xs

Tactic:
obtain ⟨rfl, h⟩ := h

Result:
case cons.h_1.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
h : p x = true
⊢ some x =
    match p x with
    | true => some x
    | false => find? p xs

Proof state:
case cons.h_2
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findSome? (Option.guard fun x => p x = true) xs = find? p xs
x✝ : Option α
h : ¬p x = true
⊢ findSome? (Option.guard fun x => p x = true) xs =
    match p x with
    | true => some x
    | false => find? p xs

Tactic:
simp [ih, h]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findSome? (Option.guard fun x => p x = true) [] = find? p []

Tactic:
simp

Result:
no goals