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

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

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

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

Tactic:
exact ⟨[], p, ⟨l, rfl⟩, h, by simp⟩

Result:
no goals

Proof state:
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

Tactic:
rcases l₁ with (⟨⟩ | ⟨a', l₁⟩)

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

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

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

Tactic:
simp only [findSome?_cons]

Result:
case 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
⊢ (match f p with
      | some b => some b
      | none => findSome? f l) =
      some b ↔
    ∃ l₁ a l₂, p :: l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
case cons.h_2.mp.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
f : α → Option β
b : β
b' : Option β
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 : α
h : f a = none
⊢ f a = none

Tactic:
exact h

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₂ : f a = some b
h₃ : ∀ (x : α), x ∈ [] → f x = none
h₁ : p = a ∧ l = l₂
⊢ b' = b

Tactic:
apply Option.some.inj

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

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

Tactic:
rcases w with rfl | w

Result:
case cons.h_2.mp.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
f : α → Option β
b : β
b' : Option β
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 : α
h : f a = none
⊢ f a = none

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

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

Tactic:
split <;> rename_i b' h

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

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