diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v
index 58e6e9c5b..9ec3cd264 100644
--- a/analysis_stdlib/showcase/uniform_bigO.v
+++ b/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 &
diff --git a/classical/cardinality.v b/classical/cardinality.v
index c84602f5f..9b73d1de3 100644
--- a/classical/cardinality.v
+++ b/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.
 
diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v
index 029af438e..6e853ac32 100644
--- a/experimental_reals/discrete.v
+++ b/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.
diff --git a/reals/prodnormedzmodule.v b/reals/prodnormedzmodule.v
index 38bfe229c..ad613feb7 100644
--- a/reals/prodnormedzmodule.v
+++ b/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.
diff --git a/reals/reals.v b/reals/reals.v
index bc9d85ce1..2b1fd3ad1 100644
--- a/reals/reals.v
+++ b/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
 }.
 
diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v
index 4dbe8f0bf..998ed7690 100644
--- a/reals_stdlib/Rstruct.v
+++ b/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).
diff --git a/theories/cantor.v b/theories/cantor.v
index 8006e1ced..b40e5631f 100644
--- a/theories/cantor.v
+++ b/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.
 
diff --git a/theories/charge.v b/theories/charge.v
index 9754bc4af..f232b0381 100644
--- a/theories/charge.v
+++ b/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.
diff --git a/theories/derive.v b/theories/derive.v
index fc68330d6..c368957b0 100644
--- a/theories/derive.v
+++ b/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.
diff --git a/theories/forms.v b/theories/forms.v
index 7b7f2f732..92e9eb164 100644
--- a/theories/forms.v
+++ b/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. *)
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index cc56990f6..0f257a568 100644
--- a/theories/function_spaces.v
+++ b/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}.
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 346c0cb48..5b5b020f8 100644
--- a/theories/hoelder.v
+++ b/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.
diff --git a/theories/kernel.v b/theories/kernel.v
index 71c065e5a..31d8ba818 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -125,8 +125,7 @@ Section kseries.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable k : (R.-ker X ~> Y)^nat.
 
-Definition kseries : X -> {measure set Y -> \bar R} :=
-  fun x => [the measure _ _ of mseries (k ^~ x) 0].
+Definition kseries (x : X) : {measure set Y -> \bar R} := mseries (k ^~ x) 0.
 
 Lemma measurable_fun_kseries (U : set Y) :
   measurable U -> measurable_fun [set: X] (kseries ^~ U).
@@ -209,8 +208,7 @@ HB.factory Record Kernel_isFinite d d'
 Section kzero.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 
-Definition kzero : X -> {measure set Y -> \bar R} :=
-  fun _ : X => [the measure _ _ of mzero].
+Definition kzero (_ : X) : {measure set Y -> \bar R} := mzero.
 
 Let measurable_fun_kzero U : measurable U ->
   measurable_fun [set: X] (kzero ^~ U).
@@ -231,8 +229,7 @@ Let sfinite_finite :
   exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) &
     forall x U, measurable U -> k x U = mseries (k_ ^~ x) 0 U.
 Proof.
-exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else
-  [the _.-ker _ ~> _ of @kzero _ _ X Y R]).
+exists (fun n => if n is O return R.-ker X ~> Y then k else @kzero _ _ X Y R).
   by case => [|_]; [exact: measure_uub|exact: kzero_uub].
 move=> t U mU/=; rewrite /mseries.
 rewrite (nneseries_split _ 1%N)// big_mkord big_ord_recl/= big_ord0 adde0.
@@ -270,10 +267,7 @@ HB.instance Definition _ n := @Kernel_isFinite.Build d d' X Y R (s n) (s_uub n).
 
 Lemma sfinite_kernel : exists s : (R.-fker X ~> Y)^nat,
   forall x U, measurable U -> k x U = kseries s x U.
-Proof.
-exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU.
-by rewrite /s /= /s; by case: cid2 => ? ? ->.
-Qed.
+Proof. by exists s => x U mU; rewrite /s /= /s; case: cid2 => ? ? ->. Qed.
 
 End sfinite.
 
@@ -605,9 +599,8 @@ Section kdirac.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable f : X -> Y.
 
-Definition kdirac (mf : measurable_fun [set: X] f)
-    : X -> {measure set Y -> \bar R} :=
-  fun x => [the measure _ _ of dirac (f x)].
+Definition kdirac (mf : measurable_fun [set: X] f) (x : X) :
+  {measure set Y -> \bar R} := dirac (f x).
 
 Hypothesis mf : measurable_fun [set: X] f.
 
@@ -666,11 +659,10 @@ Section kadd.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variables k1 k2 : R.-ker X ~> Y.
 
-Definition kadd : X -> {measure set Y -> \bar R} :=
-  fun x => [the measure _ _ of measure_add (k1 x) (k2 x)].
+Definition kadd (x : X) : {measure set Y -> \bar R} :=
+  measure_add (k1 x) (k2 x).
 
-Let measurable_fun_kadd U : measurable U ->
-  measurable_fun [set: X] (kadd ^~ U).
+Let measurable_fun_kadd U : measurable U -> measurable_fun [set: X] (kadd ^~ U).
 Proof.
 move=> mU; rewrite /kadd.
 rewrite (_ : (fun _ => _) = (fun x => k1 x U + k2 x U)); last first.
@@ -692,7 +684,7 @@ Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat,
     kadd k1 k2 x U = mseries (k_ ^~ x) 0 U.
 Proof.
 have [f1 hk1] := sfinite_kernel k1; have [f2 hk2] := sfinite_kernel k2.
-exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]).
+exists (fun n => kadd (f1 n) (f2 n)).
   move=> n.
   have [r1 f1r1] := measure_uub (f1 n).
   have [r2 f2r2] := measure_uub (f2 n).
