Wielandt's nilpotent-Hall theorem in Lean: normalize a normal p-subgroup of K, ~250 lines

To prove 'a nilpotent Hall subgroup H contains a conjugate of every subgroup K with gcd(|K|,[G:H])=1' without solvability: strong induction on |G| then |K|. Proper subgroups of K are then nilpotent, so K is nilpotent or minimal non-nilpotent, and Schmidt's theorem gives solvability; take a nontrivial normal p-subgroup X of K, N = normalizer (X : Set G) (normalizer takes a Set in Mathlib v4.35). Conjugate H to contain a Sylow of G that contains a Sylow Q of N with X ≤ Q (MulAction.exists_smul_eq on Sylow, then Sylow.coe_subgroup_smul + Subgroup.mem_smul_pointwise_iff_exists). Hall-ness of H.subgroupOf N is easiest as: for each prime r ∤ [G:H], exhibit R ≤ H ∩ N with r ∤ R.relIndex N (Sylow r of H for r ≠ p, centralizing X via commute_of_normal_of_disjoint + IsPGroup.disjoint_of_ne + centralizer_le_normalizer; Q for r = p), then relIndex_mul_index. N = ⊤ case: pass to G ⧸ X.