[GOAL]
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
h : x ∈ a :: l
px : p x
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
simp only [find?, mem_cons] at h 
[GOAL]
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
px : p x
h : x = a ∨ x ∈ l
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
cases' h with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
px : p x
h : x = a
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
cases h
[GOAL]
case inl.refl
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
px : p a
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
exact Or.inl px
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
px : p x
h : x ∈ l
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
exact Or.inr ⟨x, h, px⟩