@@ -775,8 +767,7 @@ End knormalize.
 (* TODO: useful? *)
 Lemma measurable_fun_mnormalize d d' (X : measurableType d)
     (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
-  measurable_fun [set: X] (fun x =>
-    [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
+  measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R).
 Proof.
 apply: (@measurability _ _ _ _ _ _
   (@pset _ _ _ : set (set (pprobability Y R)))) => //.
@@ -807,7 +798,7 @@ Section kcomp_def.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).
 Variable l : X -> {measure set Y -> \bar R}.
-Variable k : (X * Y)%type -> {measure set Z -> \bar R}.
+Variable k : X * Y -> {measure set Z -> \bar R}.
 
 Definition kcomp x U := \int[l x]_y k (x, y) U.
 
@@ -816,8 +807,7 @@ End kcomp_def.
 Section kcomp_is_measure.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
  (Z : measurableType d3) (R : realType).
-Variable l : R.-ker X ~> Y.
-Variable k : R.-ker [the measurableType _ of X * Y] ~> Z.
+Variables (l : R.-ker X ~> Y) (k : R.-ker (X * Y) ~> Z).
 
 Let kcomp0 x : kcomp l k x set0 = 0.
 Proof.
@@ -841,8 +831,7 @@ Qed.
 HB.instance Definition _ x := isMeasure.Build _ _ R
   (kcomp l k x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x).
 
-Definition mkcomp : X -> {measure set Z -> \bar R} := fun x =>
-  [the measure _ _ of kcomp l k x].
+Definition mkcomp : X -> {measure set Z -> \bar R} := kcomp l k.
 
 End kcomp_is_measure.
 
@@ -853,7 +842,7 @@ Module KCOMP_FINITE_KERNEL.
 Section kcomp_finite_kernel_kernel.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y)
-  (k : R.-ker [the measurableType _ of X * Y] ~> Z).
+  (k : R.-ker (X * Y) ~> Z).
 
 Lemma measurable_fun_kcomp_finite U :
   measurable U -> measurable_fun [set: X] ((l \; k) ^~ U).
@@ -870,8 +859,7 @@ End kcomp_finite_kernel_kernel.
 Section kcomp_finite_kernel_finite.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType).
-Variable l : R.-fker X ~> Y.
-Variable k : R.-fker [the measurableType _ of X * Y] ~> Z.
+Variables (l : R.-fker X ~> Y) (k : R.-fker (X * Y) ~> Z).
 
 Let mkcomp_finite : measure_fam_uub (kcomp l k).
 Proof.
@@ -894,8 +882,7 @@ End KCOMP_FINITE_KERNEL.
 Section kcomp_sfinite_kernel.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType).
-Variable l : R.-sfker X ~> Y.
-Variable k : R.-sfker [the measurableType _ of X * Y] ~> Z.
+Variable (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y) ~> Z).
 
 Import KCOMP_FINITE_KERNEL.
 
@@ -907,11 +894,10 @@ have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U,
     \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i <oo) kl i x U.
   have /ppcard_eqP[f] : ([set: nat] #= [set: nat * nat])%card.
     by rewrite card_eq_sym; exact: card_nat2.
-  exists (fun i => [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U.
+  exists (fun i => l_ (f i).2 \; k_ (f i).1) => x U.
   by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true.
 exists kl => x U mU.
-transitivity (([the _.-ker _ ~> _ of kseries l_] \;
-               [the _.-ker _ ~> _ of kseries k_]) x U).
+transitivity ((kseries l_ \; kseries k_) x U).
   rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first.
     by move=> *; rewrite hl_.
   by apply: eq_integral => y _; rewrite hk_.
@@ -940,8 +926,7 @@ Module KCOMP_SFINITE_KERNEL.
 Section kcomp_sfinite_kernel.
 Context d d' d3 (X : measurableType d) (Y : measurableType d')
   (Z : measurableType d3) (R : realType).
-Variable l : R.-sfker X ~> Y.
-Variable k : R.-sfker [the measurableType _ of X * Y] ~> Z.
+Variables (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y) ~> Z).
 
 HB.instance Definition _ :=
   isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k).
