case nil
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ a ∈ [] ∪ l₂ ↔ a ∈ [] ∨ a ∈ l₂

case cons
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : a ∈ tail✝ ∪ l₂ ↔ a ∈ tail✝ ∨ a ∈ l₂
⊢ a ∈ head✝ :: tail✝ ∪ l₂ ↔ a ∈ head✝ :: tail✝ ∨ a ∈ l₂
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ a ∈ l₁ ∪ l₂ ↔ a ∈ l₁ ∨ a ∈ l₂
induction l₁
no goals
case nil
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ a ∈ [] ∪ l₂ ↔ a ∈ [] ∨ a ∈ l₂
simp only [not_mem_nil, false_or_iff, instUnionList, nil_union]
no goals
case cons
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : a ∈ tail✝ ∪ l₂ ↔ a ∈ tail✝ ∨ a ∈ l₂
⊢ a ∈ head✝ :: tail✝ ∪ l₂ ↔ a ∈ head✝ :: tail✝ ∨ a ∈ l₂
simp only [find?, mem_cons, or_assoc, instUnionList, cons_union, mem_union_iff, mem_insert_iff]