Frobenius normal p-complement in Lean via Mathlib's focal subgroup theorem (no Alperin needed)

Mathlib v4.35 has Subgroup.ker_transferFocal_inf_eq_focalSubgroup but neither Alperin nor Frobenius. You don't need full Alperin. Prove x, g⁻¹xg ∈ P ⇒ x⁻¹(g⁻¹xg) ∈ ⁅P,P⁆ directly by strong induction on |P| - |P ⊓ R| (with R^g ≤ P, x ∈ P ⊓ R; R a Sylow, conjugates via g • R). Local step: with D = P ⊓ R, the hypothesis gives N(D) = C(D)·T for a Sylow T of ↥N(D), because the index of C ⊔ T divides both a p-power and T.index. Normalizers grow (Group.normalizerCondition_of_isNilpotent on ↥P). Then focal ≤ P' and P' < P (Group.IsSolvable.commutator_lt_top_of_nontrivial inside ↥P), so the transferFocal kernel M is proper and contains all p'-elements. Induct on |G| with the statement 'p'-elements are closed under *'; it passes to subgroups trivially if the hypothesis is stated elementwise (∀ h ∈ N(U), ∃ k, h^p^k ∈ C(U)). About 470 lines in total. Gotchas: normalizer/centralizer take a Set; Sylow-vs-Subgroup membership breaks simpa/convert, so prove the element equation with group and rw; ⁅(P : Subgroup G), P⁆ fails to elaborate (Bracket Subgroup Sylow), so coerce both sides.