@@ -986,8 +971,7 @@ Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) :
   (forall n r, measurable_fun [set: X] (l ^~ (k_ n @^-1` [set r]))) ->
   measurable_fun [set: X] (fun x => \int[l x]_z k z).
 Proof.
-move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l
-  (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=.
+move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l k_2) => /=.
 - by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_.
 - by move=> [x y]; exact: k_k.
 - move=> n r _ /= B mB.
@@ -1024,8 +1008,7 @@ End measurable_fun_integral_kernel.
 Section integral_kcomp.
 Context d d2 d3 (X : measurableType d) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).
-Variables (l : R.-sfker X ~> Y)
-          (k : R.-sfker [the measurableType _ of X * Y] ~> Z).
+Variables (l : R.-sfker X ~> Y) (k : R.-sfker (X * Y) ~> Z).
 
 Let integral_kcomp_indic x E (mE : measurable E) :
   \int[kcomp l k x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E).
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 5553c2ad2..dabbbcc8d 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -295,18 +295,18 @@ Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed.
 HB.instance Definition _ D mD := @isMeasurableFun.Build _ _ aT rT (mindic mD)
   (@measurable_indic _ aT rT setT D mD).
 
-Definition indic_mfun (D : set aT) (mD : measurable D) :=
-  [the {mfun aT >-> rT} of mindic mD].
+Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} :=
+  mindic mD.
 
 HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k).
-Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f].
+Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f.
 
 Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g).
 Proof. by split; apply: measurable_maxr. Qed.
 
 HB.instance Definition _ f g := max_mfun_subproof f g.
 
-Definition max_mfun f g := [the {mfun aT >-> _} of f \max g].
+Definition max_mfun f g : {mfun aT >-> _} := f \max g.
 
 End ring.
 Arguments indic_mfun {d aT rT} _.
@@ -365,7 +365,7 @@ HB.instance Definition _ := [Choice of {sfun aT >-> rT} by <:].
 (* NB: already instantiated in cardinality.v *)
 HB.instance Definition _ x : @FImFun aT rT (cst x) := FImFun.on (cst x).
 
-Definition cst_sfun x := [the {sfun aT >-> rT} of cst x].
+Definition cst_sfun x : {sfun aT >-> rT} := cst x.
 
 Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed.
 
@@ -426,14 +426,14 @@ Import HBSimple.
 HB.instance Definition _ (D : set aT) (mD : measurable D) :
    @FImFun aT rT (mindic _ mD) := FImFun.on (mindic _ mD).
 
-Definition indic_sfun (D : set aT) (mD : measurable D) :=
-  [the {sfun aT >-> rT} of mindic rT mD].
+Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} :=
+  mindic rT mD.
 
 HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k).
-Definition scale_sfun k f := [the {sfun aT >-> rT} of k \o* f].
+Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f.
 
 HB.instance Definition _ f g := max_mfun_subproof f g.
-Definition max_sfun f g := [the {sfun aT >-> _} of f \max g].
+Definition max_sfun f g : {sfun aT >-> _} := f \max g.
 
 End ring.
 Arguments indic_sfun {d aT rT} _.
@@ -495,7 +495,7 @@ HB.instance Definition _ x := @isNonNegFun.Build T R (cst x%:num)
 (* NB: already instantiated in cardinality.v *)
 HB.instance Definition _ x : @FImFun T R (cst x) := FImFun.on (cst x).
 
-Definition cst_nnsfun (r : {nonneg R}) := [the {nnsfun T >-> R} of cst r%:num].
+Definition cst_nnsfun (r : {nonneg R}) : {nnsfun T >-> R} := cst r%:num.
 
 Definition nnsfun0 : {nnsfun T >-> R} := cst_nnsfun 0%R%:nng.
 
@@ -535,15 +535,15 @@ Variables f g : {nnsfun T >-> R}.
 Import HBNNSimple.
 
 HB.instance Definition _ := MeasurableFun.on (f \+ g).
-Definition add_nnsfun := [the {nnsfun T >-> R} of f \+ g].
+Definition add_nnsfun : {nnsfun T >-> R} := f \+ g.
 
 HB.instance Definition _ := MeasurableFun.on (f \* g).
-Definition mul_nnsfun := [the {nnsfun T >-> R} of f \* g].
+Definition mul_nnsfun : {nnsfun T >-> R} := f \* g.
 
 HB.instance Definition _ := MeasurableFun.on (f \max g).
-Definition max_nnsfun := [the {nnsfun T >-> R} of f \max g].
+Definition max_nnsfun : {nnsfun T >-> R} := f \max g.
 
-Definition indic_nnsfun A (mA : measurable A) := [the {nnsfun T >-> R} of mindic R mA].
+Definition indic_nnsfun A (mA : measurable A) : {nnsfun T >-> R} := mindic R mA.
 
 End nnsfun_bin.
 Arguments add_nnsfun {d T R} _ _.
@@ -1500,7 +1500,7 @@ Lemma cvg_approx x (f0 : forall x, D x -> (0 <= f x)%E) : D x ->
   (f x < +oo)%E -> approx^~ x @ \oo --> fine (f x).
 Proof.
 move=> Dx fxoo; have fxfin : f x \is a fin_num by rewrite ge0_fin_numE// f0.
-apply/(@cvgrPdist_lt _ [the normedModType R of R^o]) => _/posnumP[e].
+apply/(@cvgrPdist_lt _ R^o) => _/posnumP[e].
 have [fx0|fx0] := eqVneq (f x) 0%E.
   by near=> n; rewrite f0_approx0 // fx0 /= subrr normr0.
 have /(fpos_approx_neq0 Dx)[m _ Hm] : (0 < f x < +oo)%E by rewrite lt0e fx0 f0.
@@ -1753,7 +1753,7 @@ Lemma approximation_sfun :
 Proof.
 pose fp_ := nnsfun_approx mD (measurable_funepos mf).
 pose fn_ := nnsfun_approx mD (measurable_funeneg mf).
-exists (fun n => [the {sfun T >-> R} of fp_ n \+ cst (-1) \* fn_ n]) => x /=.
+exists (fun n => fp_ n \+ cst (-1) \* fn_ n) => x /=.
 rewrite [X in X @ \oo --> _](_ : _ =
     EFin \o fp_^~ x \+ (-%E \o EFin \o fn_^~ x))%E; last first.
   by apply/funext => n/=; rewrite EFinD mulN1r.
@@ -1767,8 +1767,8 @@ Section lusin.
 Hint Extern 0 (hausdorff_space _) => (exact: Rhausdorff) : core.
 Local Open Scope ereal_scope.
 Context (rT : realType) (A : set rT).
-Let mu := [the measure _ _ of @lebesgue_measure rT].
-Let R  := [the measurableType _ of measurableTypeR rT].
+Let mu : measure _ _ := @lebesgue_measure rT.
+Let R  : measurableType _ := measurableTypeR rT.
 Hypothesis mA : measurable A.
 Hypothesis finA : mu A < +oo.
 
@@ -4254,10 +4254,10 @@ Lemma integral_count (a : nat -> \bar R) : summable setT a ->
   \int[counting]_t (a t) = \sum_(k <oo) (a k).
 Proof.
 move=> sa.
-transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t).
+transitivity (\int[mseries (fun n => \d_ n) O]_t a t).
   congr (integral _ _ _); apply/funext => A.
   by rewrite /= counting_dirac.
-rewrite (@integral_measure_series _ _ R (fun n => [the measure _ _ of \d_ n]) setT)//=.
+rewrite (@integral_measure_series _ _ R (fun n => \d_ n) setT)//=.
 - by apply: eq_eseriesr=> i _; rewrite integral_dirac//= diracT mul1e.
 - move=> n; apply/integrableP; split=> [//|].
   by rewrite integral_dirac//= diracT mul1e (summable_pinfty sa).
@@ -4269,7 +4269,7 @@ Lemma ge0_integral_count (a : nat -> \bar R) : (forall k, 0 <= a k) ->
   \int[counting]_t (a t) = \sum_(k <oo) (a k).
 Proof.
 move=> sa.
-transitivity (\int[mseries (fun n => [the measure _ _ of \d_ n]) O]_t a t).
+transitivity (\int[mseries (fun n => \d_ n) O]_t a t).
   congr (integral _ _ _); apply/funext => A.
   by rewrite /= counting_dirac.
 rewrite (@ge0_integral_measure_series _ _ R (fun n => \d_ n) setT)//=.
@@ -5087,7 +5087,7 @@ HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
   product_measure_sigma_finite.
 
 Lemma product_measure_unique
-    (m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) :
+    (m' : {measure set (T1 * T2) -> \bar R}) :
     (forall A B, measurable A -> measurable B -> m' (A `*` B) = m1 A * m2 B) ->
   forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
 Proof.
@@ -5283,8 +5283,8 @@ End simple_density_L1.
 
 Section continuous_density_L1.
 Context (rT : realType).
-Let mu := [the measure _ _ of @lebesgue_measure rT].
-Let R  := [the measurableType _ of measurableTypeR rT].
+Let mu : measure _ _ := @lebesgue_measure rT.
+Let R  : measurableType _ := measurableTypeR rT.
 Local Open Scope ereal_scope.
 
 Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
@@ -5475,7 +5475,7 @@ Qed.
 End indic_fubini_tonelli.
 
 Section sfun_fubini_tonelli.
-Variable f : {nnsfun [the measurableType _ of T1 * T2 : Type] >-> R}.
+Variable f : {nnsfun T1 * T2 >-> R}.
 
 Import HBNNSimple.
 
@@ -5599,7 +5599,7 @@ Section fubini_tonelli.
 Variable f : T1 * T2 -> \bar R.
 Hypothesis mf : measurable_fun setT f.
 Hypothesis f0 : forall x, 0 <= f x.
-Let T := [the measurableType _ of T1 * T2 : Type].
+Let T : measurableType _ := (T1 * T2)%type.
 
 Let F := fubini_F m2 f.
 Let G := fubini_G m1 f.
@@ -5928,7 +5928,7 @@ Lemma sfinite_Fubini :
 Proof.
 pose s1 := sfinite_measure_seq m1.
 pose s2 := sfinite_measure_seq m2.
-rewrite [LHS](eq_measure_integral [the measure _ _ of mseries s1 0]); last first.
+rewrite [LHS](eq_measure_integral (mseries s1 0)); last first.
   by move=> A mA _; rewrite /=; exact: sfinite_measure_seqP.
 transitivity (\int[mseries s1 0]_x \int[mseries s2 0]_y f (x, y)).
   apply: eq_integral => x _; apply: eq_measure_integral => ? ? _.
@@ -5973,8 +5973,8 @@ Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
 
 Section lebesgue_differentiation_continuous.
 Context (rT : realType).
-Let mu := [the measure _ _ of @lebesgue_measure rT].
-Let R  := [the measurableType _ of measurableTypeR rT].
+Let mu : measure _ _ := @lebesgue_measure rT.
+Let R  : measurableType _ := measurableTypeR rT.
 
 Let ballE (x : R) (r : {posnum rT}) :
   ball x r%:num = `](x - r%:num), (x + r%:num)[%classic :> set rT.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index c0abfbdd3..ecde135c1 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -1959,8 +1959,7 @@ HB.instance Definition _ := isContent.Build _ _ R
 
 Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core.
 
-Lemma hlength_sigma_subadditive :
-  measurable_subset_sigma_subadditive (hlength : set (ocitv_type R) -> _).
+Lemma hlength_sigma_subadditive : measurable_subset_sigma_subadditive hlength.
 Proof.
 move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-].
 rewrite /subset_sigma_subadditive hlength_itv ?lte_fin/= -EFinB => lebig.
@@ -1987,8 +1986,7 @@ move=> /[apply]-[i _|X _ Xc]; first exact: interval_open.
 have: `](a.1 + e%:num / 2), a.2] `<=` \bigcup_(i in [set` X]) Aoc i.
   move=> x /subset_itv_oc_cc /Xc [i /= Xi] Aooix.
   by exists i => //; apply: subset_itv_oo_oc Aooix.
