-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Find.lean
theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j]

Proof state:
case mp.intro.intro.intro
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ ∃ i h, (as ++ b :: bs)[i] = b ∧ ∀ (j : Nat) (hj : j < i), p (as ++ b :: bs)[j] = false

Tactic:
refine ⟨as.length, ⟨?_, ?_, ?_⟩⟩

Result:
case mp.intro.intro.intro.refine_1
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ as.length < (as ++ b :: bs).length

case mp.intro.intro.intro.refine_2
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ (as ++ b :: bs)[as.length] = b

case mp.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ ∀ (j : Nat) (hj : j < as.length), p (as ++ b :: bs)[j] = false

Proof state:
case mp.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ ∀ (j : Nat) (hj : j < as.length), p (as ++ b :: bs)[j] = false

Tactic:
intro j h'

Result:
case mp.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
j : Nat
h' : j < as.length
⊢ p (as ++ b :: bs)[j] = false

Proof state:
case mpr.intro.intro.intro.refine_2
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
⊢ ∀ (a : α), a ∈ take i xs → p a = false

Tactic:
intro a m

Result:
case mpr.intro.intro.intro.refine_2
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
a : α
m : a ∈ take i xs
⊢ p a = false

Proof state:
case mp.intro.intro.intro.refine_1
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ as.length < (as ++ b :: bs).length

Tactic:
simp only [length_append, length_cons]

Result:
case mp.intro.intro.intro.refine_1
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ as.length < as.length + (bs.length + 1)

Proof state:
α : Type u_1
xs : List α
p : α → Bool
b : α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
    ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false

Tactic:
constructor

Result:
case mp
α : Type u_1
xs : List α
p : α → Bool
b : α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) →
    ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false

case mpr
α : Type u_1
xs : List α
p : α → Bool
b : α
w : p b = true
⊢ (∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false) →
    ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Proof state:
case mpr.intro.intro.intro.refine_2.intro.intro
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h✝ : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
j : Nat
h : j < min i xs.length
⊢ p xs[j] = false

Tactic:
apply h'

Result:
case mpr.intro.intro.intro.refine_2.intro.intro.hj
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h✝ : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
j : Nat
h : j < min i xs.length
⊢ j < i

Proof state:
case mpr.intro.intro.intro
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
⊢ ∃ as, (∃ x, xs = as ++ xs[i] :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Tactic:
refine ⟨xs.take i, ⟨xs.drop (i+1), ?_⟩, ?_⟩

Result:
case mpr.intro.intro.intro.refine_1
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
⊢ xs = take i xs ++ xs[i] :: drop (i + 1) xs

case mpr.intro.intro.intro.refine_2
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
⊢ ∀ (a : α), a ∈ take i xs → p a = false

Proof state:
case mpr.intro.intro.intro.refine_2.intro.intro.hj
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h✝ : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
j : Nat
h : j < min i xs.length
⊢ j < i

Tactic:
omega

Result:
no goals

Proof state:
case mpr.intro.intro.intro.refine_2
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
a : α
m : a ∈ take i xs
⊢ p a = false

Tactic:
rw [mem_take_iff_getElem] at m

Result:
case mpr.intro.intro.intro.refine_2
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
a : α
m : ∃ i_1 hm, xs[i_1] = a
⊢ p a = false

Proof state:
case mpr
α : Type u_1
xs : List α
p : α → Bool
b : α
w : p b = true
⊢ (∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false) →
    ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Tactic:
rintro ⟨i, h, rfl, h'⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
⊢ ∃ as, (∃ x, xs = as ++ xs[i] :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Proof state:
case mpr.intro.intro.intro.refine_1
α : Type u_1
xs : List α
p : α → Bool
i : Nat
h : i < xs.length
h' : ∀ (j : Nat) (hj : j < i), p xs[j] = false
w : p xs[i] = true
⊢ xs = take i xs ++ xs[i] :: drop (i + 1) xs

Tactic:
rw [getElem_cons_drop, take_append_drop]

Result:
no goals

Proof state:
case mp.intro.intro.intro.refine_2
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ (b :: bs)[as.length - as.length] = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
b : α
⊢ find? p xs = some b ↔ p b = true ∧ ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

Tactic:
rw [find?_eq_some_iff_append]

Result:
α : Type u_1
xs : List α
p : α → Bool
b : α
⊢ (p b = true ∧ ∃ as bs, xs = as ++ b :: bs ∧ ∀ (a : α), a ∈ as → (!p a) = true) ↔
    p b = true ∧ ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

Proof state:
case mp.intro.intro.intro.refine_3
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
j : Nat
h' : j < as.length
⊢ p as[j] = false

Tactic:
exact h _ (getElem_mem h')

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
b : α
⊢ p b = true →
    ((∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
      ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false)

Tactic:
intro w

Result:
α : Type u_1
xs : List α
p : α → Bool
b : α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
    ∃ i h, xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), p xs[j] = false

Proof state:
case mp.intro.intro.intro.refine_2
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ (as ++ b :: bs)[as.length] = b

Tactic:
rw [getElem_append_right (Nat.le_refl as.length)]

Result:
case mp.intro.intro.intro.refine_2
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
bs : List α
⊢ (b :: bs)[as.length - as.length] = b