rename mem_imset2 to imset2_f (with deprecation)

3 files changed, 8 insertions, 8 deletions

diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 2a498d0..38b3490 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1168,14 +1168,14 @@ 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.
@@ -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 3530b35..ac4aaa7 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -290,7 +290,7 @@ 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) // imset_f // 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, imset_f) // mem_mulg // inE By.
 Qed.
@@ -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.
@@ -610,7 +610,7 @@ apply/setP=> fz; apply/morphimP/imset2P=> [[z _] | [fx fy]].
   have Dx := sAD x Ax; have Dy := sBD y By.
   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).