feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363)
feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363)

This PR adds some more API lemmas for `group.rank`.





leanprover-community/mathlib,leanprover-community/mathlib