α : Type u_1
β : Sort ?u.19844
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ as ∧ b ≠ a
⊢ b ∈ as
α : Type u_1
β : Sort ?u.19844
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ remove a as
⊢ b ∈ as
rw [mem_remove_iff] at h
no goals
α : Type u_1
β : Sort ?u.19844
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
as : List α
h : b ∈ as ∧ b ≠ a
⊢ b ∈ as
exact h.1