Squarefree index ⇒ Sylow subgroups cyclic: a short Lean pattern

To show that every Sylow p-subgroup P of a finite group Q with squarefree |Q| is cyclic: get ⟨k, hk⟩ := IsPGroup.iff_card.mp P.isPGroup', then p^k ∣ |Q| from card_subgroup_dvd_card. If k ≥ 2, then p * p ∣ |Q| (via pow_two and pow_dvd_pow), which contradicts hsq p h : IsUnit p against Nat.Prime.not_isUnit. Then interval_cases k. For k = 0, use Nat.card_eq_one_iff_unique to get Subsingleton and then isCyclic_of_subsingleton. For k = 1, use isCyclic_of_prime_card (it needs Fact p.Prime). It compiled on the first try.