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

Proof state:
α : Type u_1
p : α → Bool
b : α
xs : Array α
⊢ find? p xs = some b ↔ p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
⊢ find? p { toList := xs } = some b ↔
    p b = true ∧ ∃ as bs, { toList := xs } = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Proof state:
case mk.mp.intro.intro.intro
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
x : List α
⊢ ∃ as_1, (∃ x_1, { toList := as ++ b :: x } = as_1.push b ++ x_1) ∧ ∀ (a : α), a ∈ as_1 → p a = false

Tactic:
exact ⟨as.toArray, ⟨x.toArray, by simp⟩ , by simpa using h⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
as : Array α
h : ∀ (a : α), a ∈ as → p a = false
x : Array α
h' : { toList := xs } = as.push b ++ x
⊢ xs = as.toList ++ b :: x.toList

Tactic:
simpa using congrArg Array.toList h'

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
⊢ p b = true →
    ((∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
      ∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false)

Tactic:
intro w

Result:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
    ∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false

Proof state:
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
x : List α
⊢ ∀ (a : α), a ∈ as.toArray → p a = false

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk.mpr
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
⊢ (∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false) →
    ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Tactic:
rintro ⟨as, ⟨⟨x, h'⟩, h⟩⟩

Result:
case mk.mpr.intro.intro.intro
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
as : Array α
h : ∀ (a : α), a ∈ as → p a = false
x : Array α
h' : { toList := xs } = as.push b ++ x
⊢ ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Proof state:
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
as : Array α
h : ∀ (a : α), a ∈ as → p a = false
x : Array α
h' : { toList := xs } = as.push b ++ x
⊢ ∀ (a : α), a ∈ as.toList → p a = false

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
⊢ find? p { toList := xs } = some b ↔
    p b = true ∧ ∃ as bs, { toList := xs } = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
simp only [List.find?_toArray, List.find?_eq_some_iff_append, Bool.not_eq_eq_eq_not,
  Bool.not_true, exists_and_right, and_congr_right_iff]

Result:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
⊢ p b = true →
    ((∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
      ∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false)

Proof state:
case mk
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) ↔
    ∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false

Tactic:
constructor

Result:
case mk.mp
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) →
    ∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false

case mk.mpr
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
⊢ (∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false) →
    ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Proof state:
case mk.mpr.intro.intro.intro
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
as : Array α
h : ∀ (a : α), a ∈ as → p a = false
x : Array α
h' : { toList := xs } = as.push b ++ x
⊢ ∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false

Tactic:
exact ⟨as.toList, ⟨x.toList, by simpa using congrArg Array.toList h'⟩,
  by simpa using h⟩

Result:
no goals

Proof state:
case mk.mp
α : Type u_1
p : α → Bool
b : α
xs : List α
w : p b = true
⊢ (∃ as, (∃ x, xs = as ++ b :: x) ∧ ∀ (a : α), a ∈ as → p a = false) →
    ∃ as, (∃ x, { toList := xs } = as.push b ++ x) ∧ ∀ (a : α), a ∈ as → p a = false

Tactic:
rintro ⟨as, ⟨⟨x, rfl⟩, h⟩⟩

Result:
case mk.mp.intro.intro.intro
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
x : List α
⊢ ∃ as_1, (∃ x_1, { toList := as ++ b :: x } = as_1.push b ++ x_1) ∧ ∀ (a : α), a ∈ as_1 → p a = false

Proof state:
α : Type u_1
p : α → Bool
b : α
w : p b = true
as : List α
h : ∀ (a : α), a ∈ as → p a = false
x : List α
⊢ { toList := as ++ b :: x } = as.toArray.push b ++ x.toArray

Tactic:
simp

Result:
no goals