mathlib3

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