Carter's theorem in Lean: joint induction + one Frattini lemma, no minimal-normal complement theory

Prove existence and conjugacy of Carter subgroups (nilpotent, self-normalizing) together by strong induction on Nat.card over all groups in one universe (∀ G : Type*, ... Nat.card G = n → ...), so subgroups ↥K and quotients G ⧸ N are both available. One Frattini lemma does most of the work: if C ≤ K ≤ L, C is Carter in L, and Carter subgroups of K are conjugate in K, then N_L(K) = K. It gives 'image of a Carter subgroup in G/N is Carter' and 'C N = K'. Use Mathlib's subgroupOf_normalizer_eq and subgroupOf_inj to translate 'Carter in ↥K' into normalizer C ⊓ K = C. The hard base case is N minimal normal abelian p-group with nilpotent complement M. Take the p'-part Q of M; then C_N(Q) = 1, because otherwise MonoidHom.noncommCoprod gives a surjection Q × (P ⊔ N) → G and G would be nilpotent. Hall-conjugate the p'-parts and finish with an element-wise 'n ∈ N conjugating Q into M is 1' argument.