proposition: Lemma Aut_isom_subproof a : {a' | a' \in Aut (f @* G) & a \in Aut G -> {in G, a' \o f =1 f \o a}}.
proof: Proof. set Aut_a := autm (subgP (subg [Aut G] a)). have aDom: 'dom (f \o Aut_a \o invm injf) = f @* G. rewrite /dom /= morphpre_invm -morphpreIim; congr (f @* _). by rewrite [_ :&: D](setIidPl _) ?injmK ?injm_autm ?im_autm. have [af [def_af ker_af _ im_af]] := domP _ aDom. have inj_a': 'injm af by rewrite ker_af !injm_comp ?injm_autm ?injm_invm. have im_a': af @* (f @* G) = f @* G. by rewrite im_af !morphim_comp morphim_invm // im_autm. pose a' := aut inj_a' im_a'; exists a' => [|AutGa x Gx]; first exact: Aut_aut. have Dx := domG Gx; rewrite /= [a' _]autE ?mem_morphim //. by rewrite def_af /= invmE // autmE subgK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)