proposition: Lemma trans_subnorm_fixP x G H S : let C := 'C_G[x | to] in let T := 'Fix_(S | to)(H) in [transitive G, on S | to] -> x \in S -> H \subset C -> reflect ((H :^: G) ::&: C = H :^: C) [transitive 'N_G(H), on T | to].
proof: Proof. move=> C T trGS Sx sHC; have actGS := acts_act (atrans_acts trGS). have:= sHC; rewrite subsetI sub_astab1 => /andP[sHG cHx]. have Tx: x \in T by rewrite inE Sx. apply: (iffP idP) => [trN | trC]. apply/setP=> Ha; apply/setIdP/imsetP=> [[]|[a Ca ->{Ha}]]; last first. by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite imset_f. case/imsetP=> a Ga ->{Ha}; rewrite subsetI !sub_conjg => /andP[_ sHCa]. have Txa: to x a^-1 \in T. by rewrite inE -sub_astab1 astab1_act actGS ?Sx ?groupV. have [b] := atransP2 trN Tx Txa; case/setIP=> Gb nHb cxba. exists (b * a); last by rewrite conjsgM (normP nHb). by rewrite inE groupM //; apply/astab1P; rewrite actM -cxba actKV. apply/imsetP; exists x => //; apply/setP=> y; apply/idP/idP=> [Ty|]. have [Sy cHy]:= setIP Ty; have [a Ga defy] := atransP2 trGS Sx Sy. have: H :^ a^-1 \in H :^: C. rewrite -trC inE subsetI imset_f 1?conj_subG ?groupV // sub_conjgV. by rewrite -astab1_act -defy sub_astab1. case/imsetP=> b /setIP[Gb /astab1P cxb] defHb. rewrite defy -{1}cxb -actM mem_orbit // inE groupM //. by apply/normP; rewrite conjsgM -defHb conjsgKV. case/imsetP=> a /setIP[Ga nHa] ->{y}. by rewrite inE actGS // Sx (acts_act (acts_fix_norm _) nHa). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)