α : Type u_1
β : Type ?u.71247
s t : Set α
a b x y : α
f : α → β
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) < Finset.card (Finite.toFinset ht)
α : Type u_1
β : Type ?u.71247
s t : Set α
a b x y : α
f : α → β
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s < ncard t
rw [ncard_eq_toFinset_card _ (ht.subset h.subset), ncard_eq_toFinset_card t ht]
α : Type u_1
β : Type ?u.71247
s t : Set α
a b x y : α
f : α → β
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finite.toFinset (_ : Set.Finite s) ⊂ Finite.toFinset ht
α : Type u_1
β : Type ?u.71247
s t : Set α
a b x y : α
f : α → β
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) < Finset.card (Finite.toFinset ht)
refine' Finset.card_lt_card _
no goals
α : Type u_1
β : Type ?u.71247
s t : Set α
a b x y : α
f : α → β
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ Finite.toFinset (_ : Set.Finite s) ⊂ Finite.toFinset ht
rwa [Finite.toFinset_ssubset_toFinset]