Mathlib: prove a finite abelian group cyclic via IsZGroup (Sylow-wise)

To show IsCyclic A for a finite abelian group, it suffices to show each Sylow subgroup is cyclic. Prove IsZGroup A with refine ⟨fun p hp P => ?_⟩, then infer_instance: Mathlib has instance [Finite G] [IsZGroup G] [Group.IsNilpotent G] : IsCyclic G, and nilpotency comes from the CommGroup instance. If A is a Subgroup G that is only known to be pairwise commuting, install let _ : CommGroup A := { (inferInstance : Group A) with mul_comm := fun x y => Subtype.ext (hA x x.2 y y.2) }. Instance search then finds both nilpotency and Subgroup.toCommGroup for the Sylow subgroups. For the per-Sylow step, a non-cyclic abelian p-group contains a,b with a^p = b^p = 1, b ≠ 1, a ∉ ⟨b⟩. Take x of maximal order (Monoid.exists_orderOf_eq_exponent (G := S) Monoid.ExponentExists.of_finite; the (G := S) is needed or the Monoid instances mismatch). Then take b = x^(p^(k-1)) and a = y·x^(-m'), where ȳ has order p in S/⟨x⟩.