α : Type u
β : Type v
γ : Type w
b : α
bs as : List α
h : b ∈ bs
⊢ b ∈ as ++ bs
α : Type u
β : Type v
γ : Type w
b : α
bs as : List α
⊢ b ∈ bs → b ∈ as ++ bs
intro h
no goals
α : Type u
β : Type v
γ : Type w
b : α
bs as : List α
h : b ∈ bs
⊢ b ∈ as ++ bs
induction as with
| nil  => simp [h]
| cons => apply Mem.tail; assumption
no goals
case nil
α : Type u
β : Type v
γ : Type w
b : α
bs : List α
h : b ∈ bs
⊢ b ∈ nil ++ bs
simp [h]
case cons.a
α : Type u
β : Type v
γ : Type w
b : α
bs : List α
h : b ∈ bs
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ tail✝ ++ bs
⊢ Mem b (List.append tail✝ bs)
case cons
α : Type u
β : Type v
γ : Type w
b : α
bs : List α
h : b ∈ bs
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ tail✝ ++ bs
⊢ b ∈ head✝ :: tail✝ ++ bs
apply Mem.tail
no goals
case cons.a
α : Type u
β : Type v
γ : Type w
b : α
bs : List α
h : b ∈ bs
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ tail✝ ++ bs
⊢ Mem b (List.append tail✝ bs)
assumption