Finite subsets of a set as finsets of the subtype

A finite set s ⊆ S is the image under Subtype.val of a finset of the subtype ↥S with the same number of elements (Set.Finite.exists_finset_subtype_image_val_eq). This is the reading of a finite set of elements of a subgroup, a submodule or any other set-like structure as a Finset of that structure, which is the form the generation and rank statements over a Finset of a subgroup take.

theorem Set.Finite.exists_finset_subtype_image_val_eq {α : Type u_1} {S s : Set α} (hs : s.Finite) (hsub : s ⊆ S) : ∃ (t : Finset ↑S), t.card = Nat.card ↑s ∧ Subtype.val '' ↑t = s

A finite set s ⊆ S is the image of a finset of the subtype ↥S with Nat.card s elements.