proposition: Lemma cfIndMorph (f : {morphism D >-> rT}) (phi : 'CF(f @* H)) : 'ker f \subset H -> H \subset G -> G \subset D -> 'Ind[G] (cfMorph phi) = cfMorph ('Ind[f @* G] phi).
proof: Proof. move=> sKH sHG sGD; have [sHD inD] := (subset_trans sHG sGD, subsetP sGD). apply/cfun_inP=> /= x Gx; have [Dx sKG] := (inD x Gx, subset_trans sKH sHG). rewrite cfMorphE ?cfIndE ?morphimS // (partition_big_imset f) -morphimEsub //=. rewrite card_morphim (setIidPr sHD) natf_indexg // invfM invrK -mulrA. congr (_ * _); rewrite mulr_sumr; apply: eq_bigr => _ /morphimP[y Dy Gy ->]. rewrite -(card_rcoset _ y) mulr_natl -sumr_const. apply: eq_big => [z | z /andP[Gz /eqP <-]]. have [Gz | G'z] := boolP (z \in G). by rewrite (sameP eqP (rcoset_kerP _ _ _)) ?inD. by case: rcosetP G'z => // [[t Kt ->]]; rewrite groupM // (subsetP sKG). have [Dz Dxz] := (inD z Gz, inD (x ^ z) (groupJ Gx Gz)); rewrite -morphJ //. have [Hxz | notHxz] := boolP (x ^ z \in H); first by rewrite cfMorphE. by rewrite !cfun0 // -sub1set -morphim_set1 // morphimSGK ?sub1set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)