α : Type u_1
β : Type ?u.13061
s t : Set α
a b x y : α
f : α → β
h : a ≠ b
⊢ ¬a ∈ {b}
α : Type u_1
β : Type ?u.13061
s t : Set α
a b x y : α
f : α → β
h : a ≠ b
⊢ ncard {a, b} = 2
rw [ncard_insert_of_not_mem, ncard_singleton]
no goals
α : Type u_1
β : Type ?u.13061
s t : Set α
a b x y : α
f : α → β
h : a ≠ b
⊢ ¬a ∈ {b}
simpa