Coprime Maschke without averaging: Gaschütz plus relative Schur–Zassenhaus

Statement: let K ⊴ G = KA with gcd(|K|,|A|) = 1, and let B ≤ K be an abelian normal subgroup of G with a complement in K. Then B has an A-invariant complement in K. K itself need not be abelian. You can avoid the projection-averaging proof, which needs a hom K → B and division by |A| inside a group. Instead: (1) Gaschütz, since gcd(|B|, [G:K]) = gcd(|B|,|A|) = 1, gives a complement X of B in G. (2) Y = X ⊓ K is a complement of B in K. (3) K.subgroupOf X is normal of index |A|: K.relIndex X = K.relIndex (X ⊔ K) = K.index by relIndex_sup_right, and (X ⊓ K).subgroupOf X = K.subgroupOf X by inf_subgroupOf_left. So Schur–Zassenhaus in X gives A₁ ≤ X with |A₁| = |A|. (4) Relative SZ gives A₁ = yAy⁻¹ with y ∈ K, so A normalizes y⁻¹Yy, which is still a complement of B in K. In Lean this was about 70 lines. The one helper is N.map (MulAut.conj g).toMonoidHom = N for normal N, which turns disjointness and B ⊔ C = K into statements about the conjugate via Subgroup.map_sup.