Adjust implicits of cancellation lemmas

Like injectivity lemmas, instances of cancellation lemmas (whose
conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or
`ocancel`) are passed to
generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should
not have trailing on-demand implicits _just before_ the `cancel`
conclusion, as these would be inconvenient to insert (requiring
essentially an explicit eta-expansion).
We therefore use `Arguments` or `Prenex Implicits` directives to make
all such arguments maximally inserted implicits. We don’t, however make
other arguments implicit, so as not to spoil direct instantiation of
the lemmas (in, e.g., `rewrite -[y](invmK injf)`).
We have also tried to do this with lemmas whose statement matches a
`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern
unification will pick up `f = fun x => E[x]`).
We also adjusted implicits of a few stray injectivity
lemmas, and defined constants.
We provide a shorthand for reindexing a bigop with a permutation.
Finally we used the new implicit signatures to simplify proofs that
use injectivity or cancellation lemmas.

9 files changed, 91 insertions, 63 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 2f5e844..1da8313 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -714,7 +714,7 @@ rewrite mul1n; apply/dvdn_biggcdP/(all_nthP 0)=> a_dv_p i ltip /=.
 exact: a_dv_p.
 Qed.
 
-Lemma map_poly_divzK a p :
+Lemma map_poly_divzK {a} p :
   p \is a polyOver (dvdz a) -> a *: map_poly (divz^~ a) p = p.
 Proof.
 move/polyOverP=> a_dv_p; apply/polyP=> i.
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 3fe8d01..3b12802 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -916,9 +916,10 @@ Arguments row_mxA {R m n1 n2 n3 A1 A2 A3}.
 Arguments col_mxA {R m1 m2 m3 n A1 A2 A3}.
 Arguments block_mxA
   {R m1 m2 m3 n1 n2 n3 A11 A12 A13 A21 A22 A23 A31 A32 A33}.
-Prenex Implicits castmx trmx lsubmx rsubmx usubmx dsubmx row_mx col_mx.
+Prenex Implicits castmx trmx trmxK lsubmx rsubmx usubmx dsubmx row_mx col_mx.
 Prenex Implicits block_mx ulsubmx ursubmx dlsubmx drsubmx.
 Prenex Implicits mxvec vec_mx mxvec_indexP mxvecK vec_mxK.
+Arguments trmx_inj {R m n} [A1 A2] eqA12t : rename.
 
 Notation "A ^T" := (trmx A) : ring_scope.
 
@@ -1031,6 +1032,8 @@ End Block.
 
 End MapMatrix.
 
+Arguments map_mx {aT rT} f {m n} A.
+
 (*****************************************************************************)
 (********************* Matrix Zmodule (additive) structure *******************)
 (*****************************************************************************)
@@ -1180,9 +1183,7 @@ Qed.
 
 Lemma col_mx_eq0 (m1 m2 n : nat) (A1 : 'M_(m1, n)) (A2 : 'M_(m2, n)):
   (col_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0).
-Proof.
-by rewrite -![_ == 0](inj_eq (@trmx_inj _ _ _)) !trmx0 tr_col_mx row_mx_eq0.
-Qed.
+Proof. by rewrite -![_ == 0](inj_eq trmx_inj) !trmx0 tr_col_mx row_mx_eq0. Qed.
 
 Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) :
   (block_mx Aul Aur Adl Adr == 0) =
@@ -1332,29 +1333,29 @@ Proof. by rewrite {1}[u]matrix_sum_delta big_ord1. Qed.
 Lemma delta_mx_lshift m n1 n2 i j :
   delta_mx i (lshift n2 j) = row_mx (delta_mx i j) 0 :> 'M_(m, n1 + n2).
 Proof.
-apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)).
-by rewrite (unsplitK (inl _ _)); case: split => ?; rewrite mxE ?andbF.
+apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inl _ _)).
+by case: split => ?; rewrite mxE ?andbF.
 Qed.
 
 Lemma delta_mx_rshift m n1 n2 i j :
   delta_mx i (rshift n1 j) = row_mx 0 (delta_mx i j) :> 'M_(m, n1 + n2).
 Proof.
-apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)).
-by rewrite (unsplitK (inr _ _)); case: split => ?; rewrite mxE ?andbF.
+apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inr _ _)).
+by case: split => ?; rewrite mxE ?andbF.
 Qed.
 
 Lemma delta_mx_ushift m1 m2 n i j :
   delta_mx (lshift m2 i) j = col_mx (delta_mx i j) 0 :> 'M_(m1 + m2, n).
 Proof.
-apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)).
-by rewrite (unsplitK (inl _ _)); case: split => ?; rewrite mxE.
+apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inl _ _)).
+by  case: split => ?; rewrite mxE.
 Qed.
 
 Lemma delta_mx_dshift m1 m2 n i j :
   delta_mx (rshift m1 i) j = col_mx 0 (delta_mx i j) :> 'M_(m1 + m2, n).
 Proof.
-apply/matrixP=> i' j'; rewrite !mxE -(can_eq (@splitK _ _)).
-by rewrite (unsplitK (inr _ _)); case: split => ?; rewrite mxE.
+apply/matrixP=> i' j'; rewrite !mxE -(can_eq splitK) (unsplitK (inr _ _)).
+by case: split => ?; rewrite mxE.
 Qed.
 
 Lemma vec_mx_delta m n i j :
@@ -1628,7 +1629,7 @@ Qed.
 Lemma mul_col_perm m n p s (A : 'M_(m, n)) (B : 'M_(n, p)) :
   col_perm s A *m B = A *m row_perm s^-1 B.
 Proof.
-apply/matrixP=> i k; rewrite !mxE (reindex_inj (@perm_inj _ s^-1)).
+apply/matrixP=> i k; rewrite !mxE (reindex_perm s^-1).
 by apply: eq_bigr => j _ /=; rewrite !mxE permKV.
 Qed.
 
@@ -2013,7 +2014,7 @@ Lemma lift0_mx_perm s : lift0_mx (perm_mx s) = perm_mx (lift0_perm s).
 Proof.
 apply/matrixP=> /= i j; rewrite !mxE split1 /=; case: unliftP => [i'|] -> /=.
   rewrite lift0_perm_lift !mxE split1 /=.
-  by case: unliftP => [j'|] ->; rewrite ?(inj_eq (@lift_inj _ _)) /= !mxE.
+  by case: unliftP => [j'|] ->; rewrite ?(inj_eq (lift_inj _)) /= !mxE.
 rewrite lift0_perm0 !mxE split1 /=.
 by case: unliftP => [j'|] ->; rewrite /= mxE.
 Qed.
@@ -2142,7 +2143,7 @@ Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n.
 Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed.
 
 Lemma map_mx_is_multiplicative n' (n := n'.+1) :
-  multiplicative ((map_mx f) n n).
+  multiplicative (map_mx f : 'M_n -> 'M_n).
 Proof. by split; [apply: map_mxM | apply: map_mx1]. Qed.
 
 Canonical map_mx_rmorphism n' := AddRMorphism (map_mx_is_multiplicative n').
@@ -2291,14 +2292,14 @@ rewrite [\det A](bigID (@odd_perm _)) /=.
 apply: canLR (subrK _) _; rewrite add0r -sumrN.
 rewrite (reindex_inj (mulgI t)); apply: eq_big => //= s.
 rewrite oddMt => /negPf->; rewrite mulN1r mul1r; congr (- _).
-rewrite (reindex_inj (@perm_inj _ t)); apply: eq_bigr => /= i _.
+rewrite (reindex_perm t); apply: eq_bigr => /= i _.
 by rewrite permM tpermK /t; case: tpermP => // ->; rewrite eqA12.
 Qed.
 
 Lemma det_tr n (A : 'M[R]_n) : \det A^T = \det A.
 Proof.
-rewrite [\det A^T](reindex_inj (@invg_inj _)) /=.
-apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_inj (@perm_inj _ s)) /=.
+rewrite [\det A^T](reindex_inj invg_inj) /=.
+apply: eq_bigr => s _ /=; rewrite !odd_permV (reindex_perm s) /=.
 by congr (_ * _); apply: eq_bigr => i _; rewrite mxE permK.
 Qed.
 
@@ -2349,7 +2350,7 @@ rewrite (bigID (fun f : F => injectiveb f)) /= addrC big1 ?add0r => [|f Uf].
   rewrite (reindex_inj (mulgI s)); apply: eq_bigr => t _ /=.
   rewrite big_split /= mulrA mulrCA mulrA mulrCA mulrA.
   rewrite -signr_addb odd_permM !pvalE; congr (_ * _); symmetry.
-  by rewrite (reindex_inj (@perm_inj _ s)); apply: eq_bigr => i; rewrite permM.
+  by rewrite (reindex_perm s); apply: eq_bigr => i; rewrite permM.
 transitivity (\det (\matrix_(i, j) B (f i) j) * \prod_i A i (f i)).
   rewrite mulrC big_distrr /=; apply: eq_bigr => s _.
   rewrite mulrCA big_split //=; congr (_ * (_ * _)).
@@ -2382,7 +2383,7 @@ rewrite (reindex (lift_perm i0 j0)); last first.
   pose ulsf i (s : 'S_n.+1) k := odflt k (unlift (s i) (s (lift i k))).
   have ulsfK i (s : 'S_n.+1) k: lift (s i) (ulsf i s k) = s (lift i k).
     rewrite /ulsf; have:= neq_lift i k.
-    by rewrite -(inj_eq (@perm_inj _ s)) => /unlift_some[] ? ? ->.
+    by rewrite -(can_eq (permK s)) => /unlift_some[] ? ? ->.
   have inj_ulsf: injective (ulsf i0 _).
     move=> s; apply: can_inj (ulsf (s i0) s^-1%g) _ => k'.
     by rewrite {1}/ulsf ulsfK !permK liftK.
@@ -2497,8 +2498,8 @@ Proof. by rewrite -det_tr tr_block_mx trmx0 det_ublock !det_tr. Qed.
 
 End ComMatrix.
 
-Arguments lin_mul_row {R m n}.
-Arguments lin_mulmx {R m n p}.
+Arguments lin_mul_row {R m n} u.
+Arguments lin_mulmx {R m n p} A.
 
 Canonical matrix_finAlgType (R : finComRingType) n' :=
   [finAlgType R of 'M[R]_n'.+1].
@@ -2642,7 +2643,7 @@ Qed.
 
 End MatrixInv.
 
-Prenex Implicits unitmx invmx.
+Prenex Implicits unitmx invmx invmxK.
 
 Canonical matrix_countUnitRingType (R : countComUnitRingType) n :=
   [countUnitRingType of 'M[R]_n.+1].
@@ -2790,7 +2791,7 @@ Section MapFieldMatrix.
 Variables (aF : fieldType) (rF : comUnitRingType) (f : {rmorphism aF -> rF}).
 Local Notation "A ^f" := (map_mx f A) : ring_scope.
 
-Lemma map_mx_inj m n : injective ((map_mx f) m n).
+Lemma map_mx_inj {m n} : injective (map_mx f : 'M_(m, n) -> 'M_(m, n)).
 Proof.
 move=> A B eq_AB; apply/matrixP=> i j.
 by move/matrixP/(_ i j): eq_AB; rewrite !mxE; apply: fmorph_inj.
@@ -2811,7 +2812,7 @@ Proof. exact: map_unitmx. Qed.
 
 Lemma map_invmx n (A : 'M_n) : (invmx A)^f = invmx A^f.
 Proof.
-rewrite /invmx map_unitmx (fun_if ((map_mx f) n n)).
+rewrite /invmx map_unitmx (fun_if (map_mx f)).
 by rewrite map_mxZ map_mx_adj det_map_mx fmorphV.
 Qed.
 
@@ -2819,10 +2820,12 @@ Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1.
 Proof. exact: map_invmx. Qed.
   
 Lemma map_mx_eq0 m n (A : 'M_(m, n)) : (A^f == 0) = (A == 0).
-Proof. by rewrite -(inj_eq (@map_mx_inj m n)) raddf0. Qed.
+Proof. by rewrite -(inj_eq map_mx_inj) raddf0. Qed.
 
 End MapFieldMatrix.
 
+Arguments map_mx_inj {aF rF f m n} [A1 A2] eqA12f : rename.
+
 (*****************************************************************************)
 (****************************** LUP decomposion ******************************)
 (*****************************************************************************)
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index f679828..710adc6 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -29,7 +29,7 @@ Require Import poly polydiv.
 (*   char_poly A  == the characteristic polynomial of A.                      *)
 (* char_poly_mx A == a matrix whose determinant is char_poly A.               *)
 (*  companionmx p == a matrix whose char_poly is p                            *)
-(*   mxminpoly A  == the minimal polynomial of A, i.e., the smallest monic     *)
+(*   mxminpoly A  == the minimal polynomial of A, i.e., the smallest monic    *)
 (*                   polynomial that annihilates A (A must be nontrivial).    *)
 (* degree_mxminpoly A == the (positive) degree of mxminpoly A.                *)
 (* mx_inv_horner A == the inverse of horner_mx A for polynomials of degree    *)
@@ -116,8 +116,9 @@ Canonical rVpoly_linear := Linear rVpoly_is_linear.
 
 End RowPoly.
 
+Prenex Implicits rVpoly rVpolyK.
 Arguments poly_rV {R d}.
-Prenex Implicits rVpoly.
+Arguments poly_rV_K {R d} [p] le_p_d.
 
 Section Resultant.
 
@@ -140,6 +141,8 @@ Definition resultant := \det Sylvester_mx.
 
 End Resultant.
 
+Prenex Implicits Sylvester_mx resultant.
+
 Lemma resultant_in_ideal (R : comRingType) (p q : {poly R}) :
     size p > 1 -> size q > 1 ->
   {uv : {poly R} * {poly R} | size uv.1 < size q /\ size uv.2 < size p
@@ -224,7 +227,7 @@ apply/det0P/idP=> [[uv nz_uv] | r_nonC].
   rewrite addrC addr_eq0 => /eqP vq_up.
   have nz_v: v != 0.
     apply: contraNneq nz_uv => v0; apply/eqP.
-    congr row_mx; apply: (can_inj (@rVpolyK _ _)); rewrite linear0 // -/u.
+    congr row_mx; apply: (can_inj rVpolyK); rewrite linear0 // -/u.
     by apply: contra_eq vq_up; rewrite v0 mul0r -addr_eq0 add0r => /mulf_neq0->.
   have r_nz: r != 0 := dvdpN0 r_p p_nz.
   have /dvdpP [[c w] /= nz_c wv]: v %| m by rewrite dvdp_gcd !dvdp_mulr.
@@ -298,6 +301,8 @@ Qed.
 
 End HornerMx.
 
+Prenex Implicits horner_mx powers_mx.
+
 Section CharPoly.
 
 Variables (R : ringType) (n : nat) (A : 'M[R]_n).
@@ -330,7 +335,7 @@ apply: leq_trans (_ : #|[pred j | s j == j]|.+1 <= n.-1).
   by rewrite sub0r size_opp size_polyC leq_b1.
 rewrite -{8}[n]card_ord -(cardC (pred2 (s i) i)) card2 nfix_i !ltnS.
 apply: subset_leq_card; apply/subsetP=> j; move/(_ =P j)=> fix_j.
-rewrite !inE -{1}fix_j (inj_eq (@perm_inj _ s)) orbb.
+rewrite !inE -{1}fix_j (inj_eq perm_inj) orbb.
 by apply: contraNneq nfix_i => <-; rewrite fix_j.
 Qed.
 
@@ -373,6 +378,8 @@ Qed.
 
 End CharPoly.
 
+Prenex Implicits char_poly_mx char_poly.
+
 Lemma mx_poly_ring_isom (R : ringType) n' (n := n'.+1) :
   exists phi : {rmorphism 'M[{poly R}]_n -> {poly 'M[R]_n}},
   [/\ bijective phi,
@@ -431,13 +438,11 @@ rewrite (big_morph _ (fun p q => hornerM p q a) (hornerC 1 a)).
 by apply: eq_bigr => i _; rewrite !mxE !(hornerE, hornerMn).
 Qed.
 
-Section Companion.
-
-Definition companionmx (R : ringType) (p : seq R) (d := (size p).-1) :=
+Definition companionmx {R : ringType} (p : seq R) (d := (size p).-1) :=
   \matrix_(i < d, j < d)
     if (i == d.-1 :> nat) then - p`_j else (i.+1 == j :> nat)%:R.
 
-Lemma companionmxK (R : comRingType) (p : {poly R}) :
+Lemma companionmxK {R : comRingType} (p : {poly R}) :
    p \is monic -> char_poly (companionmx p) = p.
 Proof.
 pose D n : 'M[{poly R}]_n := \matrix_(i, j)
@@ -487,8 +492,6 @@ rewrite ltn_eqF ?big1 ?addr0 1?eq_sym //; last first.
 by move=> k /negPf ki_eqF; rewrite !mxE eqxx ki_eqF mul0r.
 Qed.
 
-End Companion.
-
 Section MinPoly.
 
 Variables (F : fieldType) (n' : nat).
@@ -601,10 +604,10 @@ Qed.
 Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p.
 Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed.
 
-Lemma horner_rVpoly_inj : @injective 'M_n 'rV_d (horner_mx A \o rVpoly).
+Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n).
 Proof.
-apply: can_inj (poly_rV \o mx_inv_horner) _ => u.
-by rewrite /= horner_rVpolyK rVpolyK.
+apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=.
+by rewrite horner_rVpolyK rVpolyK.
 Qed.
 
 Lemma mxminpoly_linear_is_scalar : (d <= 1) = is_scalar_mx A.
@@ -639,6 +642,11 @@ Qed.
 
 End MinPoly.
 
