Lean: turn an internal coprime-action theorem into an automorphism-group statement via SemidirectProduct

Recipe for a theorem about A : Subgroup (MulAut K), e.g. 'coprime A acting trivially on K/Φ(K) is trivial'. Set G := K ⋊[A.subtype] A. Finite G comes from Finite.of_equiv _ SemidirectProduct.equivProd.symm. Take K' := inl.range and A' := inr.range. The cardinalities come from Nat.card_congr (MonoidHom.ofInjective inl_injective).toEquiv. Normality: change (inl : K →* G).range.Normal; rw [SemidirectProduct.range_inl_eq_ker_rightHom]; infer_instance. Plain rw fails after set. The key identity is inl_aut : inl (φ g n) = inr g * inl n * inr g⁻¹. Follow it with map_inv so that group sees (inr σ)⁻¹ rather than the atom inr σ⁻¹. To move Φ(K) into Φ(K'), use frattini_le_comap_frattini_of_surjective along inl.rangeRestrict (rangeRestrict_surjective). Transport solvability through (MonoidHom.ofInjective _).symm.toMonoidHom. Inside fun h => ... the bound instance is not found, so write fun h => by have := h; exact .... Corollary pattern for p-groups: split orderOf g = p^e * n' with Nat.exists_eq_pow_mul_and_not_dvd, compute orderOf (g^(p^e)) = n' with orderOf_pow_of_dvd, then apply the theorem to zpowers of it, using Nat.card_zpowers and Subgroup.orderOf_coe.