proposition: Lemma isom_restr_perm a : a \in Aut G -> fHisom (inH a) = infH (fGisom a).
proof: Proof. move=> AutGa; case nHa: (a \in 'N(H | 'P)); last first. by rewrite !triv_restr_perm ?astabs_Aut_isom ?nHa ?morph1. apply: (eq_Aut (Aut_Aut_isom injf sHD _)) => [|fx Hfx /=]. by rewrite (Aut_restr_perm (morphimS f sHG)) ?Aut_Aut_isom. have [x Dx Hx def_fx] := morphimP Hfx; have Gx := subsetP sHG x Hx. rewrite {1}def_fx Aut_isomE ?(Aut_restr_perm sHG) //. by rewrite !restr_permE ?astabs_Aut_isom // def_fx Aut_isomE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)