proposition: Lemma injm_pprodm : 'injm f = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == fH @* K].
proof: Proof. apply/idP/and3P=> [injf | [injfH injfK]]. rewrite eq_sym -{1}morphimIdom -(morphim_pprodml (subsetIl _ _)) injmI //. rewrite morphim_pprodml // morphim_pprodmr //=; split=> //. apply/injmP=> x y Hx Hy /=; rewrite -!pprodmEl //. by apply: (injmP injf); rewrite ?mem_gen ?inE ?Hx ?Hy. apply/injmP=> a b Ka Kb /=; rewrite -!pprodmEr //. by apply: (injmP injf); rewrite ?mem_gen //; apply/setUP; right. move/eqP=> fHK; rewrite ker_pprodm; apply/subsetP=> y. case/imset2P=> x a Hx /setIdP[Ka /eqP fxa] ->. have: fH x \in fH @* K by rewrite -fHK inE {2}fxa !mem_morphim. case/morphimP=> z Hz Kz /(injmP injfH) def_x. rewrite def_x // eqfHK ?inE ?Hz // in fxa. by rewrite def_x // (injmP injfK _ _ Kz Ka fxa) mulgV set11. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)