Lean/Mathlib: Gaschütz's relative complement theorem without cohomology, via an explicit crossed hom

Mathlib (v4.35) has Schur–Zassenhaus for abelian N but not Gaschütz 1952. The statement: N abelian normal, N ≤ H, gcd(|N|,[G:H]) = 1; then N is complemented in G iff it is complemented in H. A concrete proof that formalizes in ~200 lines: let K be a complement in H and t_q := q.out for q : G ⧸ H. For g and q there is a unique m_q(g) ∈ N with t_{g•q}⁻¹ m⁻¹ g t_q ∈ K. Existence: t_{gq}⁻¹ g t_q ∈ H (QuotientGroup.eq + out_eq'), split it with Subgroup.mem_sup_of_normal_left, and conjugate the N-part. Uniqueness: the quotient of two candidates lies in N ∩ K. Put m(g) = ∏_q m_q(g) in N, using open scoped IsMulCommutative for the CommGroup instance on the subtype. Then m(gh) = (MulAut.conjNormal g)(m h) * m g; reindex with Fintype.prod_equiv (MulAction.toPerm h). Also m(n) = n^[G:H] for n ∈ N, because n • q = q. So C = {g | m g = 1} is a subgroup. powCoprime gives both N ∩ C = 1 and N C = G (take n = powCoprime.symm (m g)⁻¹; then m(n g) = 1). Finish with isComplement'_of_disjoint_and_mul_eq_univ. The membership proofs are all convert K.mul_mem spec1 spec2 using 1; group. Gotcha: set a := (g • q).out blocks group from matching later occurrences. Use generalize (g • q).out = a at * after collecting the specs. For the converse use Dedekind by hand: Subgroup G has no IsModularLattice instance.