case nil
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
a : α
H✝ : find? p l = some a
H : find? p [] = some a
⊢ a ∈ []

case cons
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p (b :: l) = some a
⊢ a ∈ b :: l
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
a : α
H : find? p l = some a
⊢ a ∈ l
induction' l with b l IH
case pos
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p (b :: l) = some a
h : p b = true
⊢ a ∈ b :: l

case neg
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p (b :: l) = some a
h : ¬p b = true
⊢ a ∈ b :: l
case cons
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p (b :: l) = some a
⊢ a ∈ b :: l
by_cases h : p b
no goals
case nil
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l : List α
a : α
H✝ : find? p l = some a
H : find? p [] = some a
⊢ a ∈ []
contradiction
case pos
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : some b = some a
h : p b = true
⊢ a ∈ b :: l
case pos
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p (b :: l) = some a
h : p b = true
⊢ a ∈ b :: l
rw [find?_cons_of_pos _ h] at H
case pos.refl
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H : find? p l✝ = some a
l : List α
IH : find? p l = some a → a ∈ l
h : p a = true
⊢ a ∈ a :: l
case pos
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : some b = some a
h : p b = true
⊢ a ∈ b :: l
cases H
no goals
case pos.refl
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H : find? p l✝ = some a
l : List α
IH : find? p l = some a → a ∈ l
h : p a = true
⊢ a ∈ a :: l
apply mem_cons_self
case neg
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p l = some a
h : ¬p b = true
⊢ a ∈ b :: l
case neg
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p (b :: l) = some a
h : ¬p b = true
⊢ a ∈ b :: l
rw [find?_cons_of_neg _ h] at H
no goals
case neg
ι : Type ?u.339715
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
l✝ : List α
a : α
H✝ : find? p l✝ = some a
b : α
l : List α
IH : find? p l = some a → a ∈ l
H : find? p l = some a
h : ¬p b = true
⊢ a ∈ b :: l
exact mem_cons_of_mem _ (IH H)