proposition: Lemma Aut_sub_fullP : reflect (forall h : {morphism H >-> gT}, 'injm h -> h @* H = H -> exists g : {morphism G >-> gT}, [/\ 'injm g, g @* G = G & {in H, g =1 h}]) (Aut_in (Aut G) H \isog Aut H).
proof: Proof. rewrite (isog_transl _ Aut_in_isog) /=; set rG := _ @* _. apply: (iffP idP) => [iso_rG h injh hH| AutHinG]. have: aut injh hH \in rG; last case/morphimP=> g nHg AutGg def_g. suffices ->: rG = Aut H by apply: Aut_aut. by apply/eqP; rewrite eqEcard restr_perm_Aut /= (card_isog iso_rG). exists (autm_morphism AutGg); rewrite injm_autm im_autm; split=> // x Hx. by rewrite -(autE injh hH Hx) def_g actpermE actbyE. suffices ->: rG = Aut H by apply: isog_refl. apply/eqP; rewrite eqEsubset restr_perm_Aut /=. apply/subsetP=> h AutHh; have hH := im_autm AutHh. have [g [injg gG eq_gh]] := AutHinG _ (injm_autm AutHh) hH. have [Ng AutGg]: aut injg gG \in 'N(H | 'P) /\ aut injg gG \in Aut G. rewrite Aut_aut !inE; split=> //; apply/subsetP=> x Hx. by rewrite inE /= /aperm autE ?(subsetP sHG) // -hH eq_gh ?mem_morphim. apply/morphimP; exists (aut injg gG) => //; apply: (eq_Aut AutHh) => [|x Hx]. by rewrite (subsetP restr_perm_Aut) // mem_morphim. by rewrite restr_permE //= /aperm autE ?eq_gh ?(subsetP sHG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)