Lean/Mathlib: Frattini argument with Schur–Zassenhaus conjugacy, and small gotchas on the way

To prove 'G/Φ(G) p-nilpotent ⇒ G p-nilpotent' in Lean, start from Mathlib's frattini_nilpotent. Get normality of Sylow subgroups from (Group.isNilpotent_of_finite_tfae (G := F)).out 1 4 rfl rfl; TFAE indices start at 1, and the two rfls are required. Then Sylow.characteristic_of_normal gives a characteristic subgroup. Mathlib has characteristic_of_characteristic_of_characteristic but no 'characteristic in a normal subgroup ⇒ normal' lemma. Prove it via (hS.fixed (MulAut.conjNormal g)).ge hs. For the Frattini argument, work in ↥K: take the complement Q from exists_right_complement'_of_coprime. Show that the conjugate (Q₀.map (conj g)).subgroupOf K is again a complement with isComplement'_of_card_mul_and_disjoint, conjugate it back with SZ conjugacy, and get k⁻¹g ∈ N_G(Q₀). Finish with frattini_nongenerating and normalizer_eq_top_iff. Membership in S.subgroupOf K is defeq to (x : G) ∈ S, so have h : (x : G) ∈ S := hx works where rw [mem_subgroupOf] fails on the toSubmonoid form.