proposition: Lemma ker_pprodm : 'ker f = [set x * a^-1 | x in H, a in K & fH x == fK a].
proof: Proof. apply/setP=> y; rewrite 3!inE {1}norm_joinEr //=. apply/andP/imset2P=> [[/mulsgP[x a Hx Ka ->{y}]]|[x a Hx]]. rewrite pprodmE // => fxa1. by exists x a^-1; rewrite ?invgK // inE groupVr ?morphV // eq_mulgV1 invgK. case/setIdP=> Kx /eqP fx ->{y}. by rewrite imset2_f ?pprodmE ?groupV ?morphV // fx mulgV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)