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

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
l₁ : Array α
a : α
l₂ : Array α
h₀ : { toList := toList✝ } = l₁.push a ++ l₂
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ toList✝ = l₁.toList ++ a :: l₂.toList

Tactic:
simpa using congrArg toList h₀

Result:
no goals

Proof state:
case mk.mp
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ (∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ 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₁ : List α
a : α
l₂ : List α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁_1 a_1 l₂_1,
    { toList := l₁ ++ a :: l₂ } = l₁_1.push a_1 ++ l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none

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

Tactic:
simp_all

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ (∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) ↔
    ∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ 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 : β
toList✝ : List α
⊢ (∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

case mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ (∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
l₁ : Array α
a : α
l₂ : Array α
h₀ : { toList := toList✝ } = l₁.push a ++ l₂
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∀ (x : α), x ∈ l₁.toList → f x = none

Tactic:
simpa

Result:
no goals

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

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ findSome? f { toList := toList✝ } = some b ↔
    ∃ l₁ a l₂, { toList := toList✝ } = 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₁ : List α
a : α
l₂ : List α
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁_1 a_1 l₂_1,
    { toList := l₁ ++ a :: l₂ } = l₁_1.push a_1 ++ l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none

Tactic:
exact ⟨l₁.toArray, a, l₂.toArray, by simp_all⟩

Result:
no goals

Proof state:
case mk.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ (∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

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

Result:
case mk.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
l₁ : Array α
a : α
l₂ : Array α
h₀ : { toList := toList✝ } = l₁.push a ++ l₂
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case mk.mpr.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
l₁ : Array α
a : α
l₂ : Array α
h₀ : { toList := toList✝ } = l₁.push a ++ l₂
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
exact ⟨l₁.toList, a, l₂.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ findSome? f { toList := toList✝ } = some b ↔
    ∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
simp only [List.findSome?_toArray, List.findSome?_eq_some_iff]

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
b : β
toList✝ : List α
⊢ (∃ l₁ a l₂, toList✝ = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) ↔
    ∃ l₁ a l₂, { toList := toList✝ } = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none