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

Proof state:
case cons.h_1.mpr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ (∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) → b' = b

Tactic:
rintro ⟨(⟨⟩ | ⟨p', l₁⟩), a, ⟨l₂, h₁⟩, h₂, h₃⟩

Result:
case cons.h_1.mpr.intro.nil.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
a : α
l₂ : List α
h₁ : p :: l = [] ++ a :: l₂
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ [] → f x = none
⊢ b' = b

case cons.h_1.mpr.intro.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
p' : α
l₁ : List α
a : α
l₂ : List α
h₁ : p :: l = p' :: l₁ ++ a :: l₂
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ p' :: l₁ → f x = none
⊢ b' = b

Proof state:
case cons.h_1.mpr.intro.cons.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
x✝ : Option β
b' : β
h : f p = some b'
l₁ : List α
a : α
l₂ : List α
h₂ : f a = some b
ih :
  findSome? f (l₁ ++ a :: l₂) = some b ↔
    ∃ l₁_1 a_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none
h₃ : p ∈ p :: l₁ → f p = none
⊢ b' = b

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.h_1.mpr.intro.nil.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
a : α
l₂ : List α
h₁ : p :: l = [] ++ a :: l₂
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ [] → f x = none
⊢ b' = b

Tactic:
simp only [nil_append, cons.injEq] at h₁

Result:
case cons.h_1.mpr.intro.nil.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
a : α
l₂ : List α
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ [] → f x = none
h₁ : p = a ∧ l = l₂
⊢ b' = b

Proof state:
case cons.h_1.mpr.intro.nil.intro.intro.intro.intro.x
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
a : α
l₂ : List α
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ [] → f x = none
h₁ : p = a ∧ l = l₂
⊢ some b' = some b

Tactic:
simp [← h, ← h₂, h₁.1]

Result:
no goals

Proof state:
case cons.h_2.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
b' : Option β
h : f p = none
l₁ : List α
a : α
l₂ : List α
ih :
  findSome? f (l₁ ++ a :: l₂) = some b ↔
    ∃ l₁_1 a_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁_1 a_1 l₂_1, p :: (l₁ ++ a :: l₂) = l₁_1 ++ a_1 :: l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none

Tactic:
refine ⟨p :: l₁, a, l₂, rfl, h₁, ?_⟩

Result:
case cons.h_2.mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
b' : Option β
h : f p = none
l₁ : List α
a : α
l₂ : List α
ih :
  findSome? f (l₁ ++ a :: l₂) = some b ↔
    ∃ l₁_1 a_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none
h₁ : f a = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∀ (x : α), x ∈ p :: l₁ → f x = none

Proof state:
case cons.h_2.mp.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
b' : Option β
h : f p = none
l₁ : List α
a✝ : α
l₂ : List α
ih :
  findSome? f (l₁ ++ a✝ :: l₂) = some b ↔
    ∃ l₁_1 a l₂_1, l₁ ++ a✝ :: l₂ = l₁_1 ++ a :: l₂_1 ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none
h₁ : f a✝ = some b
h₂ : ∀ (x : α), x ∈ l₁ → f x = none
a : α
w : a ∈ l₁
⊢ f a = none

Tactic:
exact h₂ _ w

Result:
no goals

Proof state:
case cons.h_2.mpr.intro.intro.intro.intro.intro.cons.intro.refl
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
b' : Option β
h : f p = none
a : α
l₂ : List α
h₂ : f a = some b
l₁ : List α
h₃ : ∀ (x : α), x ∈ p :: l₁ → f x = none
ih :
  findSome? f (l₁ ++ a :: l₂) = some b ↔
    ∃ l₁_1 a_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none
⊢ ∃ l₁_1 a_1 l₂_1, l₁ ++ a :: l₂ = l₁_1 ++ a_1 :: l₂_1 ∧ f a_1 = some b ∧ ∀ (x : α), x ∈ l₁_1 → f x = none

Tactic:
exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩

Result:
no goals

Proof state:
case cons.h_1.mpr.intro.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
p' : α
l₁ : List α
a : α
l₂ : List α
h₁ : p :: l = p' :: l₁ ++ a :: l₂
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ p' :: l₁ → f x = none
⊢ b' = b

Tactic:
simp only [cons_append, cons.injEq] at h₁

Result:
case cons.h_1.mpr.intro.cons.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
p' : α
l₁ : List α
a : α
l₂ : List α
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ p' :: l₁ → f x = none
h₁ : p = p' ∧ l = l₁ ++ a :: l₂
⊢ b' = b

Proof state:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ some b' = some b ↔ ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
simp only [Option.some.injEq, exists_and_right]

Result:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
x✝ : Option β
b' : β
h : f p = some b'
⊢ b' = b ↔ ∃ l₁ a, (∃ x, p :: l = l₁ ++ a :: x) ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case cons.h_2.mpr.intro.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
b' : Option β
h : f p = none
a : α
l₂ : List α
h₂ : f a = some b
a' : α
l₁ : List α
h₁ : p :: l = a' :: l₁ ++ a :: l₂
h₃ : ∀ (x : α), x ∈ a' :: l₁ → f x = none
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
simp only [cons_append, cons.injEq] at h₁

Result:
case cons.h_2.mpr.intro.intro.intro.intro.intro.cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
p : α
l : List α
ih : findSome? f l = some b ↔ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none
b' : Option β
h : f p = none
a : α
l₂ : List α
h₂ : f a = some b
a' : α
l₁ : List α
h₃ : ∀ (x : α), x ∈ a' :: l₁ → f x = none
h₁ : p = a' ∧ l = l₁ ++ a :: l₂
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none