mathlib

2b589cad - 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`.