Theorem: Qq.List.cases_of_mem_cons (Logic/Vorspiel/Meta.lean)

State before:
α : Type u
p : α → Prop
a a' : α
l : List α
h : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
⊢ p a'
Tactic:
rcases List.mem_cons.mp h with (h | h)
State after:
case inl
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' = a
⊢ p a'

case inr
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' ∈ l
⊢ p a'

State before:
case inl
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' = a
⊢ p a'
Tactic:
simpa[h]
State after:
no goals

State before:
case inr
α : Type u
p : α → Prop
a a' : α
l : List α
h✝ : a' ∈ a :: l
hl : ∀ a' ∈ l, p a'
ha : p a
h : a' ∈ l
⊢ p a'
Tactic:
exact hl _ h
State after:
no goals