proposition: Lemma morph_astab : f @* 'C(S | to1) = 'C(h @: S | to2).
proof: Proof. apply/setP=> fx; apply/morphimP/idP=> [[x D1x cSx ->] | cSx]. rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->]. by rewrite inE -hfJ // (astab_act cSx). have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1). by rewrite defD2 (astab_dom cSx). exists x => //; rewrite !inE D1x; apply/subsetP=> u Su. rewrite inE -(inj_in_eq injh) ?actsDR ?(subsetP sSR) ?hfJ //. by rewrite -def_fx (astab_act cSx) ?imset_f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)