α : Type u_1
β : Type ?u.20009
γ : Type ?u.20012
s : Finset α
x : α
⊢ ¬x ∈ ∅
α : Type u_1
β : Type ?u.20009
γ : Type ?u.20012
s✝ s : Finset α
⊢ s = ∅ → ∀ (x : α), ¬x ∈ s
rintro rfl x
no goals
α : Type u_1
β : Type ?u.20009
γ : Type ?u.20012
s : Finset α
x : α
⊢ ¬x ∈ ∅
apply not_mem_empty