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

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

Result:
case cons.h_2.mpr.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 = false
pb : p b = true
as : List α✝
h₂ : ∀ (a : α✝), a ∈ as → p a = false
bs : List α✝
h₁ : x :: xs = as ++ b :: bs
⊢ ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false

Proof state:
case cons.h_2.mpr.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 = false
pb : p b = true
as : List α✝
h₂ : ∀ (a : α✝), a ∈ as → p a = false
bs : List α✝
h₁ : x :: xs = as ++ b :: bs
⊢ ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α✝), a ∈ as → p a = false

Tactic:
cases as with
| nil => simp_all
| cons a as =>
  refine ⟨as, ⟨⟨bs, ?_⟩, fun a m => h₂ a (mem_cons_of_mem _ m)⟩⟩
  cases h₁
  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
⊢ ∀ (a : α✝), a ∈ x :: as → p a = false

Tactic:
intro a 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 :: as
⊢ p a = false

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

Tactic:
rintro ⟨as, ⟨⟨bs, rfl⟩, h₁⟩⟩

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
⊢ ∃ as_1, (∃ x_1, x :: (as ++ b :: bs) = as_1 ++ b :: x_1) ∧ ∀ (a : α✝), a ∈ as_1 → 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:
obtain ⟨rfl, -⟩ := h₁

Result:
case cons.h_1.mpr.intro.intro.intro.intro.cons.refl
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
x✝ : Bool
h : p x = true
bs as : List α✝
h₂ : (!p x) = true
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
⊢ x = b

Proof state:
case cons.h_1.mpr.intro.intro.intro.intro.cons.refl
α✝ : Type u_1
b : α✝
p : α✝ → Bool
x : α✝
x✝ : Bool
h : p x = true
bs as : List α✝
h₂ : (!p x) = true
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
⊢ x = b

Tactic:
simp_all

Result:
no goals

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

Tactic:
exact h

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
simp only [ih, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]

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