-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_eq_some_iff_append {xs : Vector α n} :
    xs.find? p = some b ↔
      p b ∧ ∃ (k₁ k₂ : Nat) (w : n = k₁ + 1 + k₂) (as : Vector α k₁) (bs : Vector α k₂),
        xs = (as.push b ++ bs).cast w.symm ∧ ∀ a ∈ as, !p a

Proof state:
case mk.mp
α : Type
p : α → Bool
b : α
xs : Array α
⊢ (p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true) →
    p b = true ∧ ∃ k₁ k₂ h as bs, xs = as.push b ++ bs.toArray ∧ ∀ (a : α), a ∈ as → (!p a) = true

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

Result:
case mk.mp.intro.intro.intro.intro
α : Type
p : α → Bool
b : α
h : p b = true
as bs : Array α
w : ∀ (a : α), a ∈ as → (!p a) = true
⊢ p b = true ∧ ∃ k₁ k₂ h as_1 bs_1, as.push b ++ bs = as_1.push b ++ bs_1.toArray ∧ ∀ (a : α), a ∈ as_1 → (!p a) = true

Proof state:
α : Type
p : α → Bool
b : α
xs : Array α
h : p b = true
k₁ k₂ : Nat
w : xs.size = k₁ + 1 + k₂
as : Vector α k₁
bs : Vector α k₂
h' : xs = as.push b ++ bs.toArray
w' : ∀ (a : α), a ∈ as → (!p a) = true
⊢ xs = as.push b ++ bs.toArray

Tactic:
simp [h']

Result:
no goals

Proof state:
case mk
α : Type
p : α → Bool
b : α
xs : Array α
⊢ (p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true) ↔
    p b = true ∧ ∃ k₁ k₂ h as bs, xs = as.push b ++ bs.toArray ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
constructor

Result:
case mk.mp
α : Type
p : α → Bool
b : α
xs : Array α
⊢ (p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true) →
    p b = true ∧ ∃ k₁ k₂ h as bs, xs = as.push b ++ bs.toArray ∧ ∀ (a : α), a ∈ as → (!p a) = true

case mk.mpr
α : Type
p : α → Bool
b : α
xs : Array α
⊢ (p b = true ∧ ∃ k₁ k₂ h as bs, xs = as.push b ++ bs.toArray ∧ ∀ (a : α), a ∈ as → (!p a) = true) →
    p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Proof state:
α : Type
n : Nat
p : α → Bool
b : α
xs : Vector α n
⊢ find? p xs = some b ↔
    p b = true ∧ ∃ k₁ k₂ w as bs, xs = Vector.cast ⋯ (as.push b ++ bs) ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type
p : α → Bool
b : α
xs : Array α
⊢ find? p { toArray := xs, size_toArray := ⋯ } = some b ↔
    p b = true ∧
      ∃ k₁ k₂ w as bs,
        { toArray := xs, size_toArray := ⋯ } = Vector.cast ⋯ (as.push b ++ bs) ∧ ∀ (a : α), a ∈ as → (!p a) = true

Proof state:
α : Type
p : α → Bool
b : α
h : p b = true
as bs : Array α
w : ∀ (a : α), a ∈ as → (!p a) = true
⊢ as.push b ++ bs = { toArray := as, size_toArray := ⋯ }.push b ++ { toArray := bs, size_toArray := ⋯ }.toArray

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type
p : α → Bool
b : α
xs : Array α
⊢ find? p { toArray := xs, size_toArray := ⋯ } = some b ↔
    p b = true ∧
      ∃ k₁ k₂ w as bs,
        { toArray := xs, size_toArray := ⋯ } = Vector.cast ⋯ (as.push b ++ bs) ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
simp only [find?_mk, Array.find?_eq_some_iff_append,
  mk_eq, toArray_cast, toArray_append, toArray_push]

Result:
case mk
α : Type
p : α → Bool
b : α
xs : Array α
⊢ (p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true) ↔
    p b = true ∧ ∃ k₁ k₂ h as bs, xs = as.push b ++ bs.toArray ∧ ∀ (a : α), a ∈ as → (!p a) = true

Proof state:
case mk.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type
p : α → Bool
b : α
xs : Array α
h : p b = true
k₁ k₂ : Nat
w : xs.size = k₁ + 1 + k₂
as : Vector α k₁
bs : Vector α k₂
h' : xs = as.push b ++ bs.toArray
w' : ∀ (a : α), a ∈ as → (!p a) = true
⊢ p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
exact ⟨h, as.toArray, bs.toArray, by simp [h'], by simpa using w'⟩

Result:
no goals

Proof state:
α : Type
p : α → Bool
b : α
h : p b = true
as bs : Array α
w : ∀ (a : α), a ∈ as → (!p a) = true
⊢ (as.push b ++ bs).size = as.size + 1 + bs.size

Tactic:
simp

Result:
no goals

Proof state:
α : Type
p : α → Bool
b : α
h : p b = true
as bs : Array α
w : ∀ (a : α), a ∈ as → (!p a) = true
⊢ ∀ (a : α), a ∈ { toArray := as, size_toArray := ⋯ } → (!p a) = true

Tactic:
simpa using w

Result:
no goals

Proof state:
case mk.mpr
α : Type
p : α → Bool
b : α
xs : Array α
⊢ (p b = true ∧ ∃ k₁ k₂ h as bs, xs = as.push b ++ bs.toArray ∧ ∀ (a : α), a ∈ as → (!p a) = true) →
    p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Tactic:
rintro ⟨h, k₁, k₂, w, as, bs, h', w'⟩

Result:
case mk.mpr.intro.intro.intro.intro.intro.intro.intro
α : Type
p : α → Bool
b : α
xs : Array α
h : p b = true
k₁ k₂ : Nat
w : xs.size = k₁ + 1 + k₂
as : Vector α k₁
bs : Vector α k₂
h' : xs = as.push b ++ bs.toArray
w' : ∀ (a : α), a ∈ as → (!p a) = true
⊢ p b = true ∧ ∃ as bs, xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true

Proof state:
α : Type
p : α → Bool
b : α
xs : Array α
h : p b = true
k₁ k₂ : Nat
w : xs.size = k₁ + 1 + k₂
as : Vector α k₁
bs : Vector α k₂
h' : xs = as.push b ++ bs.toArray
w' : ∀ (a : α), a ∈ as → (!p a) = true
⊢ ∀ (a : α), a ∈ as.toArray → (!p a) = true

Tactic:
simpa using w'

Result:
no goals

Proof state:
case mk.mp.intro.intro.intro.intro
α : Type
p : α → Bool
b : α
h : p b = true
as bs : Array α
w : ∀ (a : α), a ∈ as → (!p a) = true
⊢ p b = true ∧ ∃ k₁ k₂ h as_1 bs_1, as.push b ++ bs = as_1.push b ++ bs_1.toArray ∧ ∀ (a : α), a ∈ as_1 → (!p a) = true

Tactic:
exact ⟨h, as.size, bs.size, by simp, ⟨as, rfl⟩, ⟨bs, rfl⟩, by simp, by simpa using w⟩

Result:
no goals