proposition: Lemma Frobenius_action_kernel_def G H K sT S to : K ><| H = G -> @Frobenius_action _ G H sT S to -> K :=: 1 :|: [set x in G | 'Fix_(S | to)[x] == set0].
proof: Proof. move=> defG FrobG. have partG: partition (gval K |: (H^# :^: K)) G. apply: Frobenius_partition; apply/andP; rewrite defG; split=> //. by apply/Frobenius_actionP; apply: hasFrobeniusAction FrobG. have{FrobG} [ffulG transG regG ntH [u Su defH]]:= FrobG. apply/setP=> x /[!inE]; have [-> | ntx] := eqVneq; first exact: group1. rewrite /= -(cover_partition partG) /cover. have neKHy y: gval K <> H^# :^ y. by move/setP/(_ 1); rewrite group1 conjD1g setD11. rewrite big_setU1 /= ?inE; last by apply/imsetP=> [[y _ /neKHy]]. have [nsKG sHG _ _ tiKH] := sdprod_context defG; have [sKG nKG]:= andP nsKG. symmetry; case Kx: (x \in K) => /=. apply/set0Pn=> [[v /setIP[Sv]]]; have [y Gy ->] := atransP2 transG Su Sv. rewrite -sub1set -astabC sub1set astab1_act mem_conjg => Hxy. case/negP: ntx; rewrite -in_set1 -(conjgKV y x) -mem_conjgV conjs1g -tiKH. by rewrite defH setIA inE -mem_conjg (setIidPl sKG) (normsP nKG) ?Kx. apply/andP=> [[/bigcupP[_ /imsetP[y Ky ->] Hyx] /set0Pn[]]]; exists (to u y). rewrite inE (actsP (atrans_acts transG)) ?(subsetP sKG) // Su. rewrite -sub1set -astabC sub1set astab1_act. by rewrite conjD1g defH conjIg !inE in Hyx; case/and3P: Hyx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)