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

case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ p a = true
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
H : find? p (b :: l) = some a
⊢ p a = true
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
⊢ p a = true
exact H ▸ h
no goals
case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ p a = true
exact find?_some H