5 files changed, 29 insertions, 17 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v
index 9a8032d..e1f64c8 100644
--- a/mathcomp/fingroup/action.v
+++ b/mathcomp/fingroup/action.v
@@ -2703,6 +2703,7 @@ Canonical aut_groupAction := GroupAction autact_is_groupAction.
 
 End AutAct.
 
+Arguments autact {gT} G%g.
 Arguments aut_action {gT} G%g.
 Arguments aut_groupAction {gT} G%g.
 Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index f436102..4bb638c 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -577,7 +577,7 @@ Lemma conjg_inj : @left_injective T T T conjg.
 Proof. by move=> y; apply: can_inj (conjgK y). Qed.
 
 Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1).
-Proof. by rewrite -(inj_eq (@conjg_inj y) x) conj1g. Qed.
+Proof. by rewrite (canF_eq (conjgK _)) conj1g. Qed.
 
 Lemma conjg_prod I r (P : pred I) F z :
   (\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
@@ -1854,6 +1854,9 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope.
 
 Prenex Implicits subg sgval subg_of.
 Bind Scope group_scope with subg_of.
+Arguments subgK {gT G}.
+Arguments sgvalK {gT G}.
+Arguments subg_inj {gT G} [u1 u2] eq_u12 : rename.
 
 Arguments trivgP {gT G}.
 Arguments trivGP {gT G}.
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index cb02991..aa2a809 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -873,6 +873,7 @@ Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope.
 Notation "f @: D" := (morph_dom_group f D) : Group_scope.
 
 Arguments injmP {aT rT D f}.
+Arguments morphpreK {aT rT D f} [R] sRf.
 
 Section IdentityMorphism.
 
@@ -1491,10 +1492,10 @@ Canonical sgval_morphism := Morphism (@sgvalM _ G).
 Canonical subg_morphism := Morphism (@subgM _ G).
 
 Lemma injm_sgval : 'injm sgval.
-Proof. by apply/injmP; apply: in2W; apply: subg_inj. Qed.
+Proof. exact/injmP/(in2W subg_inj). Qed.
 
 Lemma injm_subg : 'injm (subg G).
-Proof. by apply/injmP; apply: can_in_inj (@subgK _ _). Qed.
+Proof. exact/injmP/(can_in_inj subgK). Qed.
 Hint Resolve injm_sgval injm_subg : core.
 
 Lemma ker_sgval : 'ker sgval = 1. Proof. exact/trivgP. Qed.
@@ -1537,3 +1538,6 @@ Proof. exact: isom_isog isom_subg. Qed.
 
 End SubMorphism.
 
+Arguments sgvalmK {gT G} A.
+Arguments subgmK {gT G} [A] sAG.
+
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index b1a7dd7..8c97ab1 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -125,10 +125,8 @@ Proof. by rewrite [@fun_of_perm]unlock. Qed.
 Lemma permE f f_inj : @perm T f f_inj =1 f.
 Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed.
 
-Lemma perm_inj s : injective s.
+Lemma perm_inj {s} : injective s.
 Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed.
-
-Arguments perm_inj : clear implicits.
 Hint Resolve perm_inj : core.
 
 Lemma perm_onto s : codom s =i predT.
@@ -141,7 +139,7 @@ Proof. by move=> x /=; rewrite f_iinv. Qed.
 
 Definition perm_inv s := perm (can_inj (perm_invK s)).
 
-Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)).
+Definition perm_mul s t := perm (inj_comp (@perm_inj t) (@perm_inj s)).
 
 Lemma perm_oneP : left_id perm_one perm_mul.
 Proof. by move=> s; apply/permP => x; rewrite permE /= permE. Qed.
@@ -191,7 +189,7 @@ Definition perm_on S : pred {perm T} := fun s => [pred x | s x != x] \subset S.
 Lemma perm_closed S s x : perm_on S s -> (s x \in S) = (x \in S).
 Proof.
 move/subsetP=> s_on_S; have [-> // | nfix_s_x] := eqVneq (s x) x.
-by rewrite !s_on_S // inE /= ?(inj_eq (perm_inj s)).
+by rewrite !s_on_S // inE /= ?(inj_eq perm_inj).
 Qed.
 
 Lemma perm_on1 H : perm_on H 1.
@@ -282,7 +280,11 @@ Qed.
 
 End Theory.
 
-Prenex Implicits tperm.
+Prenex Implicits tperm permK permKV tpermK.
+Arguments perm_inj {T s} [x1 x2] eq_sx12.
+
+(* Shorthand for using a permutation to reindex a bigop. *)
+Notation reindex_perm s := (reindex_inj (@perm_inj _ s)).
 
 Lemma inj_tperm (T T' : finType) (f : T -> T') x y z :
   injective f -> f (tperm x y z) = tperm (f x) (f y) (f z).
@@ -291,8 +293,7 @@ Proof. by move=> injf; rewrite !permE /= !(inj_eq injf) !(fun_if f). Qed.
 Lemma tpermJ (T : finType) x y (s : {perm T}) :
   (tperm x y) ^ s = tperm (s x) (s y).
 Proof.
-apply/permP => z; rewrite -(permKV s z) permJ; apply: inj_tperm.
-exact: perm_inj.
+by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj.
 Qed.
 
 Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
@@ -554,7 +555,7 @@ congr (_ (+) _); last first.
   elim: ts => [|t ts IHts] /=; first by rewrite big_nil lift_perm1 !odd_perm1.
   rewrite big_cons odd_mul_tperm -(lift_permM _ j) odd_permM {}IHts //.
   congr (_ (+) _); transitivity (tperm (lift j t.1) (lift j t.2)); last first.
-    by rewrite odd_tperm (inj_eq (@lift_inj _ _)).
+     by rewrite odd_tperm (inj_eq (pcan_inj (liftK j))).
   congr odd_perm; apply/permP=> k; case: (unliftP j k) => [k'|] ->.
     by rewrite lift_perm_lift inj_tperm //; apply: lift_inj.
   by rewrite lift_perm_id tpermD // eq_sym neq_lift.
@@ -576,5 +577,7 @@ Qed.
 
 End LiftPerm.
 
+Prenex Implicits lift_perm lift_permK.
+
 
 
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 97b2eba..61b0cd9 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -198,13 +198,14 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed.
 
 End Cosets.
 
-Arguments coset_of {_} _%g.
-Arguments coset {_} _%g _%g.
-Arguments quotient _ _%g _%g.
+Arguments coset_of {gT} H%g : rename.
+Arguments coset {gT} H%g x%g : rename.
+Arguments quotient {gT} A%g H%g : rename.
+Arguments coset_reprK {gT H%g} xbar%g : rename.
 
 Bind Scope group_scope with coset_of.
 
-Notation "A / B" := (quotient A B) : group_scope.
+Notation "A / H" := (quotient A H) : group_scope.
 
 Section CosetOfGroupTheory.
 
@@ -454,7 +455,7 @@ Proof. by rewrite /normal -{1}ker_coset; apply: morphim_injG. Qed.
 
 Lemma quotient_inj G1 G2 :
    H <| G1 -> H <| G2 -> G1 / H = G2 / H -> G1 :=: G2.
-Proof. by rewrite /normal -{1 3}ker_coset; apply: morphim_inj. Qed.
+Proof. by rewrite /normal -[in mem H]ker_coset; apply: morphim_inj. Qed.
 
 Lemma quotient_neq1 A : H <| A -> (A / H != 1) = (H \proper A).
 Proof.