-- 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_2.mp.intro.intro.intro
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
x✝ : Bool
h : p x = false
pb : p b = true
as : List α✝
h₁ : ∀ (a : α✝), a ∈ as → p a = false
bs : List α✝
ih :
  find? p (as ++ b :: bs) = some b ↔
    p b = true ∧ ∃ as_1 bs_1, as ++ b :: bs = as_1 ++ b :: bs_1 ∧ ∀ (a : α✝), a ∈ as_1 → (!p a) = true
a : α✝
m : a ∈ x :: as
⊢ p a = false

Tactic:
simp at m

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

Proof state:
case cons.h_1.mpr.intro.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 = true
bs : List α✝
h₂ : ∀ (a : α✝), a ∈ [] → (!p a) = true
h₁ : x :: xs = [] ++ b :: bs
⊢ x = b

Tactic:
simp_all

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
refine ⟨x :: as, ⟨⟨bs, rfl⟩, ?_⟩⟩

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

Proof state:
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

Tactic:
simp only [Option.some.injEq]

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
⊢ x = b ↔ p b = true ∧ ∃ as, (∃ x_1, x :: xs = as ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

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

Tactic:
exact h₁ a m

Result:
no goals

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

Tactic:
obtain (rfl|m) := m

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

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

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₁ : x :: xs = a :: as ++ b :: bs
h₂ : (!p a) = true
⊢ x = b

Tactic:
simp only [cons_append] at h₁

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
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

Tactic:
exact ⟨h, [], ⟨xs, rfl⟩, by simp⟩

Result:
no goals

Proof state:
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

Tactic:
cases as with
| nil => simp_all
| cons a as =>
  specialize h₂ a (mem_cons_self _ _)
  simp only [cons_append] at h₁
  obtain ⟨rfl, -⟩ := h₁
  simp_all

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
b : α✝
p : α✝ → Bool
⊢ find? p [] = some b ↔ p b = true ∧ ∃ as bs, [] = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Tactic:
simp

Result:
no goals

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
⊢ xs = as ++ b :: bs

Tactic:
cases h₁

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