no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Infinite s
n : ℕ
⊢ ↑(Finset.map (Embedding.subtype fun x => x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) ⊆ s ∧
    Finset.card (Finset.map (Embedding.subtype fun x => x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) = n
simp