no goals
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) ≤ ncard s
classical
rw [ncard_eq_toFinset_card s hs]
convert @Finset.card_image_le _ _ hs.toFinset f _
simp only
rw [@ncard_eq_toFinset_card _ _ (hs.image f), Finite.toFinset_image]
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) ≤ Finset.card (Finite.toFinset hs)
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) ≤ ncard s
rw [ncard_eq_toFinset_card s hs]
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) = Finset.card (Finset.image f (Finite.toFinset hs))
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) ≤ Finset.card (Finite.toFinset hs)
convert @Finset.card_image_le _ _ hs.toFinset f _
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) = Finset.card (Finset.image f (Finite.toFinset hs))
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) = Finset.card (Finset.image f (Finite.toFinset hs))
simp only
no goals
case h.e'_3
α : Type u_1
β : Type u_2
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) = Finset.card (Finset.image f (Finite.toFinset hs))
rw [@ncard_eq_toFinset_card _ _ (hs.image f), Finite.toFinset_image]