Merge pull request #592 from chdoc/mem_imset

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

7 files changed, 61 insertions, 61 deletions

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.