α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ a ∈ l₁ ∧ decide (a ∈ l₂) = true ↔ a ∈ l₁ ∧ a ∈ l₂
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ a ∈ l₁ ∩ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
erw [mem_filter]
no goals
α : Type u_1
l l₁ l₂ : List α
p : α → Prop
a : α
inst✝ : DecidableEq α
⊢ a ∈ l₁ ∧ decide (a ∈ l₂) = true ↔ a ∈ l₁ ∧ a ∈ l₂
simp