mathlib3

a9123922 - feat(data/fintype/basic): add `card_subtype_mono` (#14645)

feat(data/fintype/basic): add `card_subtype_mono` (#14645) This lemma naturally forms a counterpart to existing lemmas. I've also renamed a lemma it uses that didn't seem to fit the existing naming pattern.