-have /[apply] := @content_sub_fsum _ _ _
-  [the content _ _ of hlength : set (ocitv_type R) -> _] _ [set` X].
+have /[apply] := @content_sub_fsum _ _ _ hlength _ [set` X].
 move=> /(_ _ _ _)/Box[]//=; apply: le_le_trans.
   rewrite hlength_itv ?lte_fin -?EFinD/= -addrA -opprD.
   by case: ltP => //; rewrite lee_fin subr_le0.
@@ -2004,7 +2002,7 @@ Qed.
 HB.instance Definition _ := Content_SigmaSubAdditive_isMeasure.Build _ _ _
   hlength hlength_sigma_subadditive.
 
-Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _).
+Lemma hlength_sigma_finite : sigma_finite setT hlength.
 Proof.
 exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT.
 by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry.
@@ -2024,15 +2022,14 @@ End hlength_extension.
 End LebesgueMeasure.
 
 Definition lebesgue_measure {R : realType} :
-  set [the measurableType _.-sigma of
-       g_sigma_algebraType R.-ocitv.-measurable] -> \bar R :=
-  [the measure _ _ of lebesgue_stieltjes_measure idfun].
+  set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R :=
+  lebesgue_stieltjes_measure idfun.
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
   SigmaFiniteMeasure.on (@lebesgue_measure R).
 
 Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R :=
-  [the measure _ _ of completed_lebesgue_stieltjes_measure idfun].
+  completed_lebesgue_stieltjes_measure idfun.
 HB.instance Definition _ (R : realType) :=
   Measure.on (@completed_lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
@@ -2301,8 +2298,7 @@ Section lebesgue_measure_itv.
 Variable R : realType.
 
 Let lebesgue_measure_itvoc (a b : R) :
-  (lebesgue_measure (`]a, b] : set R) =
-  wlength [the cumulative _ of idfun] `]a, b])%classic.
+  (lebesgue_measure (`]a, b] : set R) = wlength idfun `]a, b])%classic.
 Proof.
 rewrite /lebesgue_measure/= /lebesgue_stieltjes_measure/= /measure_extension/=.
 by rewrite measurable_mu_extE//; exact: is_ocitv.
