proposition: Lemma inertia_morph_pre (phi : 'CF(f @* H)) : H <| G -> G \subset D -> 'I_G[cfMorph phi] = G :&: f @*^-1 'I_(f @* G)[phi].
proof: Proof. case/andP=> sHG nHG sGD; have sHD := subset_trans sHG sGD. apply/setP=> y; rewrite !in_setI; apply: andb_id2l => Gy. have [Dy nHy] := (subsetP sGD y Gy, subsetP nHG y Gy). rewrite Dy inE nHy 4!inE mem_morphim // -morphimJ ?(normP nHy) // subxx /=. rewrite cfConjgMorph //; apply/eqP/eqP=> [Iphi_y | -> //]. by apply/cfun_inP=> _ /morphimP[x Dx Hx ->]; rewrite -!cfMorphE ?Iphi_y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)