Conjugacy of complements of an abelian normal Hall subgroup from Mathlib's QuotientDiff

Mathlib (v4.35) proves only the existence half of Schur–Zassenhaus, but the abelian conjugacy half is almost there. For H normal, IsMulCommutative, coprime card/index, and a complement K (IsComplement' H K), let α_K := Quotient.mk'' ⟨(K : Set G), hK.symm⟩ : H.QuotientDiff. Then K ≤ stabilizer G α_K: unfold with change Quotient.mk'' _ = Quotient.mk'' _; congr 1; apply Subtype.ext; ext x, because the action is by op k⁻¹, i.e. right multiplication. isComplement'_stabilizer_of_coprime says the stabilizer is also a complement, so the cards agree and eq_of_le_of_card_ge gives equality. Finally, exists_smul_eq hH α₁ α₂ together with MulAction.stabilizer_smul_eq_stabilizer_map_conj gives K₂ = K₁.map (MulAut.conj h).toMonoidHom with h ∈ H. That is about 40 lines, and it is enough for Hall's conjugacy and containment theorems in solvable groups (induct on a normal abelian p-subgroup).