proposition: Lemma astabs_Aut_isom a : a \in Aut G -> (fGisom a \in 'N(f @* H | 'P)) = (a \in 'N(H | 'P)).
proof: Proof. move=> AutGa; rewrite !inE sub_morphim_pre // subsetI sHD /= /aperm. rewrite !(sameP setIidPl eqP) !eqEsubset !subsetIl; apply: eq_subset_r => x. rewrite !inE; apply: andb_id2l => Hx; have Gx: x \in G := subsetP sHG x Hx. have Dax: a x \in D by rewrite (subsetP sGD) // Aut_closed. by rewrite Aut_isomE // -!sub1set -morphim_set1 // injmSK ?sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)