-- 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.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

Tactic:
obtain ⟨rfl, rfl⟩ := h₁

Result:
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
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
⊢ b' = b

Proof state:
case cons.h_2.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
b' : Option β
h : f p = none
⊢ (∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

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

Result:
case cons.h_2.mpr.intro.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
b' : Option β
h : f p = none
l₁ : List α
a : α
l₂ : List α
h₁ : p :: l = l₁ ++ a :: l₂
h₂ : f a = some b
h₃ : ∀ (x : α), x ∈ l₁ → f x = none
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case cons.h_2
α : 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
⊢ (∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) ↔
    ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
constructor

Result:
case cons.h_2.mp
α : 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
⊢ (∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

case cons.h_2.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
b' : Option β
h : f p = none
⊢ (∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

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

Tactic:
simp

Result:
no goals

Proof state:
case cons.h_2.mp
α : 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
⊢ (∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none) →
    ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
rintro ⟨l₁, a, l₂, rfl, h₁, 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
⊢ ∃ 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

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

Tactic:
simp

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
⊢ ∀ (x : α), x ∈ p :: l₁ → f x = none

Tactic:
intro a w

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 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 ∈ p :: l₁
⊢ f a = none

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
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
⊢ b' = b

Tactic:
specialize h₃ p

Result:
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

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 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 ∈ p :: l₁
⊢ f a = none

Tactic:
simp at w

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 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 = p ∨ a ∈ l₁
⊢ f a = none