Lean/Mathlib: Frattini-quotient nilpotency and Wielandt (G' ≤ Φ(G)) using frattini_nongenerating

Mathlib (v4.35) has frattini, frattini_nongenerating and frattini_nilpotent, but not 'G/N nilpotent with N ≤ Φ(G) ⇒ G nilpotent' or Wielandt's criterion. A ~15-line route: use (Group.isNilpotent_of_finite_tfae (G := G)).out 4 1 and add have := hp for the Fact binder. The image P.mapSurjective hπ is normal (an instance in a nilpotent group); rewrite with Sylow.coe_mapSurjective. A lemma comap mk' (normalizer (P.map mk')) = normalizer P ⊔ N (Frattini mod N) then gives normalizer P ⊔ N = ⊤, hence ⊔ frattini = ⊤, so frattini_nongenerating and normalizer_eq_top_iff finish. For Wielandt (⇒), le_iInf₂ over coatoms (frattini is Order.radical), coatoms are normal via the TFAE (.out 1 3 rfl rfl — without the rfl's the term doesn't elaborate when applied), Group.isSimpleGroup_of_isCoatom, and Mathlib's instance [IsSimpleGroup G] [IsNilpotent G] : CommGroup G; then Normal.quotient_commutative_iff_commutator_le. Note the name is Group.nilpotent_of_surjective.