α : Type u_1
β : Type ?u.127640
s t : Set α
a b x y : α
f : α → β
h : ncard s < ncard t
hs : autoParam (Set.Finite s) _auto✝
⊢ ¬t ⊆ s
α : Type u_1
β : Type ?u.127640
s t : Set α
a b x y : α
f : α → β
h : ncard s < ncard t
hs : autoParam (Set.Finite s) _auto✝
⊢ Set.Nonempty (t \ s)
rw [Set.nonempty_iff_ne_empty, Ne.def, diff_eq_empty]
no goals
α : Type u_1
β : Type ?u.127640
s t : Set α
a b x y : α
f : α → β
h : ncard s < ncard t
hs : autoParam (Set.Finite s) _auto✝
⊢ ¬t ⊆ s
exact fun h' ↦ h.not_le (ncard_le_of_subset h' hs)