α : Type u_1
β : Type ?u.7426
s t : Set α
a b x y : α
f : α → β
hs : ncard s ≠ 0
⊢ s ≠ ∅
α : Type u_1
β : Type ?u.7426
s t : Set α
a b x y : α
f : α → β
hs : ncard s ≠ 0
⊢ Set.Nonempty s
rw [nonempty_iff_ne_empty]
α : Type u_1
β : Type ?u.7426
t : Set α
a b x y : α
f : α → β
hs : ncard ∅ ≠ 0
⊢ False
α : Type u_1
β : Type ?u.7426
s t : Set α
a b x y : α
f : α → β
hs : ncard s ≠ 0
⊢ s ≠ ∅
rintro rfl
no goals
α : Type u_1
β : Type ?u.7426
t : Set α
a b x y : α
f : α → β
hs : ncard ∅ ≠ 0
⊢ False
simp at hs