proposition: Lemma morphpreMl R S : R \subset f @* D -> f @*^-1 (R * S) = f @*^-1 R * f @*^-1 S.
proof: Proof. move=> sRfD; apply/setP=> x; rewrite !inE. apply/andP/imset2P=> [[Dx] | [y z]]; last first. rewrite !inE => /andP[Dy Rfy] /andP[Dz Rfz] ->. by rewrite ?(groupM, morphM, imset2_f). case/imset2P=> fy fz Rfy Rfz def_fx. have /morphimP[y Dy _ def_fy]: fy \in f @* D := subsetP sRfD fy Rfy. exists y (y^-1 * x); last by rewrite mulKVg. by rewrite !inE Dy -def_fy. by rewrite !inE groupM ?(morphM, morphV, groupV) // def_fx -def_fy mulKg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)