Merge pull request #592 from chdoc/mem_imset

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

10 files changed, 30 insertions, 30 deletions

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.