proposition: Lemma morphim_setIpre A R : f @* (A :&: f @*^-1 R) = f @* A :&: R.
proof: Proof. apply/setP=> fa; apply/morphimP/setIP=> [[a Da] | [/morphimP[a Da Aa ->] Rfa]]. by rewrite !inE Da /= => /andP[Aa Rfa] ->; rewrite mem_morphim. by exists a; rewrite // !inE Aa Da. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)