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