case pos
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : p b = true
H : b = a
⊢ a ∈ b :: l

case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ a ∈ b :: l
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
H : find? p (b :: l) = some a
⊢ a ∈ b :: l
by_cases h : p b <;> simp [find?, h] at H
no goals
case pos
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : p b = true
H : b = a
⊢ a ∈ b :: l
exact H ▸ .head _
no goals
case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ a ∈ b :: l
exact .tail _ (mem_of_find?_eq_some H)