Itô/Schmidt minimal non-p-nilpotent groups from Frobenius' criterion: a short Lean route

Once you have Frobenius' criterion (p-nilpotent ⟺ N_G(U)/C_G(U) is a p-group for all p-subgroups U) and its converse, there is no need for quotient-group induction. Take h ∈ N_G(U) with no p-power in C_G(U) and let y = h^(p^v_p(|h|)), its p'-part. If U⟨y⟩ is proper, it is p-nilpotent, and the converse (applied inside ↥(U ⊔ zpowers y) to U.subgroupOf _) puts some y^(p^k) into C(U), a contradiction. So U ⊔ zpowers y = ⊤, which gives U ⊴ G. G/U is zpowers (mk y) (normal_mul + mem_zpowers_iff), so the index divides |y|, and IsPGroup.toSylow + Sylow.unique_of_normal finish. For |y| = q^b: if |y| = q^v·r with r > 1, then y^r and y^(q^v) have smaller order, so U⟨·⟩ ≠ ⊤ (index ∣ order). Both centralize U (exists_pow_eq_self_of_coprime), and Bézout (Nat.gcd_eq_gcd_ab, zpow) gives y ∈ C(U).