rename mem_imset2 to imset2_f (with deprecation)

4 files changed, 5 insertions, 5 deletions

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 4733b55..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 :
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index 5af62c9..3786cff 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -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 //.