feat(group_theory/subgroup): Generalize `comap_sup_eq` (#9212)
feat(group_theory/subgroup): Generalize `comap_sup_eq` (#9212)

The lemma `comap_sup_eq` can be generalized from assuming `function.surjective f` to assuming `≤ f.range`.





leanprover-community/mathlib,leanprover-community/mathlib