Merge pull request #592 from chdoc/mem_imset

Fix naming inconsistencies between `imset` and `map` lemmas. 

24 files changed, 137 insertions, 114 deletions

diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 9c4557a..356ff5c 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -2355,7 +2355,7 @@ Proof.
 have [[injg defR] [injh defS]] := (isomP isoG, isomP isoH).
 rewrite !morphimEdom in defS defR; apply/cfun_inP=> s.
 rewrite -{1}defS => /imsetP[x Hx ->] {s}; have Gx := subsetP sHG x Hx.
-rewrite {1}eq_hg ?(cfResE, cfIsomE) // -defS -?eq_hg ?mem_imset // -defR.
+rewrite {1}eq_hg ?(cfResE, cfIsomE) // -defS -?eq_hg ?imset_f // -defR.
 by rewrite (eq_in_imset eq_hg) imsetS.
 Qed.
 
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 3809e73..76535fa 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -396,7 +396,7 @@ apply: (iffP imageP) => [[_ /rcosetsP[y Ay ->] ->] | [y Ay ->]].
 without loss nHy: y Ay / y \in 'N(H).
   have [nHy | /cfConjgEout->] := boolP (y \in 'N(H)); first exact.
   by move/(_ 1%g); rewrite !group1 !cfConjgJ1; apply.
-exists ('I_A[phi] :* y); first by rewrite -rcosetE mem_imset.
+exists ('I_A[phi] :* y); first by rewrite -rcosetE imset_f.
 case: repr_rcosetP => z /setIP[_ /setIdP[nHz /eqP Tz]].
 by rewrite cfConjgMnorm ?Tz.
 Qed.
@@ -467,7 +467,7 @@ Proof.
 move=> nsHG; have UchiG := cfclass_uniq 'chi_i nsHG.
 apply: uniq_perm; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi.
 apply/imageP/idP=> [[j iGj ->] | /cfclassP[y]]; first by rewrite -cfclass_IirrE.
-by exists (conjg_Iirr i y); rewrite ?mem_imset ?conjg_IirrE.
+by exists (conjg_Iirr i y); rewrite ?imset_f ?conjg_IirrE.
 Qed.
 
 Lemma card_cfclass_Iirr i : H <| G -> #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|.
@@ -1560,7 +1560,7 @@ have acts_Js : [acts G, on classes K | 'Js].
   apply/subsetP=> y Gy; have nKy := subsetP nKG y Gy.
   rewrite !inE; apply/subsetP=> _ /imsetP[z Gz ->]; rewrite !inE /=.
   rewrite -class_rcoset norm_rlcoset // class_lcoset.
-  by apply: mem_imset; rewrite memJ_norm.
+  by apply: imset_f; rewrite memJ_norm.
 have acts_cto : [acts G, on classes K | cto] by rewrite astabs_ract subsetIidl.
 pose m := #|'Fix_(classes K | cto)[x]|.
 have def_m: #|'Fix_ito[x]| = m.
@@ -1573,7 +1573,7 @@ apply: contraR => notKx; apply/cards1P; exists 1%g; apply/esym/eqP.
 rewrite eqEsubset !(sub1set, inE) classes1 /= conjs1g eqxx /=.
 apply/subsetP=> _ /setIP[/imsetP[y Ky ->] /afix1P /= cyKx].
 have /imsetP[z Kz def_yx]: y ^ x \in y ^: K.
-  by rewrite -cyKx; apply: mem_imset; apply: class_refl.
+  by rewrite -cyKx; apply: imset_f; apply: class_refl.
 rewrite inE classG_eq1; apply: contraR notKx => nty.
 rewrite -(groupMr x (groupVr Kz)).
 apply: (subsetP (regK y _)); first exact/setD1P.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 2b886a6..c603f91 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -465,9 +465,9 @@ transitivity ('chi_i x * 'chi_i (x^-1)%g *+ #|h x|); last first.
       by rewrite mulf_neq0 // lin_char_neq0 /= ?cfcenter_fful_irr.
     rewrite -[z](mulKg u) -cGz // -conjMg /h classGidl {u Gu}//.
     apply/eqP/setP=> w; apply/mulsgP/mulsgP=> [][_ z1 /imsetP[v Gv ->] Zz1 ->].
-      exists (x ^ v)%g (z * z1)%g; rewrite ?mem_imset ?groupM //.
+      exists (x ^ v)%g (z * z1)%g; rewrite ?imset_f ?groupM //.
       by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg.
-    exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?mem_imset ?groupM ?groupV //.
+    exists ((x * z) ^ v)%g (z^-1 * z1)%g; rewrite ?imset_f ?groupM ?groupV //.
     by rewrite conjMg -mulgA /(z ^ v)%g cGz // mulKg mulKVg.
   rewrite !irr_inv DchiZ ?groupJ ?cfunJ // rmorphM mulrACA -!normCK -exprMn.
   by rewrite (normC_lin_char lin_lambda) ?mulr1 //= cfcenter_fful_irr.
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index faecc02..e1c7ec4 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -696,7 +696,7 @@ have [j def_chi_j]: {j | 'chi_j = phi}.
 exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx].
 rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //.
 rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy.
-by rewrite -(conjgK y x) cover_imset -class_supportEr mem_imset2 ?groupV.
+by rewrite -(conjgK y x) cover_imset -class_supportEr imset2_f ?groupV.
 Qed.
 
 End MoreVchar.
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 2d1b6e6..3679b75 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -298,7 +298,7 @@ Lemma setactE S a : to^* S a = [set to x a | x in S].
 Proof. by []. Qed.
 
 Lemma mem_setact S a x : x \in S -> to x a \in to^* S a.
-Proof. exact: mem_imset. Qed.
+Proof. exact: imset_f. Qed.
 
 Lemma card_setact S a : #|to^* S a| = #|S|.
 Proof. by apply: card_imset; apply: act_inj. Qed.
@@ -321,7 +321,7 @@ Lemma orbitP A x y :
 Proof. by apply: (iffP imsetP) => [] [a]; exists a. Qed.
 
 Lemma mem_orbit A x a : a \in A -> to x a \in orbit to A x.
-Proof. exact: mem_imset. Qed.
+Proof. exact: imset_f. Qed.
 
 Lemma afixP A x : reflect (forall a, a \in A -> to x a = x) (x \in 'Fix_to(A)).
 Proof.
@@ -607,9 +607,9 @@ Qed.
 Lemma orbit1P G x : reflect (orbit to G x = [set x]) (x \in 'Fix_to(G)).
 Proof.
 apply: (iffP afixP) => [xfix | xfix a Ga].
-  apply/eqP; rewrite eq_sym eqEsubset sub1set -{1}[x]act1 mem_imset //=.
+  apply/eqP; rewrite eq_sym eqEsubset sub1set -{1}[x]act1 imset_f //=.
   by apply/subsetP=> y; case/imsetP=> a Ga ->; rewrite inE xfix.
-by apply/set1P; rewrite -xfix mem_imset.
+by apply/set1P; rewrite -xfix imset_f.
 Qed.
 
 Lemma card_orbit1 G x : #|orbit to G x| = 1%N -> orbit to G x = [set x].
@@ -645,9 +645,9 @@ have sXS: X \subset S := transversal_sub trXP.
 split=> // [x y Xx Xy /= | x Sx].
   have Sx := subsetP sXS x Xx.
   rewrite -(inj_in_eq (pblock_inj trXP)) // eq_pblock ?defS //.
-  by rewrite (def_pblock tiP (mem_imset _ Sx)) ?orbit_refl.
+  by rewrite (def_pblock tiP (imset_f _ Sx)) ?orbit_refl.
 have /imsetP[y Xy defxG]: orbit to G x \in pblock P @: X.
-  by rewrite (pblock_transversal trXP) ?mem_imset.
+  by rewrite (pblock_transversal trXP) ?imset_f.
 suffices /orbitP[a Ga def_y]: y \in orbit to G x by exists a; rewrite ?def_y.
 by rewrite defxG mem_pblock defS (subsetP sXS).
 Qed.
@@ -719,7 +719,7 @@ Lemma acts_orbit G x : G \subset D -> [acts G, on orbit to G x | to].
 Proof.
 move/subsetP=> sGD; apply/subsetP=> a Ga; rewrite !inE sGD //.
 apply/subsetP=> _ /imsetP[b Gb ->].
-by rewrite inE -actMin ?sGD // mem_imset ?groupM.
+by rewrite inE -actMin ?sGD // imset_f ?groupM.
 Qed.
 
 Lemma acts_subnorm_fix A : [acts 'N_D(A), on 'Fix_to(D :&: A) | to].
@@ -731,7 +731,7 @@ by rewrite /= (afixP Cx) // memJ_norm // groupV (subsetP (normsGI _ _) _ nAa).
 Qed.
 
 Lemma atrans_orbit G x : [transitive G, on orbit to G x | to].
-Proof. by apply: mem_imset; apply: orbit_refl. Qed.
+Proof. by apply: imset_f; apply: orbit_refl. Qed.
 
 Section OrbitStabilizer.
 
@@ -846,7 +846,7 @@ Lemma atrans_acts_in G S :
   G \subset D -> [transitive G, on S | to] -> [acts G, on S | to].
 Proof.
 move=> sGD transG; apply/subsetP=> a Ga; rewrite !inE (subsetP sGD) //.
-by apply/subsetP=> x /(atransPin sGD transG) <-; rewrite inE mem_imset.
+by apply/subsetP=> x /(atransPin sGD transG) <-; rewrite inE imset_f.
 Qed.
 
 Lemma subgroup_transitivePin G H S x :
@@ -1030,7 +1030,7 @@ Proof. by move=> GtrS x y /(atransP GtrS) <- /imsetP. Qed.
 Lemma atrans_acts G S : [transitive G, on S | to] -> [acts G, on S | to].
 Proof.
 move=> GtrS; apply/subsetP=> a Ga; rewrite !inE.
-by apply/subsetP=> x /(atransP GtrS) <-; rewrite inE mem_imset.
+by apply/subsetP=> x /(atransP GtrS) <-; rewrite inE imset_f.
 Qed.
 
 Lemma atrans_supgroup G H S :
@@ -1052,11 +1052,11 @@ apply/idP/andP=> [GtrS | [nSG]].
   apply/andP; split=> //; apply/subsetP=> _ /imsetP[x Sx ->].
   by rewrite inE (atransP GtrS).
 rewrite eqn_leq andbC lt0n => /andP[/existsP[X /imsetP[x Sx X_Gx]]].
-rewrite (cardD1 X) {X}X_Gx mem_imset // ltnS leqn0 => /eqP GtrS.
+rewrite (cardD1 X) {X}X_Gx imset_f // ltnS leqn0 => /eqP GtrS.
 apply/imsetP; exists x => //; apply/eqP.
 rewrite eqEsubset acts_sub_orbit // Sx andbT.
 apply/subsetP=> y Sy; have:= card0_eq GtrS (orbit to G y).
-by rewrite !inE /= mem_imset // andbT => /eqP <-; apply: orbit_refl.
+by rewrite !inE /= imset_f // andbT => /eqP <-; apply: orbit_refl.
 Qed.
 
 Lemma atrans_dvd G S : [transitive G, on S | to] -> #|S| %| #|G|.
@@ -1107,7 +1107,7 @@ have:= sHC; rewrite subsetI sub_astab1 => /andP[sHG cHx].
 have Tx: x \in T by rewrite inE Sx.
 apply: (iffP idP) => [trN | trC].
   apply/setP=> Ha; apply/setIdP/imsetP=> [[]|[a Ca ->{Ha}]]; last first.
-    by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite mem_imset.
+    by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite imset_f.
   case/imsetP=> a Ga ->{Ha}; rewrite subsetI !sub_conjg => /andP[_ sHCa].
   have Txa: to x a^-1 \in T.
     by rewrite inE -sub_astab1 astab1_act actGS ?Sx ?groupV.
@@ -1117,7 +1117,7 @@ apply: (iffP idP) => [trN | trC].
 apply/imsetP; exists x => //; apply/setP=> y; apply/idP/idP=> [Ty|].
   have [Sy cHy]:= setIP Ty; have [a Ga defy] := atransP2 trGS Sx Sy.
   have: H :^ a^-1 \in H :^: C.
-    rewrite -trC inE subsetI mem_imset 1?conj_subG ?groupV // sub_conjgV.
+    rewrite -trC inE subsetI imset_f 1?conj_subG ?groupV // sub_conjgV.
     by rewrite -astab1_act -defy sub_astab1.
   case/imsetP=> b /setIP[Gb /astab1P cxb] defHb.
   rewrite defy -{1}cxb -actM mem_orbit // inE groupM //.
@@ -1267,7 +1267,7 @@ apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa.
 have [Da _] := setIP sDa; rewrite !inE Da.
 apply/subsetP/subsetP=> [cSa _ /imsetP[x Sx ->] | cSa x Sx]; rewrite !inE.
   by have:= cSa x Sx; rewrite inE -val_eqE val_subact sDa.
-by have:= cSa _ (mem_imset val Sx); rewrite inE -val_eqE val_subact sDa.
+by have:= cSa _ (imset_f val Sx); rewrite inE -val_eqE val_subact sDa.
 Qed.
 
 Lemma astabs_subact S : 'N(S | subaction) = subact_dom :&: 'N(val @: S | to).
@@ -1275,8 +1275,8 @@ Proof.
 apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa.
 have [Da _] := setIP sDa; rewrite !inE Da.
 apply/subsetP/subsetP=> [nSa _ /imsetP[x Sx ->] | nSa x Sx]; rewrite !inE.
-  by have:= nSa x Sx; rewrite inE => /(mem_imset val); rewrite val_subact sDa.
-have:= nSa _ (mem_imset val Sx); rewrite inE => /imsetP[y Sy def_y].
+  by have:= nSa x Sx; rewrite inE => /(imset_f val); rewrite val_subact sDa.
+have:= nSa _ (imset_f val Sx); rewrite inE => /imsetP[y Sy def_y].
 by rewrite ((_ a =P y) _) // -val_eqE val_subact sDa def_y.
 Qed.
 
@@ -1316,9 +1316,9 @@ Canonical quotient_action := [action of qact].
 Lemma acts_qact_dom : [acts qact_dom, on 'N(H) | to].
 Proof.
 apply/subsetP=> a nNa; rewrite !inE (astabs_dom nNa); apply/subsetP=> x Nx.
-have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE mem_imset.
+have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f.
 rewrite inE -(astabs_act _ nNa) => /rcosetsP[y Ny defHy].
-have: to x a \in H :* y by rewrite -defHy (mem_imset (to^~a)) ?rcoset_refl.
+have: to x a \in H :* y by rewrite -defHy (imset_f (to^~a)) ?rcoset_refl.
 by apply: subsetP; rewrite mul_subG ?sub1set ?normG.
 Qed.
 
@@ -1328,11 +1328,11 @@ Lemma qactEcond x a :
     = coset H (if a \in qact_dom then to x a else x).
 Proof.
 move=> Nx; apply: val_inj; rewrite val_subact //= qact_subdomE.
-have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE mem_imset.
+have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f.
 case nNa: (a \in _); rewrite // -(astabs_act _ nNa).
 rewrite !val_coset ?(acts_act acts_qact_dom nNa) //=.
 case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_eqP.
-by rewrite rcoset_sym -defHy (mem_imset (_^~_)) ?rcoset_refl.
+by rewrite rcoset_sym -defHy (imset_f (_^~_)) ?rcoset_refl.
 Qed.
 
 Lemma qactE x a :
@@ -1580,7 +1580,7 @@ Proof.
 move=> sAB; apply/setP=> x; rewrite !inE /morphim (setIidPr sAB).
 apply/subsetP/subsetP=> [cAx _ /imsetP[a Aa ->] | cfAx a Aa].
   by move/cAx: Aa; rewrite !inE.
-by rewrite inE; move/(_ (f a)): cfAx; rewrite inE mem_imset // => ->.
+by rewrite inE; move/(_ (f a)): cfAx; rewrite inE imset_f // => ->.
 Qed.
 
 Lemma astab_comp S : 'C(S | comp_action) = f @*^-1 'C(S | to).
@@ -2163,7 +2163,7 @@ rewrite eqEcard (card_preimset _ (act_inj _ _)) leqnn andbT.
 apply/subsetP=> x Nx; rewrite inE; move/(astabs_act (H :* x)): HDa.
 rewrite mem_rcosets mulSGid ?normG // Nx => /rcosetsP[y Ny defHy].
 suffices: to x a \in H :* y by apply: subsetP; rewrite mul_subG ?sub1set ?normG.
-by rewrite -defHy; apply: mem_imset; apply: rcoset_refl.
+by rewrite -defHy; apply: imset_f; apply: rcoset_refl.
 Qed.
 
 Lemma qact_is_groupAction : is_groupAction (R / H) (to / H).
@@ -2326,12 +2326,12 @@ Lemma morph_astabs : f @* 'N(S | to1) = 'N(h @: S | to2).
 Proof.
 apply/setP=> fx; apply/morphimP/idP=> [[x D1x nSx ->] | nSx].
   rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->].
-  by rewrite inE -hfJ ?mem_imset // (astabs_act _ nSx).
+  by rewrite inE -hfJ ?imset_f // (astabs_act _ nSx).
 have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
   by rewrite defD2 (astabs_dom nSx).
 exists x => //; rewrite !inE D1x; apply/subsetP=> u Su.
 have /imsetP[u' Su' /injh def_u']: h (to1 u x) \in h @: S.
-  by rewrite hfJ // -def_fx (astabs_act _ nSx) mem_imset.
+  by rewrite hfJ // -def_fx (astabs_act _ nSx) imset_f.
 by rewrite inE def_u' ?actsDR ?(subsetP sSR).
 Qed.
 
@@ -2344,13 +2344,13 @@ have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
   by rewrite defD2 (astab_dom cSx).
 exists x => //; rewrite !inE D1x; apply/subsetP=> u Su.
 rewrite inE -(inj_in_eq injh) ?actsDR ?(subsetP sSR) ?hfJ //.
-by rewrite -def_fx (astab_act cSx) ?mem_imset.
+by rewrite -def_fx (astab_act cSx) ?imset_f.
 Qed.
 
 Lemma morph_afix : h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A).
 Proof.
 apply/setP=> hu; apply/imsetP/setIP=> [[u /setIP[Su cAu] ->]|].
-  split; first by rewrite mem_imset.
+  split; first by rewrite imset_f.
   by apply/afixP=> _ /morphimP[x D1x Ax ->]; rewrite -hfJ ?(afixP cAu).
 case=> /imsetP[u Su ->] /afixP c_hu_fA; exists u; rewrite // inE Su.
 apply/afixP=> x Ax; have Dx := subsetP sAD1 x Ax.
@@ -2498,7 +2498,7 @@ by rewrite -groupV -{1 3}(mulg1 G) rcoset_sym -sub1set -mulGS -!rcosetE.
 Qed.
 
 Lemma atransR G : [transitive G, on G | 'R].
-Proof. by rewrite /atrans -{1}(mul1g G) -orbitR mem_imset. Qed.
+Proof. by rewrite /atrans -{1}(mul1g G) -orbitR imset_f. Qed.
 
 Lemma faithfulR G : [faithful G, on G | 'R].
 Proof. by rewrite /faithful astabR subsetIr. Qed.
@@ -2555,7 +2555,7 @@ Lemma afixRs_rcosets A G : 'Fix_(rcosets G A | 'Rs)(G) = rcosets G 'N_A(G).
 Proof.
 apply/setP=> Gx; apply/setIP/rcosetsP=> [[/rcosetsP[x Ax ->]]|[x]].
   by rewrite sub_afixRs_norm => Nx; exists x; rewrite // inE Ax.
-by case/setIP=> Ax Nx ->; rewrite -{1}rcosetE mem_imset // sub_afixRs_norm.
+by case/setIP=> Ax Nx ->; rewrite -{1}rcosetE imset_f // sub_afixRs_norm.
 Qed.
 
 Lemma astab1Rs G : 'C[G : {set gT} | 'Rs] = G.
@@ -2669,7 +2669,7 @@ Proof. by apply: acts_sum_card_orbit; apply/actsP=> x Gx y; apply: groupJr. Qed.
 Lemma class_formula : \sum_(C in classes G) #|G : 'C_G[repr C]| = #|G|.
 Proof.
 rewrite -sum_card_class; apply: eq_bigr => _ /imsetP[x Gx ->].
-have: x \in x ^: G by rewrite -{1}(conjg1 x) mem_imset.
+have: x \in x ^: G by rewrite -{1}(conjg1 x) imset_f.
 by case/mem_repr/imsetP=> y Gy ->; rewrite index_cent1 classGidl.
 Qed.
 
@@ -2687,7 +2687,7 @@ rewrite -sum_card_class -sum1_card (leqif_sum cGgt0).
 apply/abelian_classP/forall_inP=> [cGG _ /imsetP[x Gx ->]| cGG x Gx].
   by rewrite cGG ?cards1.
 apply/esym/eqP; rewrite eqEcard sub1set cards1 class_refl leq_eqVlt cGG //.
-exact: mem_imset.
+exact: imset_f.
 Qed.
 
 End CardClass.
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index 009e723..b9ed8e1 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -134,7 +134,7 @@ Proof.
 move=> x y /=; wlog Ay: x y / y \in A.
   by move=> IH eqfxy; case: ifP (eqfxy); [symmetry | case: ifP => //]; auto.
 rewrite Ay; case: ifP => [Ax | nAx def_x]; first exact: injf.
-by case/negP: nAx; rewrite def_x (subsetP sBf) ?mem_imset.
+by case/negP: nAx; rewrite def_x (subsetP sBf) ?imset_f.
 Qed.
 
 Definition perm_in := perm perm_in_inj.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index c828225..38b3490 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1142,7 +1142,7 @@ Proof. by rewrite conjDg conjs1g. Qed.
 (* Classes; not much for now. *)
 
 Lemma memJ_class x y A : y \in A -> x ^ y \in x ^: A.
-Proof. exact: mem_imset. Qed.
+Proof. exact: imset_f. Qed.
 
 Lemma classS x A B : A \subset B -> x ^: A \subset x ^: B.
 Proof. exact: imsetS. Qed.
@@ -1164,18 +1164,18 @@ by rewrite -[xy]invgK def_xy -conjVg; exists y.
 Qed.
 
 Lemma mem_classes x A : x \in A -> x ^: A \in classes A.
-Proof. exact: mem_imset. Qed.
+Proof. exact: imset_f. Qed.
 
 Lemma memJ_class_support A B x y :
    x \in A -> y \in B -> x ^ y \in class_support A B.
-Proof. by move=> Ax By; apply: mem_imset2. Qed.
+Proof. by move=> Ax By; apply: imset2_f. Qed.
 
 Lemma class_supportM A B C :
   class_support A (B * C) = class_support (class_support A B) C.
 Proof.
 apply/setP=> x; apply/imset2P/imset2P=> [[a y Aa] | [y c]].
   case/mulsgP=> b c Bb Cc -> ->{x y}.
-  by exists (a ^ b) c; rewrite ?(mem_imset2, conjgM).
+  by exists (a ^ b) c; rewrite ?(imset2_f, conjgM).
 case/imset2P=> a b Aa Bb -> Cc ->{x y}.
 by exists a (b * c); rewrite ?(mem_mulg, conjgM).
 Qed.
@@ -1376,7 +1376,7 @@ Proof. by rewrite lt0n; apply/existsP; exists (1 : gT). Qed.
 Lemma indexg_gt0 A : 0 < #|G : A|.
 Proof.
 rewrite lt0n; apply/existsP; exists A.
-by rewrite -{2}[A]mulg1 -rcosetE; apply: mem_imset.
+by rewrite -{2}[A]mulg1 -rcosetE; apply: imset_f.
 Qed.
 
 Lemma trivgP : reflect (G :=: 1) (G \subset [1]).
@@ -1677,7 +1677,7 @@ Proof.
 rewrite (cardsD1 1) classes1 ltnS lt0n cards_eq0.
 apply/set0Pn/trivgPn=> [[xG /setD1P[nt_xG]] | [x Gx ntx]].
   by case/imsetP=> x Gx def_xG; rewrite def_xG classG_eq1 in nt_xG; exists x.
-by exists (x ^: G); rewrite !inE classG_eq1 ntx; apply: mem_imset.
+by exists (x ^: G); rewrite !inE classG_eq1 ntx; apply: imset_f.
 Qed.
 
 Lemma mem_class_support A x : x \in A -> x \in class_support A G.
@@ -2326,7 +2326,7 @@ by apply: eq_bigr => i _; rewrite genGidG.
 Qed.
 
 Lemma mem_commg A B x y : x \in A -> y \in B -> [~ x, y] \in [~: A, B].
-Proof. by move=> Ax By; rewrite mem_gen ?mem_imset2. Qed.
+Proof. by move=> Ax By; rewrite mem_gen ?imset2_f. Qed.
 
 Lemma commSg A B C : A \subset B -> [~: A, C] \subset [~: B, C].
 Proof. by move=> sAC; rewrite genS ?imset2S. Qed.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index b1181c0..7e14ce0 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -1369,7 +1369,7 @@ move=> sAH sBK; rewrite [f @* _]morphimEsub /=; last first.
   by rewrite norm_joinEr // mulgSS.
 apply/setP=> y; apply/imsetP/idP=> [[_ /mulsgP[x a Ax Ba ->] ->{y}] |].
   have Hx := subsetP sAH x Ax; have Ka := subsetP sBK a Ba.
-  by rewrite pprodmE // mem_imset2 ?mem_morphim.
+  by rewrite pprodmE // imset2_f ?mem_morphim.
 case/mulsgP=> _ _ /morphimP[x Hx Ax ->] /morphimP[a Ka Ba ->] ->{y}.
 by exists (x * a); rewrite ?mem_mulg ?pprodmE.
 Qed.
@@ -1391,7 +1391,7 @@ 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 mem_imset2 ?pprodmE ?groupV ?morphV // fx mulgV.
+by rewrite imset2_f ?pprodmE ?groupV ?morphV // fx mulgV.
 Qed.
 
 Lemma injm_pprodm :
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index ef707e1..ac4aaa7 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -223,7 +223,7 @@ Proof. by rewrite /morphim setIA setIid. Qed.
 Lemma morphpreIim R : f @*^-1 (f @* D :&: R) = f @*^-1 R.
 Proof.
 apply/setP=> x; rewrite morphimEdom !inE.
-by case Dx: (x \in D); rewrite // mem_imset.
+by case Dx: (x \in D); rewrite // imset_f.
 Qed.
 
 Lemma morphimIim A : f @* D :&: f @* A = f @* A.
@@ -276,7 +276,7 @@ Proof.
 wlog suffices: A / f @* A^-1 \subset (f @* A)^-1.
   by move=> IH; apply/eqP; rewrite eqEsubset IH -invSg invgK -{1}(invgK A) IH.
 apply/subsetP=> _ /morphimP[x Dx Ax' ->]; rewrite !inE in Ax' *.
-by rewrite -morphV // mem_imset // inE groupV Dx.
+by rewrite -morphV // imset_f // inE groupV Dx.
 Qed.
 
 Lemma morphpreV R : f @*^-1 R^-1 = (f @*^-1 R)^-1.
@@ -290,9 +290,9 @@ Proof.
 move=> sAD; rewrite /morphim setIC -group_modl // (setIidPr sAD).
 apply/setP=> fxy; apply/idP/idP.
   case/imsetP=> _ /imset2P[x y Ax /setIP[Dy By] ->] ->{fxy}.
-  by rewrite morphM // (subsetP sAD, mem_imset2) // mem_imset // inE By.
+  by rewrite morphM // (subsetP sAD, imset2_f) // imset_f // inE By.
 case/imset2P=> _ _ /imsetP[x Ax ->] /morphimP[y Dy By ->] ->{fxy}.
-by rewrite -morphM // (subsetP sAD, mem_imset) // mem_mulg // inE By.
+by rewrite -morphM // (subsetP sAD, imset_f) // mem_mulg // inE By.
 Qed.
 
 Lemma morphimMr A B : B \subset D -> f @* (A * B) = f @* A * f @* B.
@@ -307,7 +307,7 @@ 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, mem_imset2).
+  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.
@@ -409,7 +409,7 @@ move=> sKG; apply/eqP; rewrite eqEsubset morphimI setIC.
 apply/subsetP=> _ /setIP[/morphimP[x Dx Ax ->] /morphimP[z Dz Gz]].
 case/ker_rcoset=> {Dz}// y Ky def_x.
 have{z Gz y Ky def_x} Gx: x \in G by rewrite def_x groupMl // (subsetP sKG).
-by rewrite mem_imset ?inE // Dx Gx Ax.
+by rewrite imset_f ?inE // Dx Gx Ax.
 Qed.
 
 Lemma morphimIG A G : 'ker f \subset G -> f @* (A :&: G) = f @* A :&: f @* G.
@@ -442,8 +442,8 @@ Qed.
 Lemma morphim_groupset G : group_set (f @* G).
 Proof.
 apply/group_setP; split=> [|_ _ /morphimP[x Dx Gx ->] /morphimP[y Dy Gy ->]].
-  by rewrite -morph1 mem_imset ?group1.
-by rewrite -morphM ?mem_imset ?inE ?groupM.
+  by rewrite -morph1 imset_f ?group1.
+by rewrite -morphM ?imset_f ?inE ?groupM.
 Qed.
 
 Canonical morphpre_group fPh M :=
@@ -470,7 +470,7 @@ apply/idP/idP=> [/andP[Dx /morphimP[y Dy Ay eqxy]] | /imset2P[z y Kz Ay ->{x}]].
   rewrite -(mulgKV y x) mem_mulg // !inE !(groupM, morphM, groupV) //.
   by rewrite morphV //= eqxy mulgV.
 have [Dy Dz]: y \in D /\ z \in D by rewrite (subsetP sAD) // dom_ker.
-by rewrite groupM // morphM // mker // mul1g mem_imset // inE Dy.
+by rewrite groupM // morphM // mker // mul1g imset_f // inE Dy.
 Qed.
 
 Lemma morphimGK G : 'ker f \subset G -> G \subset D -> f @*^-1 (f @* G) = G.
@@ -608,9 +608,9 @@ rewrite morphim_gen; last first; last congr <<_>>.
 apply/setP=> fz; apply/morphimP/imset2P=> [[z _] | [fx fy]].
   case/imset2P=> x y Ax By -> -> {z fz}.
   have Dx := sAD x Ax; have Dy := sBD y By.
-  by exists (f x) (f y); rewrite ?(mem_imset, morphR) // ?(inE, Dx, Dy).
+  by exists (f x) (f y); rewrite ?(imset_f, morphR) // ?(inE, Dx, Dy).
 case/morphimP=> x Dx Ax ->{fx}; case/morphimP=> y Dy By ->{fy} -> {fz}.
-by exists [~ x, y]; rewrite ?(inE, morphR, groupR, mem_imset2).
+by exists [~ x, y]; rewrite ?(inE, morphR, groupR, imset2_f).
 Qed.
 
 Lemma morphim_norm A : f @* 'N(A) \subset 'N(f @* A).
@@ -1072,7 +1072,7 @@ Qed.
 Lemma morphpre_factm (C : {set rT}) : ff @*^-1 C =  q @* (f @*^-1 C).
 Proof.
 apply/setP=> y; rewrite !inE /=; apply/andP/morphimP=> [[]|[x Hx]]; last first.
-  by case/morphpreP=> Gx Cfx ->; rewrite factmE ?mem_imset ?inE ?Hx.
+  by case/morphpreP=> Gx Cfx ->; rewrite factmE ?imset_f ?inE ?Hx.
 case/morphimP=> x Hx Gx ->; rewrite factmE //.
 by exists x; rewrite // !inE Gx.
 Qed.
@@ -1268,7 +1268,7 @@ apply: (iffP eqP) => [eqfGH | [injf <-]]; last first.
   by rewrite -injmD1 // morphimEsub ?subsetDl.
 split.
   apply/subsetP=> x /morphpreP[Gx fx1]; have: f x \notin H^# by rewrite inE fx1.
-  by apply: contraR => ntx; rewrite -eqfGH mem_imset // inE ntx.
+  by apply: contraR => ntx; rewrite -eqfGH imset_f // inE ntx.
 rewrite morphimEdom -{2}(setD1K (group1 G)) imsetU eqfGH.
 by rewrite imset_set1 morph1 setD1K.
 Qed.
@@ -1501,7 +1501,7 @@ Lemma ker_subg : 'ker (subg G) = 1. Proof. exact/trivgP. Qed.
 Lemma im_subg : subg G @* G = [subg G].
 Proof.
 apply/eqP; rewrite -subTset morphimEdom.
-by apply/subsetP=> u _; rewrite -(sgvalK u) mem_imset ?subgP.
+by apply/subsetP=> u _; rewrite -(sgvalK u) imset_f ?subgP.
 Qed.
 
 Lemma sgval_sub A : sgval @* A \subset G.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index d0ba321..ebd4230 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -351,7 +351,7 @@ Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|porbits s|.
 Lemma apermE x s : aperm x s = s x. Proof. by []. Qed.
 
 Lemma mem_porbit s i x : (s ^+ i) x \in porbit s x.
-Proof. by rewrite (mem_imset (aperm x)) ?mem_cycle. Qed.
+Proof. by rewrite (imset_f (aperm x)) ?mem_cycle. Qed.
 
 Lemma porbit_id s x : x \in porbit s x.
 Proof. by rewrite -{1}[x]perm1 (mem_porbit s 0). Qed.
@@ -442,9 +442,9 @@ have xfC a b u: xf b a (t a b u) = xf a b u.
   by move/lt_xf: (lt_a); rewrite -(tXC a b) 1?ltnW //= orbC [_ || _]eq_xf.
 pose ts := t x y s; rewrite /= -[_ * s]/ts.
 pose dp u := #|porbits u :\ porbit u y :\ porbit u x|.
-rewrite !(addnC #|_|) (cardsD1 (porbit ts y)) mem_imset ?inE //.
-rewrite (cardsD1 (porbit ts x)) inE mem_imset ?inE //= -/(dp ts) {}/ts.
-rewrite (cardsD1 (porbit s y)) (cardsD1 (porbit s x)) !(mem_imset, inE) //.
+rewrite !(addnC #|_|) (cardsD1 (porbit ts y)) imset_f ?inE //.
+rewrite (cardsD1 (porbit ts x)) inE imset_f ?inE //= -/(dp ts) {}/ts.
+rewrite (cardsD1 (porbit s y)) (cardsD1 (porbit s x)) !(imset_f, inE) //.
 rewrite -/(dp s) !addnA !eq_porbit_mem andbT; congr (_ + _); last first.
   wlog suffices: s / dp s <= dp (t x y s).
     by move=> IHs; apply/eqP; rewrite eqn_leq -{2}(tK x y s) !IHs.
@@ -452,7 +452,7 @@ rewrite -/(dp s) !addnA !eq_porbit_mem andbT; congr (_ + _); last first.
   rewrite !inE andbA andbC !(eq_sym C) => /and3P[/imsetP[z _ ->{C}]].
   rewrite 2!eq_porbit_mem => sxz syz.
   suffices ts_z: porbit (t x y s) z = porbit s z.
-    by rewrite -ts_z !eq_porbit_mem {1 2}ts_z sxz syz mem_imset ?inE.
+    by rewrite -ts_z !eq_porbit_mem {1 2}ts_z sxz syz imset_f ?inE.
   suffices exp_id n: ((t x y s) ^+ n) z = (s ^+ n) z.
     apply/setP=> u; apply/idP/idP=> /imsetP[_ /cycleP[i ->] ->].
       by rewrite /aperm exp_id mem_porbit.
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index f73fda5..4fd84fb 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -301,7 +301,7 @@ Lemma quotient_setIpre A D : (A :&: coset H @*^-1 D) / H = A / H :&: D.
 Proof. exact: morphim_setIpre. Qed.
 
 Lemma mem_quotient x G : x \in G -> coset H x \in G / H.
-Proof. by move=> Gx; rewrite -imset_coset mem_imset. Qed.
+Proof. by move=> Gx; rewrite -imset_coset imset_f. Qed.
 
 Lemma quotientS A B : A \subset B -> A / H \subset B / H.
 Proof. exact: morphimS. Qed.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 3a5caeb..469c649 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1153,7 +1153,7 @@ Proof.
 rewrite morphim_gen ?genS //; last by rewrite -gen_subG Ohm_sub.
 apply/subsetP=> fx /morphimP[x Gx]; rewrite inE Gx /=.
 case/OhmPredP=> p p_pr xpn_1 -> {fx}.
-rewrite inE morphimEdom mem_imset //=; apply/OhmPredP; exists p => //.
+rewrite inE morphimEdom imset_f //=; apply/OhmPredP; exists p => //.
 by rewrite -morphX // xpn_1 morph1.
 Qed.
 
@@ -1251,7 +1251,7 @@ move=> pG; apply/eqP; rewrite eqEsubset !gen_subG; apply/andP.
 do [split; apply/subsetP=> xpn; case/imsetP=> x] => [|Gx ->]; last first.
   by rewrite Mho_p_elt ?(mem_p_elt pG).
 case/setIdP=> Gx _ ->; have [-> | ntx] := eqVneq x 1; first by rewrite expg1n.
-by rewrite (pdiv_p_elt (mem_p_elt pG Gx) ntx) mem_gen //; apply: mem_imset.
+by rewrite (pdiv_p_elt (mem_p_elt pG Gx) ntx) mem_gen //; apply: imset_f.
 Qed.
 
 Lemma MhoEabelian p G :
@@ -1260,7 +1260,7 @@ Proof.
 move=> pG cGG; rewrite (MhoE pG); rewrite gen_set_id //; apply/group_setP.
 split=> [|xn yn]; first by apply/imsetP; exists 1; rewrite ?expg1n.
 case/imsetP=> x Gx ->; case/imsetP=> y Gy ->.
-by rewrite -expgMn; [apply: mem_imset; rewrite groupM | apply: (centsP cGG)].
+by rewrite -expgMn; [apply: imset_f; rewrite groupM | apply: (centsP cGG)].
 Qed.
 
 Lemma trivg_Mho G : 'Mho^n(G) == 1 -> 'Ohm_n(G) == G.
@@ -1269,7 +1269,7 @@ rewrite -subG1 gen_subG eqEsubset Ohm_sub /= => Gp1.
 rewrite -{1}(Sylow_gen G) genS //; apply/bigcupsP=> P.
 case/SylowP=> p p_pr /and3P[sPG pP _]; apply/subsetP=> x Px.
 have Gx := subsetP sPG x Px; rewrite inE Gx //=.
-rewrite (sameP eqP set1P) (subsetP Gp1) ?mem_gen //; apply: mem_imset.
+rewrite (sameP eqP set1P) (subsetP Gp1) ?mem_gen //; apply: imset_f.
 by rewrite inE Gx; apply: pgroup_p (mem_p_elt pP Px).
 Qed.
 
@@ -1277,7 +1277,7 @@ Lemma Mho_p_cycle p x : p.-elt x -> 'Mho^n(<[x]>) = <[x ^+ (p ^ n)]>.
 Proof.
 move=> p_x.
 apply/eqP; rewrite (MhoE p_x) eqEsubset cycle_subG mem_gen; last first.
-  by apply: mem_imset; apply: cycle_id.
+  by apply: imset_f; apply: cycle_id.
 rewrite gen_subG andbT; apply/subsetP=> _ /imsetP[_ /cycleP[k ->] ->].
 by rewrite -expgM mulnC expgM mem_cycle.
 Qed.
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index 615e0ac..7b1aed7 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -200,7 +200,7 @@ Proof.
 move=> cHK; apply/setP=> z; rewrite {3}/center centM !inE.
 have cKH: H \subset 'C(K) by rewrite centsC.
 apply/imset2P/and3P=> [[x y /setIP[Hx cHx] /setIP[Ky cKy] ->{z}]| []].
-  by rewrite mem_imset2 ?groupM // ?(subsetP cHK) ?(subsetP cKH).
+  by rewrite imset2_f ?groupM // ?(subsetP cHK) ?(subsetP cKH).
 case/imset2P=> x y Hx Ky ->{z}.
 rewrite groupMr => [cHx|]; last exact: subsetP Ky.
 rewrite groupMl => [cKy|]; last exact: subsetP Hx.
diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v
index a1ffb65..904c4e9 100644
--- a/mathcomp/solvable/commutator.v
+++ b/mathcomp/solvable/commutator.v
@@ -181,7 +181,7 @@ Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)).
 Proof.
 rewrite gen_subG; apply/subsetP/subsetP=> [sRH x Gx | nGH xy].
   rewrite inE; apply/subsetP=> _ /imsetP[y Ky ->].
-  by rewrite conjg_Rmul groupMr // sRH // mem_imset2 ?groupV.
+  by rewrite conjg_Rmul groupMr // sRH // imset2_f ?groupV.
 case/imset2P=> x y Gx Hy ->{xy}.
 by rewrite commgEr groupMr // memJ_norm (groupV, nGH).
 Qed.
@@ -254,7 +254,7 @@ Proof.
 have R_C := sameP trivgP commG1P.
 rewrite -subG1 R_C gen_subG -{}R_C gen_subG.
 apply: (iffP subsetP) => [cABC x y z Ax By Cz | cABC xyz].
-  by apply/set1P; rewrite cABC // !mem_imset2.
+  by apply/set1P; rewrite cABC // !imset2_f.
 by case/imset2P=> _ z /imset2P[x y Ax By ->] Cz ->; rewrite cABC.
 Qed.
 
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index d82009b..334255e 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -131,7 +131,7 @@ Lemma cycleM a b :
 Proof.
 move=> cab co_ab; apply/eqP; rewrite eqEsubset -(cent_joinEl (cents_cycle cab)).
 rewrite join_subG {3}cab !cycleMsub // 1?coprime_sym //.
-by rewrite -genM_join cycle_subG mem_gen // mem_imset2 ?cycle_id.
+by rewrite -genM_join cycle_subG mem_gen // imset2_f ?cycle_id.
 Qed.
 
 Lemma cyclicM A B :
@@ -716,7 +716,7 @@ apply/setP=> C; apply/idP/imsetP=> [| [gC GdC ->{C}]].
   case/imsetP=> x /setIdP[_ oxd] ->; exists <[x]>%G => //.
   by rewrite -def_Gd inE -Zp_cycle subsetT.
 have:= GdC; rewrite -def_Gd => /setIdP[_ /eqP <-].
-by rewrite (set1P GdC) /= mem_imset // inE eqxx (mem_cycle x1).
+by rewrite (set1P GdC) /= imset_f // inE eqxx (mem_cycle x1).
 Qed.
 
 Section FieldMulCyclic.
@@ -742,7 +742,7 @@ elim/big_ind2: _ => // [m1 n1 m2 n2 | d _]; first exact: leq_add.
 set Gd := _ @: _; case: (set_0Vmem Gd) => [-> | [C]]; first by rewrite cards0.
 rewrite {}/Gd => /imsetP[x /setIdP[Gx /eqP <-] _ {C d}].
 rewrite order_dvdG // (@eq_card1 _ <[x]>) ?mul1n // => C.
-apply/idP/eqP=> [|-> {C}]; last by rewrite mem_imset // inE Gx eqxx.
+apply/idP/eqP=> [|-> {C}]; last by rewrite imset_f // inE Gx eqxx.
 by case/imsetP=> y /setIdP[Gy /eqP/ucG->].
 Qed.
 
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index 42882bc..8185773 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -792,7 +792,7 @@ have defK: K = [set w].
   rewrite add0n -[j./2]odd_double_half addnC doubleD -!muln2 -mulnA.
   rewrite -(expg_mod_order v) ov modnMDl; case: (odd _); last first.
     right; rewrite mulg1 /r -(subnKC n_gt2) expnSr mulnA expgM.
-    by apply: mem_imset; rewrite inE.
+    by apply: imset_f; rewrite inE.
   rewrite (inj_eq (mulIg _)) -expg_mod_order ou -[k]odd_double_half.
   rewrite addnC -muln2 mulnDl -mulnA def2r modnMDl -ou expg_mod_order.
   case: (odd k); [left | right]; rewrite ?mul1n ?mul1g //.
@@ -996,7 +996,7 @@ have defG': G^`(1) = <[x ^+ 2]>.
   by rewrite -def2q -def2r mulnA mulnK.
 have defG1: 'Mho^1(G) = <[x ^+ 2]>.
   apply/eqP; rewrite (MhoE _ pG) eqEsubset !gen_subG sub1set andbC.
-  rewrite mem_gen; last exact: mem_imset.
+  rewrite mem_gen; last exact: imset_f.
   apply/subsetP=> z2; case/imsetP=> z Gz ->{z2}.
   case Xz: (z \in X); last by rewrite -{1}(oX' z) ?expg_order ?group1 // inE Xz.
   by case/cycleP: Xz => i ->; rewrite expgAC mem_cycle.
@@ -1195,7 +1195,7 @@ have defG': G^`(1) = <[x ^+ 2]>.
   by rewrite -def2q -def2r mulnA mulnK.
 have defG1: 'Mho^1(G) = <[x ^+ 2]>.
   apply/eqP; rewrite (MhoE _ pG) eqEsubset !gen_subG sub1set andbC.
-  rewrite mem_gen; last exact: mem_imset.
+  rewrite mem_gen; last exact: imset_f.
   apply/subsetP=> z2; case/imsetP=> z Gz ->{z2}.
   case Xz: (z \in X).
     by case/cycleP: Xz => i ->; rewrite -expgM mulnC expgM mem_cycle.
@@ -1373,7 +1373,7 @@ have defG': G^`(1) = <[x ^+ 2]>.
   by rewrite -def2q -def2r mulnA mulnK.
 have defG1: 'Mho^1(G) = <[x ^+ 2]>.
   apply/eqP; rewrite (MhoE _ pG) eqEsubset !gen_subG sub1set andbC.
-  rewrite mem_gen; last exact: mem_imset.
+  rewrite mem_gen; last exact: imset_f.
   apply/subsetP=> z2; case/imsetP=> z Gz ->{z2}.
   case Xz: (z \in X).
     by case/cycleP: Xz => i ->; rewrite -expgM mulnC expgM mem_cycle.
diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v
index 0fa02be..35c189a 100644
--- a/mathcomp/solvable/finmodule.v
+++ b/mathcomp/solvable/finmodule.v
@@ -462,8 +462,8 @@ apply: (addrI (\sum_(Hx in HG) fmalpha (repr Hx * (rX Hx)^-1))).
 rewrite {1}(reindex_acts 'Rs _ Gg) ?actsRs_rcosets // -!big_split /=.
 apply: eq_bigr => _ /rcosetsP[x Gx ->]; rewrite !rcosetE -!rcosetM.
 case: repr_rcosetP => h1 Hh1; case: repr_rcosetP => h2 Hh2.
-have: H :* (x * g) \in rcosets H G by rewrite -rcosetE mem_imset ?groupM.
-have: H :* x \in rcosets H G by rewrite -rcosetE mem_imset.
+have: H :* (x * g) \in rcosets H G by rewrite -rcosetE imset_f ?groupM.
+have: H :* x \in rcosets H G by rewrite -rcosetE imset_f.
 case/mem_rX/rcosetP=> h3 Hh3 -> /mem_rX/rcosetP[h4 Hh4 ->].
 rewrite -!(mulgA h1) -!(mulgA h2) -!(mulgA h3) !(mulKVg, invMg).
 by rewrite addrC -!zmodMgE -!morphM ?groupM ?groupV // -!mulgA !mulKg.
@@ -512,12 +512,12 @@ Let sXG : {subset X <= G}. Proof. exact/subsetP/(transversal_sub trX). Qed.
 Lemma rcosets_cycle_transversal : H_g_rcosets @: X = HGg.
 Proof.
 have sHXgHGg x: x \in X -> H_g_rcosets x \in HGg.
-  by move/sXG=> Gx; apply: mem_imset; rewrite -rcosetE mem_imset.
+  by move/sXG=> Gx; apply: imset_f; rewrite -rcosetE imset_f.
 apply/setP=> Hxg; apply/imsetP/idP=> [[x /sHXgHGg HGgHxg -> //] | HGgHxg].
 have [_ /rcosetsP[z Gz ->] ->] := imsetP HGgHxg.
 pose Hzg := H :* z * <[g]>; pose x := transversal_repr 1 X Hzg.
 have HGgHzg: Hzg \in HG :* <[g]>.
-  by rewrite mem_mulg ?set11 // -rcosetE mem_imset.
+  by rewrite mem_mulg ?set11 // -rcosetE imset_f.
 have Hzg_x: x \in Hzg by rewrite (repr_mem_pblock trX).
 exists x; first by rewrite (repr_mem_transversal trX).
 case/mulsgP: Hzg_x => y u /rcoset_eqP <- /(orbit_act 'Rs) <- -> /=.
@@ -567,7 +567,7 @@ have trY: is_transversal Y HG G.
   have eq_xx': x = x'.
     apply: (pblock_inj trX) => //; have /andP[/and3P[_ tiX _] _] := trX.
     have HGgHyg: H :* y * <[g]> \in HG :* <[g]>.
-      by rewrite mem_mulg ?set11 // -rcosetE mem_imset ?(subsetP sYG).
+      by rewrite mem_mulg ?set11 // -rcosetE imset_f ?(subsetP sYG).
     rewrite !(def_pblock tiX HGgHyg) //.
       by rewrite -[x'](mulgK (g ^+ j)) mem_mulg // groupV mem_cycle.
     by rewrite -[x](mulgK (g ^+ i)) mem_mulg ?rcoset_refl // groupV mem_cycle.
@@ -578,7 +578,7 @@ have rYE x i : x \in X -> i < n_ x -> rY (H :* x :* g ^+ i) = x * g ^+ i.
   move=> Xx lt_i_x; rewrite -rcosetM; apply: (canLR_in (pblockK trY 1)).
     by apply/bigcupP; exists x => //; apply/imsetP; exists (Ordinal lt_i_x).
   apply/esym/def_pblock; last exact: rcoset_refl; first by case/and3P: partHG.
-  by rewrite -rcosetE mem_imset ?groupM ?groupX // sXG.
+  by rewrite -rcosetE imset_f ?groupM ?groupX // sXG.
 rewrite (transfer_indep trY Gg) /V -/rY (set_partition_big _ partHGg) /=.
 rewrite -defHgX big_imset /=; last first.
   apply/imset_injP; rewrite defHgX (card_transversal trX) defHGg.
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v
index 6234224..119a9fc 100644
--- a/mathcomp/solvable/hall.v
+++ b/mathcomp/solvable/hall.v
@@ -851,7 +851,7 @@ have trNPA: A :^: AG ::&: N = A :^: N.
   pose NG := 'N_G(P); have sNG_G : NG \subset G := subsetIl _ _.
   have nNGA: A \subset 'N(NG) by rewrite normsI ?norms_norm.
   apply/setP=> Ax; apply/setIdP/imsetP=> [[]|[x Nx ->{Ax}]]; last first.
-    by rewrite conj_subG //; case/setIP: Nx => AGx; rewrite mem_imset.
+    by rewrite conj_subG //; case/setIP: Nx => AGx; rewrite imset_f.
   have ->: N = A <*> NG by rewrite /N /AG !norm_joinEl // -group_modl.
   have coNG_A := coprimeSg sNG_G coGA; case/imsetP=> x AGx ->{Ax}.
   case/SchurZassenhaus_trans_actsol; rewrite ?cardJg // => y Ny /= ->.
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index 3d3162b..cd121cb 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -325,7 +325,7 @@ Lemma qacts_coset (H K : {group rT}) :
 Proof.
 move=> sHD aK.
 apply/subsetP=> x qdx; rewrite inE qdx inE; apply/subsetP=> y.
-case/morphimP=> z Nz Kz /= e; rewrite e inE qactE // mem_imset // inE.
+case/morphimP=> z Nz Kz /= e; rewrite e inE qactE // imset_f // inE.
 move/gactsP: aK; move/(_ x (subsetP (qact_dom_doms sHD) _ qdx) z); rewrite Kz.
 move->; move/acts_act: (acts_qact_dom to H); move/(_ x qdx z).
 by rewrite Nz andbT.
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 95b7184..3786cff 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -301,7 +301,7 @@ apply/andP; split.
   apply/abelemP=> //; rewrite [abelian _]quotient_cents2 ?joing_subl //.
   split=> // _ /morphimP[x Nx Px ->] /=.
   rewrite -morphX //= coset_id // (MhoE 1 pP) joing_idr expn1.
-  by rewrite mem_gen //; apply/setUP; right; apply: mem_imset.
+  by rewrite mem_gen //; apply/setUP; right; apply: imset_f.
 rewrite -quotient_cents2 // [_ \subset 'C(_)]abP (MhoE 1 pP) gen_subG /=.
 apply/subsetP=> _ /imsetP[x Px ->]; rewrite expn1.
 have nPhi_x: x \in 'N('Phi(P)) by apply: (subsetP nPhiP).
@@ -731,7 +731,7 @@ rewrite -{1}defG' gen_subG; apply/subsetP=> _ /imset2P[x y Gx Gy ->].
 have Zxy: [~ x, y] \in 'Z(G) by rewrite -defG' mem_commg.
 have Zxp: x ^+ p \in 'Z(G).
   rewrite -defPhi (Phi_joing pG) (MhoE 1 pG) joing_idr mem_gen // !inE.
-  by rewrite expn1 orbC (mem_imset (expgn^~ p)).
+  by rewrite expn1 orbC (imset_f (expgn^~ p)).
 rewrite mem_morphpre /= ?defG' ?Zxy // inE -commXg; last first.
   by red; case/setIP: Zxy => _ /centP->.
 by apply/commgP; red; case/setIP: Zxp => _ /centP->.
@@ -1157,7 +1157,7 @@ have defS: <<X>> = S.
   apply: Phi_nongen; apply/eqP; rewrite eqEsubset join_subG sPS sXS -joing_idr.
   rewrite -genM_join sub_gen // -quotientSK ?quotient_gen // -defSb genS //.
   apply/subsetP=> xb Xxb; apply/imsetP; rewrite (setIidPr nPX).
-  by exists (repr xb); rewrite /= ?coset_reprK //; apply: mem_imset.
+  by exists (repr xb); rewrite /= ?coset_reprK //; apply: imset_f.
 pose f (a : {perm gT}) := [ffun x => if x \in X then x^-1 * a x else 1].
 have injf: {in A &, injective f}.
   move=> _ _ /morphimP[y nSy Ry ->] /morphimP[z nSz Rz ->].
@@ -1544,7 +1544,7 @@ have{genXp minU xp1 sVU ltVU} expVp: exponent V %| p.
 have{A pA defA1 sX'A V expVp} Zxy: [~ x, y] \in Z.
   rewrite -defA1 (OhmE 1 pA) mem_gen // !inE (exponentP expVp).
     by rewrite (subsetP sX'A) //= mem_commg ?(subsetP sUX).
-  by rewrite groupMl -1?[x^-1]conjg1 mem_gen // mem_imset2 // ?groupV cycle_id.
+  by rewrite groupMl -1?[x^-1]conjg1 mem_gen // imset2_f // ?groupV cycle_id.
 have{Zxy sUX cZX} cXYxy: [~ x, y] \in 'C(XY).
   by rewrite centsC in cZX; rewrite defXY (subsetP (centS sUX)) ?(subsetP cZX).
 rewrite -defU1 exponent_Ohm1_class2 // nil_class2 -defXY der1_joing_cycles //.
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index e6016e8..80005a4 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -80,7 +80,7 @@ apply/forallP/maximal_eqP=> /= [primG | [_ maxCx] Q].
       case/imsetP=> _ /imsetP[b Hb ->] ->.
       by rewrite !(actsP (atrans_acts trG)) //; apply: subsetP Hb.
     case: (atransP2 trG Sx Sy) => a Ga ->.
-    by exists ((to^*)%act X a); apply: mem_imset; rewrite // orbit_refl.
+    by exists ((to^*)%act X a); apply: imset_f; rewrite // orbit_refl.
   apply/trivIsetP=> _ _ /imsetP[a Ga ->] /imsetP[b Gb ->].
   apply: contraR => /exists_inP[_ /imsetP[_ /imsetP[a1 Ha1 ->] ->]].
   case/imsetP=> _ /imsetP[b1 Hb1 ->] /(canLR (actK _ _)) /(canLR (actK _ _)).
@@ -95,7 +95,7 @@ have QX: X \in Q by rewrite pblock_mem ?defS.
 have toX Y a: Y \in Q -> a \in G -> to x a \in Y -> sto X a = Y.
   move=> QY Ga Yxa; rewrite -(contraNeq (trivIsetP tIQ Y (sto X a) _ _)) //.
     by rewrite (actsP actQ).
-  by apply/existsP; exists (to x a); rewrite /= Yxa; apply: mem_imset.
+  by apply/existsP; exists (to x a); rewrite /= Yxa; apply: imset_f.
 have defQ: Q = orbit (to^*)%act G X.
   apply/eqP; rewrite eqEsubset andbC acts_sub_orbit // QX.
   apply/subsetP=> Y QY.
@@ -245,7 +245,7 @@ apply/imsetP; exists t => //.
 apply/setP=> u; apply/idP/imsetP=> [du | [a Ga ->{u}]].
   case: (ext_t u du) => y; rewrite tr_xt.
   by case/imsetP=> a Ga [_ def_u]; exists a => //; apply: val_inj.
-have: n_act to xt a \in dtuple_on _ S by rewrite tr_xt mem_imset.
+have: n_act to xt a \in dtuple_on _ S by rewrite tr_xt imset_f.
 by rewrite n_act_add dtuple_on_add; case/and3P.
 Qed.
 
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index d419745..836c323 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -424,7 +424,7 @@ rewrite (reindex (fun p : {ffun _} => [ffun i => f0 (p i)])) /=; last first.
     by rewrite ffunE eqxx.
   rewrite -im_f0 => /andP[/andP[/ffun_onP f_ffun /injectiveP injf] /eqP im_f].
   apply/ffunP=> i; rewrite !ffunE /ff0'; case: pickP => [y /eqP //|].
-  have /imsetP[j _ eq_f0j_fi]: f i \in f0 @: 'I_k by rewrite -im_f mem_imset.
+  have /imsetP[j _ eq_f0j_fi]: f i \in f0 @: 'I_k by rewrite -im_f imset_f.
   by move/(_ j)/eqP.
 rewrite -ffactnn -card_inj_ffuns -sum1dep_card; apply: eq_bigl => p.
 rewrite -andbA.
@@ -434,10 +434,10 @@ set f := finfun _.
 have injf: injective f by move=> i j; rewrite !ffunE => /inj_f0; apply: inj_p.
 have imIkf : imIk f == A.
   rewrite eqEcard card_imset // cardAk card_ord leqnn andbT -im_f0.
-  by apply/subsetP=> x /imsetP[i _ ->]; rewrite ffunE mem_imset.
+  by apply/subsetP=> x /imsetP[i _ ->]; rewrite ffunE imset_f.
 split; [|exact/injectiveP|exact: imIkf].
 apply/ffun_onP => x; apply: (subsetP AsubB).
-by rewrite -(eqP imIkf) mem_imset.
+by rewrite -(eqP imIkf) imset_f.
 Qed.
 
 Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 7d41b12..4a3eaf1 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1246,16 +1246,21 @@ apply: (iffP imageP) => [[[x1 x2] Dx12] | [x1 x2 Dx1 Dx2]] -> {y}.
 by exists (x1, x2); rewrite //= !inE Dx1.
 Qed.
 
-Lemma mem_imset (D : {pred aT}) x : x \in D -> f x \in f @: D.
+Lemma imset_f (D : {pred aT}) x : x \in D -> f x \in f @: D.
 Proof. by move=> Dx; apply/imsetP; exists x. Qed.
 
+Lemma mem_imset_eq (D : {pred aT}) x : injective f -> f x \in f @: D = (x \in D).
+Proof.
+by move=> f_inj; apply/imsetP/idP;[case=> [y] ? /f_inj -> | move=> ?; exists x].
+Qed.
+
 Lemma imset0 : f @: set0 = set0.
 Proof. by apply/setP => y; rewrite inE; apply/imsetP=> [[x]]; rewrite inE. Qed.
 
 Lemma imset_eq0 (A : {set aT}) : (f @: A == set0) = (A == set0).
 Proof.
 have [-> | [x Ax]] := set_0Vmem A; first by rewrite imset0 !eqxx.
-by rewrite -!cards_eq0 (cardsD1 x) Ax (cardsD1 (f x)) mem_imset.
+by rewrite -!cards_eq0 (cardsD1 x) Ax (cardsD1 (f x)) imset_f.
 Qed.
 
 Lemma imset_set1 x : f @: [set x] = [set f x].
@@ -1264,16 +1269,24 @@ apply/setP => y.
 by apply/imsetP/set1P=> [[x' /set1P-> //]| ->]; exists x; rewrite ?set11.
 Qed.
 
-Lemma mem_imset2 (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
+Lemma imset2_f (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
     x \in D -> x2 \in D2 x ->
   f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)).
 Proof. by move=> Dx Dx2; apply/imset2P; exists x x2. Qed.
 
+Lemma mem_imset2_eq (D : {pred aT}) (D2 : aT -> {pred aT2}) x x2 :
+    injective2 f2 ->
+  f2 x x2 \in imset2 f2 (mem D) (fun x1 => mem (D2 x1)) = ((x \in D) && (x2 \in D2 x)).
+Proof.
+move=> inj2_f; apply/imset2P/andP => [|[xD xD2]]; last by exists x x2.
+by move => [x' x2' xD xD2 eq_f2]; case: (inj2_f _ _ _ _ eq_f2) => -> ->.
+Qed.
+
 Lemma sub_imset_pre (A : {pred aT}) (B : {pred rT}) :
   (f @: A \subset B) = (A \subset f @^-1: B).
 Proof.
 apply/subsetP/subsetP=> [sfAB x Ax | sAf'B fx].
-  by rewrite inE sfAB ?mem_imset.
+  by rewrite inE sfAB ?imset_f.
 by case/imsetP=> x Ax ->; move/sAf'B: Ax; rewrite inE.
 Qed.
 
@@ -1313,7 +1326,7 @@ Lemma imset_proper (A B : {set aT}) :
 Proof.
 move=> injf /properP[sAB [x Bx nAx]]; rewrite properE imsetS //=.
 apply: contra nAx => sfBA.
-have: f x \in f @: A by rewrite (subsetP sfBA) ?mem_imset.
+have: f x \in f @: A by rewrite (subsetP sfBA) ?imset_f.
 by case/imsetP=> y Ay /injf-> //; apply: subsetP sAB y Ay.
 Qed.
 
@@ -1341,7 +1354,7 @@ Proof.
 move=> injf; apply/eqP; rewrite eqEsubset subsetI.
 rewrite 2?imsetS (andTb, subsetIl, subsetIr) //=.
 apply/subsetP=> _ /setIP[/imsetP[x Ax ->] /imsetP[z Bz /injf eqxz]].
-by rewrite mem_imset // inE Ax eqxz.
+by rewrite imset_f // inE Ax eqxz.
 Qed.
 
 Lemma imset2Sl (A B : {pred aT}) (C : {pred aT2}) :
@@ -1585,7 +1598,7 @@ Lemma imset_comp (f : T' -> U) (g : T -> T') (H : {pred T}) :
 Proof.
 apply/setP/subset_eqP/andP.
 split; apply/subsetP=> _ /imsetP[x0 Hx0 ->]; apply/imsetP.
-  by exists (g x0); first apply: mem_imset.
+  by exists (g x0); first apply: imset_f.
 by move/imsetP: Hx0 => [x1 Hx1 ->]; exists x1.
 Qed.
 
@@ -1766,14 +1779,14 @@ Qed.
 Lemma curry_imset2l : f @2: (D1, D2) = \bigcup_(x1 in D1) f x1 @: D2.
 Proof.
 apply/setP=> y; apply/imset2P/bigcupP => [[x1 x2 Dx1 Dx2 ->{y}] | [x1 Dx1]].
-  by exists x1; rewrite // mem_imset.
+  by exists x1; rewrite // imset_f.
 by case/imsetP=> x2 Dx2 ->{y}; exists x1 x2.
 Qed.
 
 Lemma curry_imset2r : f @2: (D1, D2) = \bigcup_(x2 in D2) f^~ x2 @: D1.
 Proof.
 apply/setP=> y; apply/imset2P/bigcupP => [[x1 x2 Dx1 Dx2 ->{y}] | [x2 Dx2]].
-  by exists x2; rewrite // (mem_imset (f^~ x2)).
+  by exists x2; rewrite // (imset_f (f^~ x2)).
 by case/imsetP=> x1 Dx1 ->{y}; exists x1 x2.
 Qed.
 
@@ -1898,7 +1911,7 @@ Lemma cover_imset J F : cover (F @: J) = \bigcup_(i in J) F i.
 Proof.
 apply/setP=> x.
 apply/bigcupP/bigcupP=> [[_ /imsetP[i Ji ->]] | [i]]; first by exists i.
-by exists (F i); first apply: mem_imset.
+by exists (F i); first apply: imset_f.
 Qed.
 
 Lemma trivIimset J F (P := F @: J) :
@@ -1986,7 +1999,7 @@ Hypothesis eqiR : {in D & &, equivalence_rel R}.
 
 Let Pxx x : x \in D -> x \in Px x.
 Proof. by move=> Dx; rewrite !inE Dx (eqiR Dx Dx). Qed.
-Let PPx x : x \in D -> Px x \in P := fun Dx => mem_imset _ Dx.
+Let PPx x : x \in D -> Px x \in P := fun Dx => imset_f _ Dx.
 
 Lemma equivalence_partitionP : partition P D.
 Proof.
@@ -2058,7 +2071,7 @@ case/and3P=> /eqP <- tiP notP0; apply/and3P; split; first exact/and3P.
 apply/forall_inP=> B PB; have /set0Pn[x Bx]: B != set0 := memPn notP0 B PB.
 apply/cards1P; exists (odflt x [pick y in pblock P x]); apply/esym/eqP.
 rewrite eqEsubset sub1set inE -andbA; apply/andP; split.
-  by apply/mem_imset/bigcupP; exists B.
+  by apply/imset_f/bigcupP; exists B.
 rewrite (def_pblock tiP PB Bx); case def_y: _ / pickP => [y By | /(_ x)/idP//].
 rewrite By /=; apply/subsetP=> _ /setIP[/imsetP[z Pz ->]].
 case: {1}_ / pickP => [t zPt Bt | /(_ z)/idP[]]; last by rewrite mem_pblock.
@@ -2381,3 +2394,8 @@ Qed.
 End Greatest.
 
 End SetFixpoint.
+
+Notation mem_imset := 
+  ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _).
+Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => 
+  deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _).
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index f189dcb..c789e67 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -21,3 +21,8 @@ Proof. by case. Qed.
 Lemma inj_compr A B C (f : B -> A) (h : C -> B) :
    injective (f \o h) -> injective h.
 Proof. by move=> fh_inj x y /(congr1 f) /fh_inj. Qed.
+
+Definition injective2 (rT aT1 aT2 : Type) (f : aT1 -> aT2 -> rT) :=
+  forall (x1 x2 : aT1) (y1 y2 : aT2), f x1 y1 = f x2 y2 -> (x1 = x2) * (y1 = y2).
+
+Arguments injective2 [rT aT1 aT2] f.