Theorem: List.mem_cons_iff_of_mem (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
⊢ a ∈ b :: l ↔ a ∈ l
Tactic:
simp only [mem_cons, or_iff_right_iff_imp]
State after:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
⊢ a = b → a ∈ l

State before:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
⊢ a = b → a ∈ l
Tactic:
intro heq
State after:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
heq : a = b
⊢ a ∈ l

State before:
α : Type u
β : Type v
l : List α
a b : α
hb : b ∈ l
heq : a = b
⊢ a ∈ l
Tactic:
exact heq ▸ hb
State after:
no goals