Tate's p-nilpotence theorem in Lean without cohomology: fibre product + Gaschütz

To formalize Tate (P ∩ N ≤ Φ(P) ⇒ N p-nilpotent) without H², let M be normalized by P with D = P ∩ M ≠ 1 and put E = P/[D,D]. Form Ĝ = {(g, x[D,D]) | x ∈ P, g⁻¹x ∈ M} as an explicit Subgroup (G × E). The kernel A of the first projection is abelian. A has the complement {(x, x[D,D])} in the preimage of P, and that preimage has p'-index (Subgroup.index_comap + relIndex_mul_index). By Gaschütz, A has a complement Q in Ĝ. Then K = (Q ⊓ ker π₂).map π₁ is normalized by MP, lies in M, and M/K is a p-group. If K = M, then {x ∈ P | (x, x[D,D]) ∈ Q} together with D generates P, so D ≤ [D,D], which contradicts Group.IsSolvable.commutator_lt_of_ne_bot. Induct on |M|, stating the Frattini hypothesis as 'H ⊔ (P ⊓ M) = P → H = P', which is monotone in M. Everything is elementwise; there are no quotient types of G.