@@ -2327,7 +2323,7 @@ rewrite (_ : _ \o _ = (fun n => (1 - n.+1%:R^-1)%:E)); last first.
     by rewrite ler_ltB// invr_lt1 ?unitfE// ltr1n ltnS lt0n.
   by rewrite !(EFinB,EFinN) fin_num_oppeB// addeAC addeA subee// add0e.
 apply/cvg_lim => //=; apply/fine_cvgP; split => /=; first exact: nearW.
-apply/(@cvgrPdist_lt _ [the pseudoMetricNormedZmodType R of R^o]) => _/posnumP[e].
+apply/(@cvgrPdist_lt _ R^o) => _/posnumP[e].
 near=> n; rewrite opprB addrCA subrr addr0 ger0_norm//.
 by near: n; exact: near_infty_natSinv_lt.
 Unshelve. all: by end_near. Qed.
@@ -2347,8 +2343,7 @@ by rewrite in_itv/= => + xa; rewrite xa ltxx andbF.
 Qed.
 
 Let lebesgue_measure_itvoo (a b : R) :
-  (lebesgue_measure (`]a, b[ : set R) =
-   wlength [the cumulative _ of idfun] `]a, b[)%classic.
+  (lebesgue_measure (`]a, b[ : set R) = wlength idfun `]a, b[)%classic.
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
@@ -2358,8 +2353,7 @@ rewrite 2!wlength_itv => <-; rewrite -setUitv1// measureU//.
 Qed.
 
 Let lebesgue_measure_itvcc (a b : R) :
-  (lebesgue_measure (`[a, b] : set R) =
-   wlength [the cumulative _ of idfun] `[a, b])%classic.
+  (lebesgue_measure (`[a, b] : set R) = wlength idfun `[a, b])%classic.
 Proof.
 have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
@@ -2369,8 +2363,7 @@ rewrite 2!wlength_itv => <-; rewrite -setU1itv// measureU//.
 Qed.
 
 Let lebesgue_measure_itvco (a b : R) :
-  (lebesgue_measure (`[a, b[ : set R) =
-   wlength [the cumulative _ of idfun] `[a, b[)%classic.
+  (lebesgue_measure (`[a, b[ : set R) = wlength idfun `[a, b[)%classic.
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoo a b.
@@ -2381,7 +2374,7 @@ Qed.
 
 Let lebesgue_measure_itv_bnd (x y : bool) (a b : R) :
   lebesgue_measure ([set` Interval (BSide x a) (BSide y b)] : set R) =
-  wlength [the cumulative _ of idfun] [set` Interval (BSide x a) (BSide y b)].
+  wlength idfun [set` Interval (BSide x a) (BSide y b)].
 Proof.
 by move: x y => [|] [|]; [exact: lebesgue_measure_itvco |
   exact: lebesgue_measure_itvcc | exact: lebesgue_measure_itvoo |
@@ -2566,7 +2559,7 @@ End negligible_outer_measure.
 Section lebesgue_regularity.
 Local Open Scope ereal_scope.
 Context {R : realType}.
-Let mu := [the measure _ _ of @lebesgue_measure R].
+Let mu : measure _ _ := @lebesgue_measure R.
 
 Lemma lebesgue_regularity_outer (D : set R) (eps : R) :
   measurable D -> mu D < +oo -> (0 < eps)%R ->
@@ -2888,7 +2881,7 @@ have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =
     rewrite -bigcup_mkcond; apply: bigcup_measurable => k _.
     exact: measurable_closure.
   rewrite esum_mkcond//= nneseries_esum// -fun_true//=.
-  by under eq_esum do rewrite (fun_if mu) (measure0 [the measure _ _ of mu]).
+  by under eq_esum do rewrite (fun_if mu) (measure0 mu).
 apply/eqP; rewrite -measure_le0.
 apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e.
 have [N F5e] : exists N, \sum_(N <= n <oo) \esum_(i in F n) mu (closure (B i)) <
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 9e05ac8e7..45312722c 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -76,8 +76,7 @@ Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R)
   e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e.
 Proof.
 move=> e0; move: (cumulative_is_right_continuous f).
-move=> /(_ a)/(@cvgr_dist_lt _ [the normedModType R of R^o]).
-move=> /(_ _ e0)[] _ /posnumP[d] => h.
+move=> /(_ a) /(@cvgr_dist_lt _ R^o) /(_ _ e0)[] _ /posnumP[d] => h.
 exists (PosNum [gt0 of (d%:num / 2)]) => //=.
 move: h => /(_ (a + d%:num / 2)) /=.
 rewrite opprD addrA subrr distrC subr0 ger0_norm //.
@@ -397,11 +396,9 @@ move=> Dab h; have [ab|ab] := leP a0 b0; last first.
   by rewrite subr_ge0 cumulative_is_nondecreasing// Dab.
 have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by [].
 move: h; rewrite -bigcup_fset.
-move/(@content_sub_fsum _ R _ [the content _ _ of wlength f] _ [set` D]
-    `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab
-  (is_ocitv _ _)) => /=.
+move/(content_sub_fsum (wlength f) (finite_fset D) mab (is_ocitv a0 b0)) => /=.
 rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply.
-rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq.
+rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in leRHS]big_seq.
 by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab.
 Qed.
 
@@ -495,7 +492,7 @@ by case: ifP; rewrite ltey.
 Qed.
 
 Definition lebesgue_stieltjes_measure (f : cumulative R) :=
-  measure_extension [the measure _ _ of wlength f].
+  measure_extension (wlength f).
 HB.instance Definition _ (f : cumulative R) :=
   Measure.on (lebesgue_stieltjes_measure f).
 
@@ -514,7 +511,7 @@ Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing).
 
 Section lebesgue_stieltjes_measure.
 Variable R : realType.
-Let gitvs := [the measurableType _ of g_sigma_algebraType (@ocitv R)].
+Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R).
 
 Lemma lebesgue_stieltjes_measure_unique (f : cumulative R)
     (mu : {measure set gitvs -> \bar R}) :
@@ -532,7 +529,7 @@ Section completed_lebesgue_stieltjes_measure.
 Context {R : realType}.
 
 Definition completed_lebesgue_stieltjes_measure (f : cumulative R) :=
-  @completed_measure_extension _ _ _ [the measure _ _ of wlength f].
+  @completed_measure_extension _ _ _ (wlength f).
 
 HB.instance Definition _ (f : cumulative R) :=
   Measure.on (@completed_lebesgue_stieltjes_measure f).
diff --git a/theories/measure.v b/theories/measure.v
index b26b412db..691b79f9b 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -3256,7 +3256,7 @@ move=> [F UF mF]; rewrite /sfinite_measure.
 have mDF k : measurable (seqDU F k).
   apply: measurableD; first exact: (mF k).1.
   by apply: bigsetU_measurable => i _; exact: (mF i).1.
-exists (fun k => [the measure _ _ of mrestr mu (mDF k)]) => [n|U mU].
+exists (fun k => mrestr mu (mDF k)) => [n|U mU].
 - apply: lty_fin_num_fun => //=.
   rewrite /mrestr setTI (@le_lt_trans _ _ (mu (F n)))//.
   + apply: le_measure; last exact: subDsetl.
@@ -3320,7 +3320,7 @@ HB.builders Context d (T : measurableType d) (R : realType)
   mu of @Measure_isSigmaFinite d T R mu.
 
 Lemma sfinite : sfinite_measure mu.
-Proof. by apply: sfinite_measure_sigma_finite; exact: sigma_finiteT. Qed.
+Proof. exact/sfinite_measure_sigma_finite/sigma_finiteT. Qed.
 
 HB.instance Definition _ := @isSFinite.Build _ _ _ mu sfinite.
 
@@ -3337,7 +3337,7 @@ HB.instance Definition _ d (T : measurableType d) (R : realFieldType) :=
 
 Lemma sfinite_mzero d (T : measurableType d) (R : realType) :
   sfinite_measure (@mzero d T R).
-Proof. by apply: sfinite_measure_sigma_finite; exact: sigma_finite_mzero. Qed.
+Proof. exact/sfinite_measure_sigma_finite/sigma_finite_mzero. Qed.
 
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
   @isSFinite.Build d T R mzero (@sfinite_mzero d T R).
@@ -3464,8 +3464,7 @@ Proof. by rewrite /s; case: cid2 => F finF muE; exact: finF. Qed.
 
 HB.instance Definition _ n := @Measure_isFinite.Build d T R (s n) (s_fin n).
 
-Definition sfinite_measure_seq : {finite_measure set T -> \bar R}^nat :=
-  fun n => [the {finite_measure set T -> \bar R} of s n].
+Definition sfinite_measure_seq : {finite_measure set T -> \bar R}^nat := s.
 
 Lemma sfinite_measure_seqP U : measurable U ->
   mu U = mseries sfinite_measure_seq O U.
@@ -3627,7 +3626,7 @@ HB.instance Definition _ x :=
 End pdirac.
 
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
-  isPointed.Build (probability T R) [the probability _ _ of dirac point].
+  isPointed.Build (probability T R) (dirac point).
 
 Section dist_sigma_algebra_instance.
 Context d (T : measurableType d) (R : realType).
@@ -3651,7 +3650,7 @@ Definition pset : set (set (probability T R)) :=
   [set mset U r | r in `[0%R,1%R] & U in measurable].
 
 Definition pprobability : measurableType pset.-sigma :=
-  [the measurableType _ of g_sigma_algebraType pset].
+  g_sigma_algebraType pset.
 
 End dist_sigma_algebra_instance.
 
@@ -4946,7 +4945,7 @@ near=> n; apply: lee_sum => i _; rewrite -measure_semi_additive2.
 - by rewrite setIACA setICr setI0.
 Unshelve. all: by end_near. Qed.
 
-Let I := [the measurableType _ of g_sigma_algebraType (@measurable _ T)].
+Let I : measurableType _ := g_sigma_algebraType (@measurable _ T).
 
 Definition measure_extension : set I -> \bar R := mu^*.
 
@@ -4984,7 +4983,7 @@ Lemma measure_extension_unique : sigma_finite [set: T] mu ->
       measure_extension X = mu' X)).
 Proof.
 move=> [F TF /all_and2[Fm muF]] mu' mu'mu X mX.
-apply: (@measure_unique _ _ [the measurableType _ of I] d.-measurable F) => //.
+apply: (@measure_unique _ _ I d.-measurable F) => //.
 - by move=> A B Am Bm; apply: measurableI.
 - by move=> A Am; rewrite /= /measure_extension measurable_mu_extE// mu'mu.
 - by move=> k; rewrite /= /measure_extension measurable_mu_extE.
@@ -5006,7 +5005,7 @@ Variable mu : {measure set T -> \bar R}.
 Notation rT := (SetRing.type T).
 Let Rmu : set rT -> \bar R := SetRing.measure mu.
 
-Let I := [the measurableType _ of caratheodory_type (mu^*)%mu].
+Let I : measurableType _ := caratheodory_type (mu^*)%mu.
 
 Definition completed_measure_extension : set I -> \bar R := (mu^*)%mu.
 
@@ -5140,7 +5139,7 @@ Hypothesis setTC2 : setT `<=` C2.
 
 (* NB: useful? *)
 Lemma measurable_prod_g_measurableTypeR :
-  @measurable _ [the measurableType _ of T1 * g_sigma_algebraType C2 : Type]
+  @measurable _ (T1 * g_sigma_algebraType C2)%type
   = <<s [set A `*` B | A in measurable & B in C2] >>.
 Proof.
 rewrite measurable_prod_measurableType //; congr (<<s _ >>).
@@ -5198,15 +5197,13 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2).
 
 Lemma measurable_fst : measurable_fun [set: T1 * T2] fst.
 Proof.
-by have /prod_measurable_funP[] :=
-  @measurable_id _ [the measurableType _ of (T1 * T2)%type] setT.
+by have /prod_measurable_funP[] := @measurable_id _ (T1 * T2)%type setT.
 Qed.
 #[local] Hint Resolve measurable_fst : core.
 
 Lemma measurable_snd : measurable_fun [set: T1 * T2] snd.
 Proof.
-by have /prod_measurable_funP[] :=
-  @measurable_id _ [the measurableType _ of (T1 * T2)%type] setT.
+by have /prod_measurable_funP[] := @measurable_id _ (T1 * T2)%type setT.
 Qed.
 #[local] Hint Resolve measurable_snd : core.
 
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 46eba5707..81ef032d2 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -1473,8 +1473,8 @@ Lemma open_itvoo_subset :
 Proof.
 move=> /[apply] -[] _/posnumP[r] /subset_ball_prop_in_itv xrA.
 exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0.
-by apply/(subset_trans _ xrA)/subset_itvW;
-  [rewrite lerB//; exact: ltW | rewrite lerD//; exact: ltW].
+by apply/(subset_trans _ xrA)/subset_itvW; apply/ltW;
+  [rewrite ler_ltB | rewrite ler_ltD].
 Qed.
 
 Lemma open_itvcc_subset :
@@ -2398,8 +2398,7 @@ Variables (K : numFieldType) (m n : nat).
 Local Lemma ball_gt0 (x y : 'M[K]_(m.+1, n.+1)) e : ball x e y -> 0 < e.
 Proof. by move/(_ ord0 ord0); apply: le_lt_trans. Qed.
 
-Lemma mx_norm_ball :
-  @ball _ [the pseudoMetricType K of 'M[K]_(m.+1, n.+1)] = ball_ (fun x => `| x |).
+Lemma mx_norm_ball : @ball _ 'M[K]_(m.+1, n.+1) = ball_ (fun x => `| x |).
 Proof.
 rewrite /normr /ball_ predeq3E => x e y /=; rewrite mx_normE; split => xey.
 - have e_gt0 : 0 < e := ball_gt0 xey.
@@ -2441,8 +2440,7 @@ rewrite /ball /= /prod_ball -!ball_normE /ball_ /=.
 by rewrite comparable_gt_max// ?real_comparable//; split=> /andP.
 Qed.
 
-Lemma prod_norm_ball :
-  @ball _ [the pseudoMetricType K of (U * V)%type] = ball_ (fun x => `|x|).
+Lemma prod_norm_ball : @ball _ (U * V)%type = ball_ (fun x => `|x|).
 Proof. by rewrite /= - ball_prod_normE. Qed.
 
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type
@@ -3041,7 +3039,7 @@ Qed.
 Lemma abse_continuous : continuous (@abse R).
 Proof.
 case=> [r|A /= [r [rreal rA]]|A /= [r [rreal rA]]]/=.
-- exact/(cvg_comp (@norm_continuous _ [the normedModType R of R^o] r)).
+- exact/(cvg_comp (@norm_continuous _ R r)).
 - by exists r; split => // y ry; apply: rA; rewrite (lt_le_trans ry)// lee_abs.
 - exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lteNr => yr.
   by apply: rA; rewrite (lt_le_trans yr)// -abseN lee_abs.
@@ -4207,8 +4205,7 @@ Unshelve. all: by end_near. Qed.
 HB.instance Definition _ (R : realType) := Uniform_isComplete.Build R^o
   (@R_complete R). (* todo : delete *)
 
-HB.instance Definition _ (R : realType) := Complete.copy R
-  [the completeType of R^o].
+HB.instance Definition _ (R : realType) := Complete.copy R R^o.
 (* new *)
 
 Section cvg_seq_bounded.
@@ -4794,27 +4791,27 @@ case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=.
     rewrite !(lteifF, lteifT).
   + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx].
     rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
-    apply: (@interior_subset [the topologicalType of R : Type]).
+    apply: (@interior_subset R).
     by rewrite interval_bounded_interior // /mkset infXx.
   + move=> /andP[]; rewrite le_eqVlt => /orP[/eqP <- //|infXx supXx].
-    apply: (@interior_subset [the topologicalType of R : Type]).
+    apply: (@interior_subset R).
     by rewrite interval_bounded_interior // /mkset infXx.
   + move=> /andP[infXx]; rewrite le_eqVlt => /orP[/eqP -> //|xsupX].
-    apply: (@interior_subset [the topologicalType of R : Type]).
+    apply: (@interior_subset R).
     by rewrite interval_bounded_interior // /mkset infXx.
-  + move=> ?; apply: (@interior_subset [the topologicalType of R : Type]).
+  + move=> ?; apply: (@interior_subset R).
     by rewrite interval_bounded_interior // /mkset infXx.
 - case: asboolP => XinfX; rewrite !(lteifF, lteifT, andbT).
   + rewrite le_eqVlt => /orP[/eqP<-//|infXx].
-    apply: (@interior_subset [the topologicalType of R : Type]).
+    apply: (@interior_subset R).
     by rewrite interval_right_unbounded_interior.
-  + move=> infXx; apply: (@interior_subset [the topologicalType of R : Type]).
+  + move=> infXx; apply: (@interior_subset R).
     by rewrite interval_right_unbounded_interior.
 - case: asboolP => XsupX /=.
   + rewrite le_eqVlt => /orP[/eqP->//|xsupX].
-    apply: (@interior_subset [the topologicalType of R : Type]).
+    apply: (@interior_subset R).
     by rewrite interval_left_unbounded_interior.
-  + move=> xsupX; apply: (@interior_subset [the topologicalType of R : Type]).
+  + move=> xsupX; apply: (@interior_subset R).
     by rewrite interval_left_unbounded_interior.
 - by move=> _; rewrite (interval_unbounded_setT iX).
 Qed.
diff --git a/theories/numfun.v b/theories/numfun.v
index 3a892df55..92f31a9c9 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -440,11 +440,11 @@ Qed.
 
 HB.instance Definition _ X := indic_fimfun_subproof X.
 
-Definition indic_fimfun (X : set aT) := [the {fimfun aT >-> rT} of \1_X].
+Definition indic_fimfun (X : set aT) : {fimfun aT >-> rT} := \1_X.
 
 HB.instance Definition _ k f := FImFun.copy (k \o* f) (f * cst_fimfun k).
 
-Definition scale_fimfun k f := [the {fimfun aT >-> rT} of k \o* f].
+Definition scale_fimfun k f : {fimfun aT >-> rT} := k \o* f.
 
 End ring.
 Arguments indic_fimfun {aT rT} _.
@@ -598,8 +598,7 @@ exists (lim (h_ @ \oo)); split.
 - move=> t /set_mem At; have /pointwise_cvgP/(_ t)/(cvg_lim (@Rhausdorff _)) :=
     !! pointwise_uniform_cvg _ cvgh.
   rewrite -fmap_comp /comp /h_ => <-; apply/esym/(@cvg_lim _ (@Rhausdorff R)).
-  apply: (@cvg_zero R [the pseudoMetricNormedZmodType R of R^o]).
-  apply: norm_cvg0; under eq_fun => n.
+  apply: (@cvg_zero R R^o); apply: norm_cvg0; under eq_fun => n.
     rewrite distrC /series /cst /= -mulN1r fct_sumE mulr_sumr.
     under [fun _ : nat => _]eq_fun => ? do rewrite mulN1r -fgE opprB.
     rewrite telescope_sumr //= addrCA subrr addr0.
diff --git a/theories/probability.v b/theories/probability.v
index c958e511f..11f4d758c 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -569,9 +569,8 @@ Local Notation "'M_ X t" := (mmt_gen_fun X t).
 Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R ->
   P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E.
 Proof.
-move=> t0.
-rewrite /mmt_gen_fun; have -> : expR \o r \o* X =
-    (normr \o normr) \o [the {mfun _ >-> _} of expR \o r \o* X].
+move=> t0; rewrite /mmt_gen_fun.
+have -> : expR \o r \o* X = (normr \o normr) \o (expR \o r \o* X).
   by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0.
 rewrite expRN lee_pdivlMr ?expR_gt0//.
 rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first.
@@ -600,7 +599,7 @@ have h (Y : {RV P >-> R}) :
   - by move=> x /=; exact: sqr_ge0.
   - by move=> x /=; exact: sqr_ge0.
   - by apply/aeW => t /=; rewrite real_normK// num_real.
-have := h [the {mfun T >-> R} of (X \- cst (fine ('E_P[X])))%R].
+have := h (X \- cst (fine ('E_P[X])))%R.
 by move=> /le_trans; apply; rewrite /variance [in leRHS]unlock.
 Qed.
 
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 89a01e9d6..023e28739 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -955,8 +955,7 @@ Definition type : Type := let _ := countableBase in let _ := entF in T.
 #[export] HB.instance Definition _ {q : Pointed T} :=
   Pointed.copy type (Pointed.Pack q).
 
-Lemma countable_uniform_bounded (x y : T) :
-  let U := [the pseudoMetricType R of type] in @ball _ U x 2 y.
+Lemma countable_uniform_bounded (x y : T) : @ball _ type x 2 y.
 Proof.
 rewrite /ball; exists O%N; rewrite /n_step_ball; split; rewrite // /distN.
 rewrite [X in `|X|%N](_ : _ = 0) ?absz0//.
diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v
index 29b8dc62f..ef2df6951 100644
--- a/theories/topology_theory/bool_topology.v
+++ b/theories/topology_theory/bool_topology.v
@@ -48,7 +48,7 @@ End bool_ord_topology.
 Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool].
 Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed.
 
-Definition pseudoMetric_bool {R : realType} :=
-  [the pseudoMetricType R of discrete_topology discrete_bool : Type].
+Definition pseudoMetric_bool {R : realType} : pseudoMetricType R :=
+  discrete_topology discrete_bool.
 
 #[global] Hint Resolve discrete_bool : core.
diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v
index 0168e1809..adada2fa9 100644
--- a/theories/topology_theory/subspace_topology.v
+++ b/theories/topology_theory/subspace_topology.v
@@ -249,8 +249,7 @@ Lemma closure_subspaceW (U : set T) :
   U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A.
 Proof.
 have /closed_subspaceP := (@closed_closure _ (U : set (subspace A))).
-move=> [V] [clV VAclUA].
-move=> /[dup] /(@closure_subset [the topologicalType of subspace _]).
+move=> [V] [clV VAclUA] /[dup] /(@closure_subset (subspace _)).
 have /closure_id <- := closed_subspaceT => /setIidr <-; rewrite setIC.
 move=> UsubA; rewrite eqEsubset; split.
   apply: setSI; rewrite closureE; apply: smallest_sub (@subset_closure _ U).
diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v
index 7546e0b1b..14cec1014 100644
--- a/theories/topology_theory/supremum_topology.v
+++ b/theories/topology_theory/supremum_topology.v
@@ -45,7 +45,7 @@ move=> Ffilt; split=> cvFt.
   move=> _ ->; exists [fset B]%fset.
     by move=> ?; rewrite inE inE => /eqP->; exists i.
   by rewrite predeqE=> ?; split=> [|??]; [apply|]; rewrite /= inE // =>/eqP->.
-move=> A /=; rewrite (@nbhsE [the topologicalType of S]).
+move=> A /=; rewrite (@nbhsE S).
 move=> [_ [[B sB <-] [C BC Ct] sUBA]].
 rewrite nbhs_filterE; apply: filterS sUBA _; apply: (@filterS _ _ _ C).
   by move=> ? ?; exists C.