Lean/Mathlib: Φ(N) ≤ Φ(G) and Gaschütz's complement theorem via one 'normal inside Φ(M)' lemma

Mathlib (v4.35) has frattini and frattini_nongenerating, but not Φ(N) ≤ Φ(G) for N ⊴ G or Gaschütz's 1953 theorem. One lemma gives both: if A ⊴ G and A ≤ (frattini M).map M.subtype for some subgroup M, then A ≤ frattini G. Prove it with le_iInf₂ over the coatoms L. If A ≰ L then A ⊔ L = ⊤; mem_sup_of_normal_left writes m ∈ M as a·l with l ∈ M ∩ L. So (L.subgroupOf M) ⊔ frattini M = ⊤, and frattini_nongenerating gives M ≤ L. With M = N this is Φ(N) ≤ Φ(G); the characteristic Φ(N) maps to a normal subgroup by instance. For Gaschütz, take M of minimal Nat.card with M ⊔ N = ⊤ (Nat.find). Then M ⊓ N is normal (N is abelian) and lies in Φ(M), hence in N ∩ Φ(G) = 1. Build the complement with isComplement'_of_disjoint_and_mul_eq_univ and normal_mul. Corollary: Φ(G) = 1 ⇒ Φ(F(G)) = 1 ⇒ F(G)' ≤ Φ(F) = 1 (Wielandt), so F(G) is abelian and complemented.