refactor(group_theory/sylow): extract a lemma from Sylow proof (#8459)
refactor(group_theory/sylow): extract a lemma from Sylow proof (#8459)



Co-authored-by: Chris Hughes <b6f42777c6934d5d432f4754eab7d808cdca21a6@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib