Remove the use of [the _ of _] notations (#1430)

analysis_stdlib/showcase/uniform_bigO.v

@@ -33,7 +33,7 @@ Definition OuP (f : A -> R * R -> R) (g : R * R -> R) :=
 
 (* first we replace sig with ex and the l^2 norm with the l^oo norm *)
 
-Let normedR2 := [the normedModType _ of (R^o * R^o)%type].
+Let normedR2 : normedModType _ := (R^o * R^o)%type.
 
 Definition OuPex (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
   exists2 alp, 0 < alp & exists2 C, 0 < C &

classical/cardinality.v

@@ -1327,7 +1327,7 @@ Qed.
 HB.instance Definition _ aT rT x :=
   FiniteImage.Build aT rT (cst x) (@finite_image_cst aT rT x).
 
-Definition cst_fimfun {aT rT} x := [the {fimfun aT >-> rT} of cst x].
+Definition cst_fimfun {aT rT} x : {fimfun aT >-> rT} := cst x.
 
 Lemma fimfun_cst aT rT x : @cst_fimfun aT rT x =1 cst x. Proof. by []. Qed.
 

experimental_reals/discrete.v

@@ -169,7 +169,7 @@ Variables (T : eqType) (E F : pred T).
 Lemma countable_sub: {subset E <= F} -> countable F -> countable E.
 Proof.
 move=> le_EF [f g fgK]; pose f' (x : [psub E]) := f (pincl le_EF x).
-pose g' x := obind (insub (sT := [the subType _ of [psub E]])) (omap val (g x)).
+pose g' x := obind (insub (sT := [psub E])) (omap val (g x)).
 by exists f' g' => x; rewrite /f' /g' fgK /= valK.
 Qed.
 End CountSub.

reals/prodnormedzmodule.v

@@ -57,8 +57,7 @@ Proof. by rewrite /norm/= !normrN. Qed.
 HB.instance Definition _ := Num.Zmodule_isNormed.Build R (U * V)%type
   normD norm_eq0 normMn normrN.
 
-Lemma prod_normE (x : [the normedZmodType R of (U * V)%type]) :
-  `|x| = Num.max `|x.1| `|x.2|.
+Lemma prod_normE (x : U * V) : `|x| = Num.max `|x.1| `|x.2|.
 Proof. by []. Qed.
 
 End ProdNormedZmodule.

reals/reals.v

@@ -116,9 +116,9 @@ End has_bound_lemmas.
 (* -------------------------------------------------------------------- *)
 
 HB.mixin Record ArchimedeanField_isReal R of Num.ArchiField R := {
-  sup_upper_bound_subdef : forall E : set [the archiFieldType of R],
+  sup_upper_bound_subdef : forall E : set R,
     has_sup E -> ubound E (supremum 0 E) ;
-  sup_adherent_subdef : forall (E : set [the archiFieldType of R]) (eps : R),
+  sup_adherent_subdef : forall (E : set R) (eps : R),
     0 < eps -> has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e
 }.
 

reals_stdlib/Rstruct.v

@@ -250,8 +250,7 @@ Qed.
 
 HB.instance Definition _ := Order.POrder_isTotal.Build _ R R_total.
 
-Lemma Rarchimedean_axiom :
-  Num.archimedean_axiom [the numDomainType of R : Type].
+Lemma Rarchimedean_axiom : Num.archimedean_axiom R.
 Proof.
 move=> x; exists (Z.abs_nat (up x) + 2)%N.
 have [Hx1 Hx2]:= (archimed x).
@@ -269,7 +268,7 @@ apply/RltbP/Rabs_def1.
     apply/Rplus_le_compat_r/IHz; split; first exact: Zlt_le_weak.
     exact: Zlt_pred.
   apply: (Rle_trans _ (IZR 0)); first exact: IZR_le.
-  by apply/RlebP/(ler0n [the numDomainType of R : Type] (Z.abs_nat z)).
+  by apply/RlebP/(ler0n R (Z.abs_nat z)).
 apply: (Rlt_le_trans _ (IZR (up x) - 1)).
   apply: Ropp_lt_cancel; rewrite Ropp_involutive.
   rewrite Ropp_minus_distr /Rminus -opp_IZR -{2}(Z.opp_involutive (up x)).
@@ -287,7 +286,7 @@ apply: (Rlt_le_trans _ (IZR (up x) - 1)).
   rewrite mulrnDr; apply: (Rlt_le_trans _ 2).
     by rewrite -{1}[1]Rplus_0_r; apply/Rplus_lt_compat_l/Rlt_0_1.
   rewrite -[2]Rplus_0_l; apply: Rplus_le_compat_r.
-  by apply/RlebP/(ler0n [the numDomainType of R : Type] (Z.abs_nat _)).
+  by apply/RlebP/(ler0n R (Z.abs_nat _)).
 apply: Rminus_le.
 rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _).
 exact: Rle_minus.
@@ -334,8 +333,7 @@ have Hg: (fun x=> f x * f x ^+ n)%R =1 g.
 by apply: (continuity_eq Hg); exact: continuity_mult.
 Qed.
 
-Lemma Rreal_closed_axiom :
-  Num.real_closed_axiom [the numDomainType of R : Type].
+Lemma Rreal_closed_axiom : Num.real_closed_axiom R.
 Proof.
 move=> p a b; rewrite !le_eqVlt.
 case Hpa: ((p.[a])%R == 0%R).

theories/cantor.v

@@ -340,7 +340,7 @@ Lemma homeomorphism_cantor_like :
   exists f : {splitbij [set: cantor_space] >-> [set: T]},
     continuous f /\ (forall A, closed A -> closed (f @` A)).
 Proof.
-exists [the {splitbij _ >-> _} of tree_map] => /=.
+exists tree_map => /=.
 have [cts surj inje] := projT2 (cid cantor_map); split; first exact: cts.
 move=> A clA; apply: (compact_closed hsdfT).
 apply: (@continuous_compact _ _ tree_map); first exact: continuous_subspaceT.
@@ -527,7 +527,7 @@ have [//| | |? []//| |? []// | |] := @tree_map_props
   have [z [Dz DzE]] := Csub _ cbD.
   have /ent_closure := DzE _ Dx => /(_ (ent_count_unif n))/xsectionP/ctE [_ /= Exz].
   have /ent_closure := DzE _ Dy => /(_ (ent_count_unif n))/xsectionP/ctE [Ezy _].
-  exact: (@entourage_split _ (*[the uniformType of T]*) z).
+  exact: (@entourage_split T z).
 by move=> f [ctsf surjf _]; exists f.
 Qed.
 

theories/charge.v

@@ -520,8 +520,7 @@ Let mu0 : mu set0 = 0.
 Proof. by apply: measure0. Qed.
 
 HB.instance Definition _ := isCharge.Build _ _ _
-  mu (measure0 [the content _ _ of mu])
-    fin_num_measure measure_semi_sigma_additive.
+  mu (measure0 mu) fin_num_measure measure_semi_sigma_additive.
 
 HB.end.
 
@@ -917,8 +916,7 @@ Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed.
 
 Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed.
 
-Local Definition cjordan_pos : {charge set T -> \bar R} :=
-  [the charge _ _ of crestr0 nu mP].
+Local Definition cjordan_pos : {charge set T -> \bar R} := crestr0 nu mP.
 
 Lemma cjordan_posE A : cjordan_pos A = crestr0 nu mP A.
 Proof. by []. Qed.
@@ -944,7 +942,7 @@ HB.instance Definition _ := @Measure_isFinite.Build _ _ _
   jordan_pos finite_jordan_pos.
 
 Local Definition cjordan_neg : {charge set T -> \bar R} :=
-  [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]].
+  cscale (-1) (crestr0 nu mN).
 
 Lemma cjordan_negE A : cjordan_neg A = - crestr0 nu mN A.
 Proof. by rewrite /= /cscale/= EFinN mulN1e. Qed.
@@ -970,8 +968,7 @@ HB.instance Definition _ := @Measure_isFinite.Build _ _ _
   jordan_neg finite_jordan_neg.
 
 Lemma jordan_decomp (A : set T) : measurable A ->
-  nu A = (cadd [the charge _ _ of jordan_pos]
-           ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A.
+  nu A = cadd jordan_pos (cscale (-1) jordan_neg) A.
 Proof.
 move=> mA.
 rewrite /cadd cjordan_posE /= /cscale EFinN mulN1e cjordan_negE oppeK.
@@ -1684,8 +1681,7 @@ move=> nu_mu; exists f; split.
   - by apply/integrableP; split; [exact: mf|exact: int_fRN_lty].
 move=> // A mA.
 apply/eqP; rewrite eq_le int_fRN_ub// andbT leNgt; apply/negP => abs.
-pose sigma : {charge set T -> \bar R} :=
-  [the {charge set T -> \bar R} of sigmaRN mA abs].
+pose sigma : {charge set T -> \bar R} := sigmaRN mA abs.
 have [P [N [[mP posP] [mN negN] PNX PN0]]] := Hahn_decomposition sigma.
 pose AP := A `&` P.
 have mAP : measurable AP by exact: measurableI.
@@ -1781,11 +1777,9 @@ have muEoo k : mu (E k) < +oo.
   by rewrite (le_lt_trans _ (muFoo k))// le_measure ?inE//; exact: subDsetl.
 have UET : \bigcup_i E i = [set: T] by rewrite TF [RHS]seqDU_bigcup_eq.
 have tE := trivIset_seqDU F.
-pose mu_ j : {finite_measure set T -> \bar R} :=
-  [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (muEoo j)].
+pose mu_ j : {finite_measure set T -> \bar R} := mfrestr (mE j) (muEoo j).
 have nuEoo i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure.
-pose nu_ j : {finite_measure set T -> \bar R} :=
-  [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (nuEoo j)].
+pose nu_ j : {finite_measure set T -> \bar R} := mfrestr (mE j) (nuEoo j).
 have nu_mu_ k : nu_ k `<< mu_ k.
   by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI.
 have [g_] := choice (fun j => radon_nikodym_finite (nu_mu_ j)).
@@ -2034,11 +2028,9 @@ Local Lemma Radon_Nikodym0 : nu `<< mu ->
 Proof.
 move=> nu_mu; have [P [N nuPN]] := Hahn_decomposition nu.
 have [fp [fp0 fpfin intfp fpE]] := @radon_nikodym_sigma_finite _ _ _ mu
-  [the {finite_measure set _ -> \bar _} of jordan_pos nuPN]
-  (jordan_pos_dominates nuPN nu_mu).
+  (jordan_pos nuPN) (jordan_pos_dominates nuPN nu_mu).
 have [fn [fn0 fnfin intfn fnE]] := @radon_nikodym_sigma_finite _ _ _ mu
-  [the {finite_measure set _ -> \bar _} of jordan_neg nuPN]
-  (jordan_neg_dominates nuPN nu_mu).
+  (jordan_neg nuPN) (jordan_neg_dominates nuPN nu_mu).
 exists (fp \- fn); split; first by move=> x; rewrite fin_numB// fpfin fnfin.
   exact: integrableB.
 move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//;
@@ -2091,7 +2083,7 @@ Implicit Types f : T -> \bar R.
 
 Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E ->
   ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu)
-             ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu).
+             ('d (charge_of_finite_measure nu) '/d mu).
 Proof.
 move=> mE; apply: integral_ae_eq => //.
 - apply: (integrableS measurableT) => //.
@@ -2103,8 +2095,7 @@ Qed.
 
 Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
     nu.-integrable E f ->
-  \int[mu]_(x in E)
-    (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) =
+  \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) =
   \int[nu]_(x in E) f x.
 Proof.
 move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first.
@@ -2140,8 +2131,7 @@ Implicit Types (nu : {charge set T -> \bar R})
                (mu : {sigma_finite_measure set T -> \bar R}).
 
 Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu ->
-  ae_eq mu E ('d [the charge _ _ of cscale c nu] '/d mu)
-             (fun x => c%:E * 'd nu '/d mu x).
+  ae_eq mu E ('d (cscale c nu) '/d mu) (fun x => c%:E * 'd nu '/d mu x).
 Proof.
 move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA].
 - apply: (integrableS measurableT) => //.
@@ -2155,8 +2145,7 @@ Qed.
 
 Lemma Radon_Nikodym_cadd mu nu0 nu1 E : measurable E ->
   nu0 `<< mu -> nu1 `<< mu ->
-  ae_eq mu E ('d [the charge _ _ of cadd nu0 nu1] '/d mu)
-             ('d nu0 '/d mu \+ 'd nu1 '/d mu).
+  ae_eq mu E ('d (cadd nu0 nu1) '/d mu) ('d nu0 '/d mu \+ 'd nu1 '/d mu).
 Proof.
 move=> mE nu0mu nu1mu; apply: integral_ae_eq => [//| | |A AE mA].
 - apply: (integrableS measurableT) => //.
@@ -2177,8 +2166,7 @@ Variables (nu : {charge set T -> \bar R})
 
 Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la ->
   ae_eq la setT ('d nu '/d la)
-                ('d nu '/d mu \*
-                  'd [the charge _ _ of charge_of_finite_measure mu] '/d la).
+                ('d nu '/d mu \* 'd (charge_of_finite_measure mu) '/d la).
 Proof.
 have [Pnu [Nnu nuPN]] := Hahn_decomposition nu.
 move=> numu mula; have nula := measure_dominates_trans numu mula.

theories/derive.v

@@ -671,7 +671,7 @@ Qed.
 Global Instance is_diff_scalel (k : R) (x : V) :
   is_diff k ( *:%R ^~ x) ( *:%R ^~ x).
 Proof.
-have sx_lin : linear ( *:%R ^~ x : [the lmodType R of R : Type] -> _).
+have sx_lin : linear ( *:%R ^~ x : R -> _).
   by move=> u y z; rewrite scalerDl scalerA.
 pose sxlM := GRing.isLinear.Build _ _ _ _ _ sx_lin.
 pose sxL : {linear _ -> _} := HB.pack ( *:%R ^~ x) sxlM.

theories/forms.v

@@ -200,8 +200,7 @@ Qed.
 
 HB.instance Definition _ (R : comRingType) m n p :=
   bilinear_isBilinear.Build R
-    [the lmodType R of 'M[R]_(m, n)] [the lmodType R of 'M[R]_(n, p)]
-    [the zmodType of 'M[R]_(m, p)] _ _ (@mulmx R m n p)
+    'M[R]_(m, n) 'M[R]_(n, p) 'M[R]_(m, p) _ _ (@mulmx R m n p)
     (mulmx_is_bilinear R m n p).
 
 (* Section classfun. *)

theories/function_spaces.v

@@ -124,20 +124,19 @@ Variable I : Type.
 
 Definition product_topology_def (T : I -> topologicalType) :=
   sup_topology (fun i => Topological.class
-    (weak_topology (fun f : [the choiceType of forall i, T i] => f i))).
+    (weak_topology (fun f : (forall i, T i) => f i))).
 
 HB.instance Definition _ (T : I -> topologicalType) :=
   Topological.copy (prod_topology T) (product_topology_def T).
 
 HB.instance Definition _ (T : I -> uniformType) :=
   Uniform.copy (prod_topology T)
-    (sup_topology (fun i => Uniform.class
-      [the uniformType of weak_topology (@proj _ T i)])).
+    (sup_topology (fun i => Uniform.class (weak_topology (@proj _ T i)))).
 
 HB.instance Definition _ (R : realType) (Ii : countType)
     (Tc : Ii -> pseudoMetricType R) := PseudoMetric.copy (prod_topology Tc)
-  (sup_pseudometric (fun i => PseudoMetric.class
-     [the pseudoMetricType R of weak_topology (@proj _ Tc i)]) (countableP _)).
+  (sup_pseudometric (fun i => PseudoMetric.class (weak_topology (@proj _ Tc i)))
+    (countableP _)).
 
 End Product_Topology.
 
@@ -327,10 +326,10 @@ Definition separate_points_from_closed := forall (U : set T) x,
 Hypothesis sepf : separate_points_from_closed.
 Hypothesis ctsf : forall i, continuous (f_ i).
 
-Let weakT := [the topologicalType of
-  sup_topology (fun i => Topological.on (weak_topology (f_ i)))].
+Let weakT : topologicalType :=
+  sup_topology (fun i => Topological.on (weak_topology (f_ i))).
 
-Let PU := [the topologicalType of prod_topology U_].
+Let PU : topologicalType := prod_topology U_.
 
 Local Notation sup_open := (@open weakT).
 Local Notation "'weak_open' i" := (@open weakT) (at level 0).
@@ -660,7 +659,7 @@ by move: rBrE; rewrite eqEsubset; case => [+ _]; apply; exists g.
 Unshelve. all: by end_near. Qed.
 
 Lemma uniform_entourage :
-  @entourage [the uniformType of {uniform` A -> V}] =
+  @entourage {uniform` A -> V} =
   filter_from
     (@entourage V)
     (fun P => [set fg | forall t : U, A t -> P (fg.1 t, fg.2 t)]).
@@ -698,7 +697,7 @@ Notation "{ 'family' fam , F --> f }" :=
 HB.instance Definition _ {U : choiceType} {V : uniformType}
     (fam : set U -> Prop) :=
   Uniform.copy {family fam, U -> V} (sup_topology (fun k : sigT fam =>
-       Uniform.class [the uniformType of {uniform` projT1 k -> V}])).
+       Uniform.class {uniform` projT1 k -> V})).
 
 Section UniformCvgLemmas.
 Context {U : choiceType} {V : uniformType}.

theories/hoelder.v

@@ -104,7 +104,7 @@ Section lnorm.
 (* l-norm is just L-norm applied to counting *)
 Context d {T : measurableType d} {R : realType}.
 Local Open Scope ereal_scope.
-Local Notation "'N_ p [ f ]" := (Lnorm [the measure _ _ of counting] p f).
+Local Notation "'N_ p [ f ]" := (Lnorm counting p f).
 
 Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R ->
   'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
@@ -263,7 +263,7 @@ Proof.
 move=> a10 a20 b10 b20 p0 q0 pq.
 pose f a b n : R := match n with 0%nat => a | 1%nat => b | _ => 0 end.
 have mf a b : measurable_fun setT (f a b) by [].
-have := hoelder [the measure _ _ of counting] (mf a1 a2) (mf b1 b2) p0 q0 pq.
+have := hoelder counting (mf a1 a2) (mf b1 b2) p0 q0 pq.
 rewrite !Lnorm_counting//.
 rewrite (nneseries_split 0 2); last by move=> k; rewrite lee_fin powR_ge0.
 rewrite add0n ereal_series_cond eseries0 ?adde0; last first.