-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_eq_some_iff_append :
    xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ a ∈ as, !p a

Proof state:
case cons.h_1.mpr.intro.intro.intro.intro.cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = true
bs : List α✝
a : α✝
as : List α✝
h₂ : ∀ (a_1 : α✝), a_1 ∈ a :: as → (!p a_1) = true
h₁ : x :: xs = a :: as ++ b :: bs
⊢ x = b

Tactic:
specialize h₂ a (mem_cons_self _ _)

Result:
case cons.h_1.mpr.intro.intro.intro.intro.cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = true
bs : List α✝
a : α✝
as : List α✝
h₁ : x :: xs = a :: as ++ b :: bs
h₂ : (!p a) = true
⊢ x = b

Proof state:
case cons.h_1.mp
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = true
⊢ x = b → p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Tactic:
rintro rfl

Result:
case cons.h_1.mp
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
x✝ : Bool
h : p x = true
ih : find? p xs = some x ↔ p x = true ∧ ∃ as bs, xs = as ++ x :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
⊢ p x = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ x :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Proof state:
case cons.h_2.mpr.intro.intro.intro.nil
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
bs : List α✝
h₂ : ∀ (a : α✝), a ∈ [] → p a = false
h₁ : x :: xs = [] ++ b :: bs
⊢ ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.h_2
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false) ↔
    ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → p a = false

Tactic:
constructor

Result:
case cons.h_2.mp
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false) →
    ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → p a = false

case cons.h_2.mpr
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
⊢ (∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → p a = false) →
    ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false

Proof state:
case cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
⊢ (match p x with
      | true => some x
      | false => find? p xs) =
      some b ↔
    p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Tactic:
split <;> rename_i h

Result:
case cons.h_1
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = true
⊢ some x = some b ↔ p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

case cons.h_2
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
⊢ find? p xs = some b ↔ p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Proof state:
case cons.h_1.mpr
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = true
⊢ (p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true) → x = b

Tactic:
rintro ⟨-, ⟨as, ⟨⟨bs, h₁⟩, h₂⟩⟩⟩

Result:
case cons.h_1.mpr.intro.intro.intro.intro
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = true
as : List α✝
h₂ : ∀ (a : α✝), a ∈ as → (!p a) = true
bs : List α✝
h₁ : x :: xs = as ++ b :: bs
⊢ x = b

Proof state:
case cons.h_2.mpr.intro.intro.intro.cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
bs : List α✝
a : α✝
as : List α✝
h₂ : ∀ (a_1 : α✝), a_1 ∈ a :: as → p a_1 = false
h₁ : x :: xs = a :: as ++ b :: bs
⊢ ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false

Tactic:
refine ⟨as, ⟨⟨bs, ?_⟩, fun a m => h₂ a (mem_cons_of_mem _ m)⟩⟩

Result:
case cons.h_2.mpr.intro.intro.intro.cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
bs : List α✝
a : α✝
as : List α✝
h₂ : ∀ (a_1 : α✝), a_1 ∈ a :: as → p a_1 = false
h₁ : x :: xs = a :: as ++ b :: bs
⊢ xs = as ++ b :: bs

Proof state:
case cons.h_2
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
⊢ p b = true →
    ((∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false) ↔
      ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → p a = false)

Tactic:
intro pb

Result:
case cons.h_2
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
x✝ : Bool
h : p x = false
pb : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false) ↔
    ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → p a = false

Proof state:
α✝ : Type u_1
p : α✝ → Bool
x : α✝
xs : List α✝
x✝ : Bool
h : p x = true
ih : find? p xs = some x ↔ p x = true ∧ ∃ as bs, xs = as ++ x :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
⊢ ∀ (a : α✝), a ∈ [] → (!p a) = true

Tactic:
simp

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
⊢ find? p (x :: xs) = some b ↔ p b = true ∧ ∃ as bs, x :: xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Tactic:
simp only [find?_cons, exists_and_right]

Result:
case cons
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
xs : List α✝
ih : find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true
⊢ (match p x with
      | true => some x
      | false => find? p xs) =
      some b ↔
    p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true