-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_eq_some_iff {f : α → Option β} {l : Vector α n} {b : β} :
    l.findSome? f = some b ↔
      ∃ (k₁ k₂ : Nat) (w : n = k₁ + 1 + k₂) (l₁ : Vector α k₁) (a : α) (l₂ : Vector α k₂),
        l = (l₁.push a ++ l₂).cast w.symm ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none

Proof state:
case mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ (∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rintro ⟨k₁, k₂, h, l₁, a, l₂, w, h₁, h₂⟩

Result:
case mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
k₁ k₂ : Nat
h : l.size = k₁ + 1 + k₂
l₁ : Vector α k₁
a : α
l₂ : Vector α k₂
w : l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case mk.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l₁ : Array α
a : α
l₂ : Array α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ k₁ k₂ h l₁_1 a_1 l₂_1,
    l₁.push a ++ l₂ = (Vector.cast ⋯ (l₁_1.push a_1 ++ l₂_1)).toArray ∧
      f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none

Tactic:
exact ⟨l₁.size, l₂.size, by simp, ⟨l₁, rfl⟩, a, ⟨l₂, rfl⟩, by simp, h₁, by simpa using h₂⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
l : Vector α n
b : β
⊢ findSome? f l = some b ↔
    ∃ k₁ k₂ w l₁ a l₂, l = Vector.cast ⋯ (l₁.push a ++ l₂) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ findSome? f { toArray := l, size_toArray := ⋯ } = some b ↔
    ∃ k₁ k₂ w l₁ a l₂,
      { toArray := l, size_toArray := ⋯ } = Vector.cast ⋯ (l₁.push a ++ l₂) ∧
        f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ findSome? f { toArray := l, size_toArray := ⋯ } = some b ↔
    ∃ k₁ k₂ w l₁ a l₂,
      { toArray := l, size_toArray := ⋯ } = Vector.cast ⋯ (l₁.push a ++ l₂) ∧
        f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
simp only [findSome?_mk, mk_eq]

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ Array.findSome? f l = some b ↔
    ∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ (∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩

Result:
case mk.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l₁ : Array α
a : α
l₂ : Array α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ k₁ k₂ h l₁_1 a_1 l₂_1,
    l₁.push a ++ l₂ = (Vector.cast ⋯ (l₁_1.push a_1 ++ l₂_1)).toArray ∧
      f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ Array.findSome? f l = some b ↔
    ∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rw [Array.findSome?_eq_some_iff]

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ (∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) ↔
    ∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
k₁ k₂ : Nat
h : l.size = k₁ + 1 + k₂
l₁ : Vector α k₁
a : α
l₂ : Vector α k₂
w : l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ l = l₁.push a ++ l₂.toArray

Tactic:
simp [w]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l₁ : Array α
a : α
l₂ : Array α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∀ (x : α), x ∈ { toArray := l₁, size_toArray := ⋯ } → f x = none

Tactic:
simpa using h₂

Result:
no goals

Proof state:
case mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
k₁ k₂ : Nat
h : l.size = k₁ + 1 + k₂
l₁ : Vector α k₁
a : α
l₂ : Vector α k₂
w : l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
exact ⟨l₁.toArray, a, l₂.toArray, by simp [w], h₁, by simpa using h₂⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ (∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) ↔
    ∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
constructor

Result:
case mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ (∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

case mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
⊢ (∃ k₁ k₂ h l₁ a l₂, l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l₁ : Array α
a : α
l₂ : Array α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ l₁.push a ++ l₂ =
    (Vector.cast ⋯ ({ toArray := l₁, size_toArray := ⋯ }.push a ++ { toArray := l₂, size_toArray := ⋯ })).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l : Array α
k₁ k₂ : Nat
h : l.size = k₁ + 1 + k₂
l₁ : Vector α k₁
a : α
l₂ : Vector α k₂
w : l = (Vector.cast ⋯ (l₁.push a ++ l₂)).toArray
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∀ (x : α), x ∈ l₁.toArray → f x = none

Tactic:
simpa using h₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
l₁ : Array α
a : α
l₂ : Array α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ (l₁.push a ++ l₂).size = l₁.size + 1 + l₂.size

Tactic:
simp

Result:
no goals