+Prenex Implicits degree_mxminpoly mxminpoly mx_inv_horner.
+
+Arguments mx_inv_hornerK {F n' A} [B] AnB.
+Arguments horner_rVpoly_inj {F n' A} [u1 u2] eq_u12A : rename.
+          
 (* Parametricity. *)
 Section MapRingMatrix.
 
@@ -1044,9 +1052,9 @@ Local Notation holds := GRing.holds.
 Local Notation qf_form := GRing.qf_form.
 Local Notation qf_eval := GRing.qf_eval.
 
-Definition eval_mx (e : seq F) := map_mx (eval e).
+Definition eval_mx (e : seq F) := @map_mx term F (eval e).
 
-Definition mx_term := map_mx (@GRing.Const F).
+Definition mx_term := @map_mx F term GRing.Const.
 
 Lemma eval_mx_term e m n (A : 'M_(m, n)) : eval_mx e (mx_term A) = A.
 Proof. by apply/matrixP=> i j; rewrite !mxE. Qed.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 929c313..702dfc4 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -142,8 +142,8 @@ Definition coefp_head h i (p : poly_of (Phant R)) := let: tt := h in p`_i.
 
 End Polynomial.
 
-(* We need to break off the section here to let the argument scope *)
-(* directives take effect.                                         *)
+(* We need to break off the section here to let the Bind Scope directives     *)
+(* take effect.                                                               *)
 Bind Scope ring_scope with poly_of.
 Bind Scope ring_scope with polynomial.
 Arguments polyseq {R} p%R.
@@ -1675,7 +1675,7 @@ Qed.
 
 End PolynomialTheory.
 
-Prenex Implicits polyC Poly lead_coef root horner polyOver.
+Prenex Implicits polyC polyCK Poly polyseqK lead_coef root horner polyOver.
 Arguments monic {R}.
 Notation "\poly_ ( i < n ) E" := (poly n (fun i => E)) : ring_scope.
 Notation "c %:P" := (polyC c) : ring_scope.
@@ -1694,6 +1694,7 @@ Arguments rootPf {R p x}.
 Arguments rootPt {R p x}.
 Arguments unity_rootP {R n z}.
 Arguments polyOverP {R S0 addS kS p}.
+Arguments polyC_inj {R} [x1 x2] eq_x12P.
 
 Canonical polynomial_countZmodType (R : countRingType) :=
   [countZmodType of polynomial R].
@@ -1947,7 +1948,7 @@ Definition comp_poly q p := p^:P.[q].
 Local Notation "p \Po q" := (comp_poly q p) : ring_scope.
 
 Lemma size_map_polyC p : size p^:P = size p.
-Proof. exact: size_map_inj_poly (@polyC_inj R) _ _. Qed.
+Proof. exact/(size_map_inj_poly polyC_inj). Qed.
 
 Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0).
 Proof. by rewrite -!size_poly_eq0 size_map_polyC. Qed.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 40a1f83..47cee1f 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -875,6 +875,7 @@ End ZmoduleTheory.
 
 Arguments addrI {V} y [x1 x2].
 Arguments addIr {V} x [x1 x2].
+Arguments opprK {V}.
 Arguments oppr_inj {V} [x1 x2].
 
 Module Ring.
@@ -3031,6 +3032,7 @@ End ClosedPredicates.
 
 End UnitRingTheory.
 
+Arguments invrK {R}.
 Arguments invr_inj {R} [x1 x2].
 
 Section UnitRingMorphism.
@@ -5370,7 +5372,8 @@ Arguments addrI {V} y [x1 x2].
 Arguments addIr {V} x [x1 x2].
 Arguments subrI {V} y [x1 x2].
 Arguments subIr {V} x [x1 x2].
-Definition opprK := opprK.
+Definition opprK := @opprK.
+Arguments opprK {V}.
 Definition oppr_inj := @oppr_inj.
 Arguments oppr_inj {V} [x1 x2].
 Definition oppr0 := oppr0.
@@ -5554,7 +5557,8 @@ Definition divIr := divIr.
 Definition telescope_prodr := telescope_prodr.
 Definition commrV := commrV.
 Definition unitrE := unitrE.
-Definition invrK := invrK.
+Definition invrK := @invrK.
+Arguments invrK {R}.
 Definition invr_inj := @invr_inj.
 Arguments invr_inj {R} [x1 x2].
 Definition unitrV := unitrV.
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index b734ad7..e6b0264 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -290,7 +290,7 @@ Lemma mulz_addl : left_distributive mulz (+%R).
 Proof.
 move=> x y z; elim: z=> [|n|n]; first by rewrite !(mul0z,mulzC).
   by rewrite !mulzS=> ->; rewrite !addrA [X in X + _]addrAC.
-rewrite !mulzN !mulzS -!opprD=> /(inv_inj (@opprK _))->.
+rewrite !mulzN !mulzS -!opprD=> /oppr_inj->.
 by rewrite !addrA [X in X + _]addrAC.
 Qed.
 
@@ -330,22 +330,21 @@ Lemma mulVz : {in unitz, left_inverse 1%R invz *%R}.
 Proof. by move=> n /pred2P[] ->. Qed.
 
 Lemma mulzn_eq1 m (n : nat) : (m * n == 1) = (m == 1) && (n == 1%N).
-Proof. by case: m=> m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed.
+Proof. by case: m => m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed.
 
 Lemma unitzPl m n : n * m = 1 -> m \is a unitz.
 Proof.
-case: m => m; move/eqP; rewrite qualifE.
-* by rewrite mulzn_eq1; case/andP=> _; move/eqP->.
-* by rewrite NegzE intS mulrN -mulNr mulzn_eq1; case/andP=> _.
+rewrite qualifE => /eqP.
+by case: m => m; rewrite ?NegzE ?mulrN -?mulNr mulzn_eq1 => /andP[_ /eqP->].
 Qed.
 
-Lemma  invz_out : {in [predC unitz], invz =1 id}.
+Lemma invz_out : {in [predC unitz], invz =1 id}.
 Proof. exact. Qed.
 
 Lemma idomain_axiomz m n : m * n = 0 -> (m == 0) || (n == 0).
 Proof.
-by case: m n => m [] n //=; move/eqP; rewrite ?(NegzE,mulrN,mulNr);
-  rewrite ?(inv_eq (@opprK _)) -PoszM [_==_]muln_eq0.
+by case: m n => m [] n //= /eqP;
+  rewrite ?(NegzE, mulrN, mulNr) ?oppr_eq0 -PoszM [_ == _]muln_eq0.
 Qed.
 
 Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 2414e13..ec932a1 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1457,18 +1457,18 @@ Hint Resolve ltr_opp2 : core.
 Definition lter_opp2 := (ler_opp2, ltr_opp2).
 
 Lemma ler_oppr x y : (x <= - y) = (y <= - x).
-Proof. by rewrite (monoRL (@opprK _) ler_opp2). Qed.
+Proof. by rewrite (monoRL opprK ler_opp2). Qed.
 
 Lemma ltr_oppr x y : (x < - y) = (y < - x).
-Proof. by rewrite (monoRL (@opprK _) (lerW_nmono _)). Qed.
+Proof. by rewrite (monoRL opprK (lerW_nmono _)). Qed.
 
 Definition lter_oppr := (ler_oppr, ltr_oppr).
 
 Lemma ler_oppl x y : (- x <= y) = (- y <= x).
-Proof. by rewrite (monoLR (@opprK _) ler_opp2). Qed.
+Proof. by rewrite (monoLR opprK ler_opp2). Qed.
 
 Lemma ltr_oppl x y : (- x < y) = (- y < x).
-Proof. by rewrite (monoLR (@opprK _) (lerW_nmono _)). Qed.
+Proof. by rewrite (monoLR opprK (lerW_nmono _)). Qed.
 
 Definition lter_oppl := (ler_oppl, ltr_oppl).
 
@@ -4797,12 +4797,17 @@ Qed.
 
 End ClosedFieldTheory.
 
-Notation "n .-root" := (@nthroot _ n) (at level 2, format "n .-root") : ring_scope.
+Notation "n .-root" := (@nthroot _ n)
+  (at level 2, format "n .-root") : ring_scope.
 Notation sqrtC := 2.-root.
 Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.
 Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
 Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.
 
+Arguments conjCK {C} x.
+Arguments sqrCK {C} [x] le0x.
+Arguments sqrCK_P {C x}.
+
 End Theory.
 
 Module RealMixin.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index c4c62c3..4766c74 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1355,6 +1355,8 @@ Proof. by elim/big_rec2: _ => [|i _ f _ <-]; rewrite lfunE. Qed.
 
 End LfunZmodType.
 
+Arguments fun_of_lfunK {R aT rT}.
+
 Section LfunVectType.
 
 Variables (R : comRingType) (aT rT : vectType R).
@@ -1603,6 +1605,7 @@ Arguments lfunPn {K aT rT f g}.
 Arguments lker0P {K aT rT f}.
 Arguments eqlfunP {K aT rT f g v}.
 Arguments eqlfun_inP {K aT rT V f g}.
+Arguments limg_lfunVK {K aT rT f} [x] f_x.
 
 Section FixedSpace.
 
@@ -1718,6 +1721,8 @@ Qed.
 
 End LinearPreimage.
 
+Arguments lpreimK {K aT rT f} [W] fW.
+
 Section LfunAlgebra.
 (* This section is a bit of a place holder: the instances we build here can't *)
 (* be canonical because we are missing an interface for proper vectTypes,     *)
@@ -1944,7 +1949,7 @@ Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin.
 End SubVector.
 Prenex Implicits vsval vsproj vsvalK.
 Arguments subvs_inj {K vT U} [x1 x2].
-Arguments vsprojK {K vT U} [x].
+Arguments vsprojK {K vT U} [x] Ux.
 
 Section MatrixVectType.
 
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index ba6c1b3..5e931ef 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -180,7 +180,8 @@ End ZpDef.
 
 Arguments Zp0 {p'}.
 Arguments Zp1 {p'}.
-Arguments inZp {p'}.
+Arguments inZp {p'} i.
+Arguments valZpK {p'} x.
 
 Lemma ord1 : all_equal_to (0 : 'I_1).
 Proof. by case=> [[] // ?]; apply: val_inj. Qed.
@@ -259,6 +260,8 @@ Notation "''Z_' p" := 'I_(Zp_trunc p).+2
 Notation "''F_' p" := 'Z_(pdiv p)
   (at level 8, p at level 2, format "''F_' p") : type_scope.
 
+Arguments natr_Zp {p'} x.
+
 Section Groups.
 
 Variable p : nat.