diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7b8c09aae5..35fb4aaef5 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,14 +8,6 @@
   + `kseries` is now an instance of `Kernel_isSFinite_subdef`
 - in `classical_sets.v`:
   + lemma `setU_id2r`
-- in `topology.v`:
-  + lemma `globally0`
-- in `normedtype.v`:
-  + lemma `lipschitz_set0`, `lipschitz_set1`
-- in `measure.v`:
-  + lemma `measurable_fun_bigcup`
-- in `sequences.v`:
-  + lemma `eq_eseriesl`
 - in `lebesgue_measure.v`:
   + lemma `compact_measurable`
 
@@ -60,54 +52,6 @@
 
 - in `constructive_ereal.v`:
   + lemma `bigmaxe_fin_num`
-  + lemmas `lee_sqr`, `lte_sqr`, `lee_sqrE`, `lte_sqrE`, `sqre_ge0`,
-    `EFin_expe`, `sqreD`, `sqredD`
-- in `probability.v`
-  + definition of `covariance`
-  + lemmas `expectation_sum`, `covarianceE`, `covarianceC`,
-    `covariance_fin_num`, `covariance_cst_l`, `covariance_cst_r`,
-    `covarianceZl`, `covarianceZr`, `covarianceNl`, `covarianceNr`,
-    `covarianceNN`, `covarianceDl`, `covarianceDr`, `covarianceBl`,
-    `covarianceBr`, `variance_fin_num`, `varianceZ`, `varianceN`,
-    `varianceD`, `varianceB`, `varianceD_cst_l`, `varianceD_cst_r`,
-    `varianceB_cst_l`, `varianceB_cst_r`
-- in `functions.v`:
-  + lemma `sumrfctE`
-- in `lebesgue_integral.v`:
-  + lemma `integrable_sum`
-- in `probability.v`
-  + lemma `cantelli`
-- in `classical_sets.v`:
-  + lemmas `preimage_mem_true`, `preimage_mem_false`
-- in `measure.v`:
-  + definition `measure_dominates`, notation `` `<< ``
-  + lemma `measure_dominates_trans`
-- in `measure.v`:
-  + defintion `mfrestr`
-- in `charge.v`:
-  + definition `measure_of_charge`
-  + definition `crestr0`
-  + definitions `jordan_neg`, `jordan_pos`
-  + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates`
-  + lemma `radon_nikodym_finite`
-  + definition `Radon_Nikodym`, notation `'d nu '/d mu`
-  + theorems `Radon_Nikodym_integrable`, `Radon_Nikodym_integral`
-
-- in `measure.v`:
-  + lemmas `measurable_pair1`, `measurable_pair2`
-  + lemma `covariance_le`
-- in `mathcomp_extra.v`
-  + definition `coefE` (will be in MC 2.1/1.18)
-  + lemmas `deg2_poly_canonical`, `deg2_poly_factor`, `deg2_poly_min`,
-    `deg2_poly_minE`, `deg2_poly_ge0`, `Real.deg2_poly_factor`,
-    `deg_le2_poly_delta_ge0`, `deg_le2_poly_ge0`
-    (will be in MC 2.1/1.18)
-  + lemma `deg_le2_ge0`
-  + new lemmas `measurable_subring`, and `semiring_sigma_additive`.
-  + added factory `Content_SubSigmaAdditive_isMeasure`
-
-- in `lebesgue_integral.v`:
-  + lemmas `integrableP`, `measurable_int`
 
 - in file `cantor.v`,
   + new definitions `cantor_space`, `cantor_like`, `pointedDiscrete`, and 
diff --git a/theories/cantor.v b/theories/cantor.v
index 0378a4bd91..6aca4ade5a 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -10,9 +10,9 @@ From HB Require Import structures.
 (*                                                                            *)
 (* This file develops the theory of the Cantor space, that is bool^nat with   *)
 (* the product topology. The two main theorems proved here are                *)
-(* homeomorphism_cantor_like, and cantor_surj, aka Alexandroff-Hausdorff,.    *)
+(* homeomorphism_cantor_like, and cantor_surj, aka Alexandroff-Hausdorff.     *)
 (*                                                                            *)
-(*         cantor_space == the cantor space, with its canonical metric        *)
+(*         cantor_space == the Cantor space, with its canonical metric        *)
 (*         cantor_like T == perfect + compact + hausdroff + zero dimensional  *)
 (*         pointed_discrete T == equips T with the discrete topology          *)
 (*         tree_of T == builds a topological tree with levels (T n)           *)
@@ -22,8 +22,10 @@ From HB Require Import structures.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
+
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldTopology.Exports.
+
 Local Open Scope classical_set_scope.
 
 Definition cantor_space :=
@@ -39,10 +41,10 @@ Canonical cantor_pseudoMetric {R} :=
   @product_pseudoMetricType R _ (fun (_ : nat) =>
     @discrete_pseudoMetricType R _ discrete_bool) (countableP _).
 
-Lemma cantor_space_compact: compact [set: cantor_space].
+Lemma cantor_space_compact : compact [set: cantor_space].
 Proof.
-have := @tychonoff _ (fun (_: nat) => _) _ (fun=> bool_compact).
-by congr (compact _); rewrite eqEsubset; split => b.
+have := @tychonoff _ (fun _ : nat => _) _ (fun=> bool_compact).
+by congr (compact _); rewrite eqEsubset.
 Qed.
 
 Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
@@ -54,7 +56,7 @@ Proof. by apply: zero_dimension_prod => _; exact: discrete_zero_dimension. Qed.
 Lemma cantor_perfect : perfect_set [set: cantor_space].
 Proof. by apply: perfect_diagonal => _; exists (true, false). Qed.
 
-Lemma cantor_like_cantor_space: cantor_like cantor_space.
+Lemma cantor_like_cantor_space : cantor_like cantor_space.
 Proof.
 split.
 - exact: cantor_perfect.
@@ -64,15 +66,15 @@ split.
 Qed.
 
 (* The overall goal of the next few sections is to prove that
-        Every compact metric space `T` is the image of the cantor space.
+        Every compact metric space `T` is the image of the Cantor space.
    The overall proof will build two continuous functions
-             cantor space -> a bespoke tree for `T` -> `T`
+             Cantor space -> a bespoke tree for `T` -> `T`
    The proof is in 4 parts.
 
    Part 1: Some generic machinery about continuous functions from trees.
-   Part 2: All cantor-like spaces are homeomorphic to the cantor space.
+   Part 2: All cantor-like spaces are homeomorphic to the Cantor space.
           (an application of part 1)
-   Part 3: Finitely branching trees are cantor-like.
+   Part 3: Finitely branching trees are Cantor-like.
    Part 4: Every compact metric space has a finitely branching tree with
            a continuous surjection. (a second application of part 1)
 
@@ -82,14 +84,14 @@ Qed.
    The goal is to build a map from branches to X.
    1. Each level of the tree corresponds to an approximation of `X`.
    2. Each level refines the previous approximation.
-   3. Then each branch has a corresponding cauchy filter.
+   3. Then each branch has a corresponding Cauchy filter.
    4. The overall function from branches to X is a continuous surjection.
    5. With an extra disjointness condition, this is also an injection
 *)
 Section topological_trees.
-Context {K : nat -> topologicalType} {X : topologicalType}.
-Context (refine_apx : forall n, set X -> K n -> set X).
-Context (tree_invariant : (set X -> Prop)).
+Context {K : nat -> topologicalType} {X : topologicalType}
+        (refine_apx : forall n, set X -> K n -> set X)
+        (tree_invariant : set X -> Prop).
 
 Hypothesis cmptX : compact [set: X].
 Hypothesis hsdfX : hausdorff_space X.
@@ -99,42 +101,41 @@ Hypothesis refine_invar : forall n U e,
   tree_invariant U -> tree_invariant (@refine_apx n U e).
 Hypothesis invar_n0 : forall U, tree_invariant U -> U !=set0.
 Hypothesis invarT : tree_invariant [set: X].
-Hypothesis invar_cl : (tree_invariant `<=` closed).
-Hypothesis refine_separates: forall (x y : X), x != y ->
-  exists n, (forall (U : set X) e,
-    @refine_apx n U e x -> ~@refine_apx n U e y).
+Hypothesis invar_cl : tree_invariant `<=` closed.
+Hypothesis refine_separates: forall x y : X, x != y ->
+  exists n, forall (U : set X) e,
+    @refine_apx n U e x -> ~@refine_apx n U e y.
 
-
-Local Lemma refine_subset : forall n U e, @refine_apx n U e `<=` U.
-Proof.
-by move=> n U e; rewrite [x in _ `<=` x] (refine_cover n); exact: bigcup_sup.
-Qed.
+Local Lemma refine_subset n U e : @refine_apx n U e `<=` U.
+Proof. by rewrite [X in _ `<=` X](refine_cover n); exact: bigcup_sup. Qed.
 
 Let T := product_topologicalType K.
 
 Local Fixpoint branch_apx (b : T) n :=
-  if n is S m then refine_apx (branch_apx b m) (b m) else [set: X].
+  if n is m.+1 then refine_apx (branch_apx b m) (b m) else [set: X].
 
 Let tree_mapF (b : T) := filter_from [set: nat] (branch_apx b).
 
 Local Lemma tree_map_invar b n : tree_invariant (branch_apx b n).
 Proof. by elim: n => // n ?; exact: refine_invar. Qed.
 
-Local Lemma tree_map_sub b i j : (i <= j)%N -> branch_apx b j `<=` branch_apx b i.
-elim: j i; first by move=> ?; rewrite leqn0 => /eqP ->.
-move=> j IH i; rewrite leq_eqVlt => /orP; case; first by move=> /eqP ->.
-by move/IH/(subset_trans _); apply; exact: refine_subset.
+Local Lemma tree_map_sub b i j :
+  (i <= j)%N -> branch_apx b j `<=` branch_apx b i.
+Proof.
+elim: j i => [?|j IH i]; first by rewrite leqn0 => /eqP ->.
+rewrite leq_eqVlt => /predU1P[->//|/IH].
+by apply: subset_trans; exact: refine_subset.
 Qed.
 
 Instance tree_map_filter b : ProperFilter (tree_mapF b).
 Proof.
 split; first by case => n _ P; case: (invar_n0 (tree_map_invar b n)) => x /P.
-apply: filter_from_filter; first by exists O.
-move=> i j _ _; exists (maxn i j) => //; rewrite subsetI.
+apply: filter_from_filter; first by exists 0%N.
+move=> i j _ _; exists (maxn i j)  => //; rewrite subsetI.
 by split; apply: tree_map_sub; [exact: leq_maxl | exact: leq_maxr].
 Qed.
 
-Let tree_map (b : T) := lim (tree_mapF b).
+Let tree_map b := lim (tree_mapF b).
 
 Local Lemma cvg_tree_map b : cvg (tree_mapF b).
 Proof.
@@ -142,57 +143,54 @@ have [|x [_ clx]] := cmptX (tree_map_filter b); first exact: filterT.
 apply/cvg_ex; exists x => /=; apply: (compact_cluster_set1 _ cmptX) => //.
 - exact: filterT.
 - exact: filterT.
-rewrite eqEsubset; split; last by move=> ? ->.
-move=> y cly; case: (eqVneq x y); first by move=> ->.
-case/refine_separates => n sep; have bry : branch_apx b n.+1 y.
-  rewrite [branch_apx _ _](iffLR (closure_id _)).
-    by move: cly; rewrite clusterE; apply; exists n.+1.
-  by apply: invar_cl; exact: tree_map_invar.
-suff /sep : branch_apx b n.+1 x by done.
-rewrite [branch_apx _ _](iffLR (closure_id _)).
-  by move: clx; rewrite clusterE; apply; exists n.+1.
-by apply: invar_cl; exact: tree_map_invar.
+rewrite eqEsubset; split=> [y cly|? -> //].
+have [->//|/refine_separates[n sep]] := eqVneq x y.
+have bry : branch_apx b n.+1 y.
+  have /closure_id -> := invar_cl (tree_map_invar b n.+1).
+  by move: cly; rewrite clusterE; apply; exists n.+1.
+suff /sep : branch_apx b n.+1 x by [].
+have /closure_id -> := invar_cl (tree_map_invar b n.+1).
+by move: clx; rewrite clusterE; apply; exists n.+1.
 Qed.
 
 Local Lemma tree_map_surj : set_surj [set: T] [set: X] tree_map.
 Proof.
 move=> z _; suff : exists g, forall n, branch_apx g n z.
   case=> g gnz; exists g => //; apply: close_eq => // U [oU Uz] V ngV; exists z.
-  by split => //; have [n _] := @cvg_tree_map g _ ngV; by apply; exact: gnz.
+  by split => //; have [n _] := @cvg_tree_map g _ ngV; exact.
 have zcov' : forall n (U : set X), exists e, U z -> @refine_apx n U e z.
-  move=> n U; case: (pselect (U z)); last by move => ?; exists point.
-  by rewrite {1}(@refine_cover n U); case => e _ ?; exists e.
+  move=> n U; have [|?] := pselect (U z); last by exists point.
+  by rewrite [X in X z -> _](@refine_cover n U); case => e _ ?; exists e.
 pose zcov n U := projT1 (cid (zcov' n U)).
-pose fix g n : (K n * set X) :=
-  if n is S m
+pose fix g n : K n * set X :=
+  if n is m.+1
   then (zcov m.+1 (g m).2, @refine_apx m.+1 (g m).2 (zcov m.+1 (g m).2))
   else (zcov O [set: X], @refine_apx O [set: X] (zcov O [set: X])).
-pose g' n := (g n).1; have apxg : forall n, branch_apx g' n.+1 = (g n).2.
-  by elim => //= n ->; congr (_ _).
+pose g' n := (g n).1; have apxg n : branch_apx g' n.+1 = (g n).2.
+  by elim: n => //= n ->.
 exists g'; elim => // n /= IH.
 have /(_ IH) := projT2 (cid (zcov' n (branch_apx g' n))).
 by case: n {IH} => // n; rewrite apxg.
 Qed.
 
-Local Lemma tree_prefix (b: T) (n : nat) :
+Local Lemma tree_prefix (b : T) (n : nat) :
   \forall c \near b, forall i,  (i < n)%N -> b i = c i.
 Proof.
-elim: n; first by near=> z => ?; rewrite ltn0.
-move=> n IH; near=> z => i; rewrite leq_eqVlt => /orP []; first last.
-  by move=> iSn; have -> := near IH z.
-move=> /eqP/succn_inj ->; near: z; exists (proj n@^-1` [set b n]). 
-split => //; suff : @open T (proj n@^-1` [set b n]) by [].
+elim: n => [|n IH]; first by near=> z => ?; rewrite ltn0.
+near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z).
+move=> [->]; near: z; exists (proj n @^-1` [set b n]).
+split => //; suff : @open T (proj n @^-1` [set b n]) by [].
 by apply: open_comp; [move=> + _; exact: proj_continuous| exact: discrete_open].
 Unshelve. all: end_near. Qed.
 
-Local Lemma apx_prefix (b c : T) (n : nat) :
+Local Lemma apx_prefix b c n :
   (forall i, (i < n)%N -> b i = c i) -> branch_apx b n = branch_apx c n.
 Proof.
-elim: n => //= n IH inS; rewrite IH; first by congr (refine_apx _); exact: inS.
-by move=> ? ?; apply: inS; exact: ltnW.
+elim: n => //= n IH inS; rewrite IH; first by rewrite inS.
+by move=> ? ?; exact/inS/ltnW.
 Qed.
 
-Local Lemma tree_map_apx b n: branch_apx b n (tree_map b).
+Local Lemma tree_map_apx b n : branch_apx b n (tree_map b).
 Proof.
 apply: (@closed_cvg _ _ _ (tree_map_filter b)); last exact: cvg_tree_map.
   by apply: invar_cl; exact: tree_map_invar.
@@ -202,33 +200,36 @@ Qed.
 Local Lemma tree_map_cts : continuous tree_map.
 Proof.
 move=> b U /cvg_tree_map [n _] /filterS; apply.
-  by apply: fmap_filter; exact: nbhs_filter.
+  exact/fmap_filter/nbhs_filter.
 rewrite nbhs_simpl /=; near_simpl; have := tree_prefix b n; apply: filter_app.
-by near=> z => /apx_prefix ->; apply: tree_map_apx.
+by near=> z => /apx_prefix ->; exact: tree_map_apx.
 Unshelve. all: end_near. Qed.
 
-Let tree_map_inj: (forall n U, trivIset [set: K n] (@refine_apx n U)) ->
+Let tree_map_setI x y n : tree_map x = tree_map y ->
+  refine_apx (branch_apx x n) (x n) `&` refine_apx (branch_apx y n) (y n) !=set0.
+Proof.
+move=> xyE; exists (tree_map y); split.
+  by rewrite -xyE -/(branch_apx x n.+1); exact: tree_map_apx.
+by rewrite -/(branch_apx y n.+1); exact: tree_map_apx.
+Qed.
+
+Let tree_map_inj : (forall n U, trivIset [set: K n] (@refine_apx n U)) ->
   set_inj [set: T] tree_map.
 Proof.
 move=> triv x y _ _ xyE; apply: functional_extensionality_dep => n.
 suff : forall n, branch_apx x n = branch_apx y n.
-  move=> brE; have := @triv n (branch_apx x n) (x n) (y n) I I; apply.
-  exists (tree_map y); split.
-    by rewrite -?xyE -/(branch_apx x n.+1); apply: tree_map_apx.
-  by rewrite brE -/(branch_apx y n.+1); apply: tree_map_apx.
+  move=> brE; apply: (@triv n (branch_apx x n) _ _ I I).
+  by rewrite [in X in _ `&` X]brE; exact: tree_map_setI.
 elim => // m /= brE.
-have -> := @triv m (branch_apx x m) (x m) (y m) I I; first by rewrite brE.
-exists (tree_map y); split.
-  by rewrite -?xyE -/(branch_apx x m.+1); apply: tree_map_apx.
-by rewrite brE -/(branch_apx y m.+1); apply: tree_map_apx.
+rewrite (@triv m (branch_apx x m) (x m) (y m) I I) 1?brE//.
+by rewrite -[in X in X `&` _]brE; exact: tree_map_setI.
 Qed.
 
 Lemma tree_map_props : exists (f : T -> X),
   [/\ continuous f,
       set_surj [set: T] [set: X] f &
       (forall n U, trivIset [set: K n] (@refine_apx n U)) ->
-        set_inj [set: T] f
-  ].
+        set_inj [set: T] f].
 Proof.
 exists tree_map; split.
 - exact: tree_map_cts.
@@ -240,91 +241,87 @@ End topological_trees.
 
 (*
   Part 2: We can use `tree_map_props` to build a homeomorphism from the
-  cantor_space to a cantor-like space T.
+  cantor_space to a Cantor-like space T.
 *)
 
 Section TreeStructure.
 Context {R : realType} {T : pseudoMetricType R}.
 Hypothesis cantorT : cantor_like T.
-Let dsctT : zero_dimensional T.
-Proof. by case: cantorT. Qed.
-Let pftT : perfect_set [set: T].
-Proof. by case: cantorT. Qed.
-Let cmptT : compact [set: T].
-Proof. by case: cantorT. Qed.
-Let hsdfT : @hausdorff_space T.
-Proof. by case: cantorT. Qed.
+
+Let dsctT : zero_dimensional T.   Proof. by case: cantorT. Qed.
+Let pftT  : perfect_set [set: T]. Proof. by case: cantorT. Qed.
+Let cmptT : compact [set: T].     Proof. by case: cantorT. Qed.
+Let hsdfT : @hausdorff_space T.   Proof. by case: cantorT. Qed.
 
 Let c_invar (U : set T) := clopen U /\ U !=set0.
 
 Let clopen_surj : $|{surjfun [set: nat] >-> @clopen T}|.
 Proof.
-suff : (@clopen T = set0 \/ $|{surjfun [set: nat] >-> @clopen T}|).
-  by case; rewrite // eqEsubset; case=>/(_ _ clopenT).
-by apply/pfcard_geP/clopen_countable/compact_second_countable; case: cantorT.
+suff : @clopen T = set0 \/ $|{surjfun [set: nat] >-> @clopen T}|.
+  by case; rewrite // eqEsubset => -[/(_ _ clopenT)].
+exact/pfcard_geP/clopen_countable/compact_second_countable.
 Qed.
 
 Let U_ := unsquash clopen_surj.
 
-Let split_clopen' (U : set T) : exists V, 
+Let split_clopen' (U : set T) : exists V,
   open U -> U !=set0 -> clopen V /\ V `&` U !=set0 /\ ~`V `&` U !=set0.
 Proof.
-case: (pselect (open U)) => oU; last by exists point.
-case: (pselect (U !=set0)) => Un0; last by exists point.
+have [oU|?] := pselect (open U); last by exists point.
+have [Un0|?] := pselect (U !=set0); last by exists point.
 have [x [y] [Ux] Uy xny] := (iffLR perfect_set2) pftT U oU Un0.
-have [V [? ? ?]] := dsctT xny; exists V.
+have [V [clV Vx Vy]] := dsctT xny; exists V.
 by repeat split => //; [exists x | exists y].
 Qed.
 
 Let split_clopen (U : set T) := projT1 (cid (split_clopen' U)).
 
-Let c_ind (n : nat) (V : set T) (b : bool) :=
+Let c_ind n (V : set T) (b : bool) :=
   let Wn :=
     if pselect ((U_ n) `&` V !=set0 /\ ~` (U_ n) `&` V !=set0)
-    then (U_ n) else split_clopen V in
+    then U_ n else split_clopen V in
   (if b then Wn else ~` Wn) `&` V.
 
-Local Lemma cantor_map : exists (f : cantor_space -> T),
+Local Lemma cantor_map : exists f : cantor_space -> T,
   [/\ continuous f,
       set_surj [set: cantor_space] [set: T] f &
       set_inj [set: cantor_space] f
   ].
 Proof.
-have [] := (@tree_map_props 
-  (fun=> [topologicalType of bool]) T c_ind c_invar cmptT hsdfT).
-- done.
-- move=> n V; rewrite eqEsubset; split => t; last by case => ? ? [].
-  move=> Vt; case: (pselect ((U_ n) `&` V !=set0 /\ ~` (U_ n) `&` V !=set0)).
-    move=> ?; case: (pselect (U_ n t)).
-      by exists true => //; rewrite /c_ind; case pselect.
-    by exists false => //; rewrite /c_ind; case pselect.
-  move=> ?; case: (pselect (split_clopen V t)).
-    by exists true => //; rewrite /c_ind; case pselect.
-  by exists false => //; rewrite /c_ind; case pselect.
-- move=> n U e [] clU Un0; rewrite /c_ind; case: pselect.
-    case => /= ? ?; case: e => //; split => //; apply: clopenI => //.
+have [] := @tree_map_props
+    (fun=> [topologicalType of bool]) T c_ind c_invar cmptT hsdfT.
+- by [].
+- move=> n V; rewrite eqEsubset; split => [t Vt|t [? ? []]//].
+  have [?|?] := pselect (U_ n `&` V !=set0 /\ ~` U_ n `&` V !=set0).
+  + have [Unt|Unt] := pselect (U_ n t).
+    * by exists true => //; rewrite /c_ind; case: pselect.
+    * by exists false => //; rewrite /c_ind; case: pselect.
+  + have [scVt|scVt] := pselect (split_clopen V t).
+    * by exists true => //; rewrite /c_ind; case: pselect.
+    * by exists false => //; rewrite /c_ind; case: pselect.
+- move=> n U e [] clU Un0; rewrite /c_ind; case: pselect => /=.
+  + move=> [UU CUU]; case: e => //; split => //; apply: clopenI => //.
       exact: funS.
     by apply: clopenC => //; exact: funS.
-  have [| | ? [? ?]] := projT2 (cid (split_clopen' U)) => //. 
-    by case: clU.
-  move=> ?; case: e => //=; (split; first apply: clopenI) => //; exact: clopenC.
+  + move=> _; have [|//|clscU [scUU CscUU]] := projT2 (cid (split_clopen' U)).
+      by case: clU.
+    case: e; split => //; first exact: clopenI.
+    by apply: clopenI => //; exact: clopenC.
 - by move=> ? [].
-- by split;[ exact: clopenT |exists point].
+- by split; [exact: clopenT | exists point].
 - by move=> ? [[]].
 - move=> x y /dsctT [A [clA Ax Any]].
-  have [] := (@surj _ _ _ _ U_ _ clA) => n _ UnA; exists n => V e.
-  case: (pselect (V y)); last by move=> + _; apply: subsetC => ? [].
-  case: (pselect (V x)); last by move=> + _ [].
-  move=> Vx Vy; rewrite {1 2}/c_ind; case: pselect => /=; rewrite ?UnA.
+  have [n _ UnA] := @surj _ _ _ _ U_ _ clA; exists n => V e.
+  have [|+ _] := pselect (V y); last by apply: subsetC => ? [].
+  have [Vx Vy|? _ []//] := pselect (V x).
+  rewrite {1 2}/c_ind; case: pselect => /=; rewrite ?UnA.
     by move=> _; case: e; case => // ? ?; apply/not_andP; left.
   by apply: absurd; split; [exists x | exists y].
 - move=> f [ctsf surjf injf]; exists f; split => //; apply: injf.
-  move=> n U i j _ _ [z] [] [] + Uz [+ _]; case: pselect => /=.
-    by case => ? ?; case: i; case: j => //.
-  by move=> ?; case: i; case: j => //.
+  by move=> n U i j _ _ [z] [] [] + Uz [+ _]; move: i j => [] [].
 Qed.
 
-Let tree_map := projT1 (cid (cantor_map)).
+Let tree_map := projT1 (cid cantor_map).
 
 Local Lemma tree_map_bij : bijective tree_map.
 Proof.
@@ -334,13 +331,14 @@ Qed.
 #[local] HB.instance Definition _ := @BijTT.Build _ _ _ tree_map_bij.
 
 Lemma homeomorphism_cantor_like :
-  exists (f : {splitbij [set: cantor_space] >->  [set: T]}),
+  exists (f : {splitbij [set: cantor_space] >-> [set: T]}),
     continuous f /\
-    (forall A, closed A -> closed (f@`A)).
+    (forall A, closed A -> closed (f @` A)).
 Proof.
-exists tree_map => /=; have [? ? ?] := projT2 (cid cantor_map); split => //.
-move=> A clA; apply: compact_closed; first exact: hsdfT.
-apply (@continuous_compact _ _ tree_map); first exact: continuous_subspaceT.
+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.
 apply: (@subclosed_compact _ _ [set: cantor_space]) => //.
 exact: cantor_space_compact.
 Qed.
@@ -368,12 +366,11 @@ Lemma cantor_like_finite_prod (T : nat -> topologicalType) :
   cantor_like (tree_of T).
 Proof.
 move=> finiteT twoElems; split.
-- apply: (@perfect_diagonal (fun n => pointed_discrete (T n))). 
-  exact: twoElems.
+- exact/(@perfect_diagonal (pointed_discrete \o T))/twoElems.
 - have := tychonoff (fun n => finite_compact (finiteT n)).
-  by congr (compact _) => //=; rewrite eqEsubset; split => b.
-- apply (@hausdorff_product _ (fun n => pointed_discrete (T n))).
-  by move=> n; exact: discrete_hausdorff.
+  by congr (compact _) => //=; rewrite eqEsubset.
+- apply: (@hausdorff_product _ (pointed_discrete \o T)) => n.
+  exact: discrete_hausdorff.
 - by apply zero_dimension_prod => ?; exact: discrete_zero_dimension.
 Qed.
 
@@ -383,7 +380,7 @@ Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
 
 (* Part 4: Building a finitely branching tree to cover `T` *)
 Section alexandroff_hausdorff.
-Context {R: realType} {T : pseudoMetricType R}.
+Context {R : realType} {T : pseudoMetricType R}.
 
 Hypothesis cptT : compact [set: T].
 Hypothesis hsdfT : hausdorff_space T.
@@ -392,50 +389,50 @@ Section two_pointed.
 Context (t0 t1 : T).
 Hypothesis T2e : t0 != t1.
 
-Local Lemma ent_balls' (E : set (T*T)) :
-  exists (M : set (set T)),
+Local Lemma ent_balls' (E : set (T * T)) :
+  exists M : set (set T),
     entourage E -> [/\
       finite_set M,
       forall A, M A -> exists a, A a /\
-        A `<=` closure [set y | split_ent E (a,y)],
-      exists (A B : set T), M A /\ M B /\ A != B,
+        A `<=` closure [set y | split_ent E (a, y)],
+      exists A B : set T, M A /\ M B /\ A != B,
       \bigcup_(A in M) A = [set: T] &
       M `<=` closed].
 Proof.
-case: (pselect (entourage E)); last by move=> ?; exists point.
-move=> entE; move: cptT; rewrite compact_cover.
+have [entE|?] := pselect (entourage E); last by exists point.
+move: cptT; rewrite compact_cover.
 pose fs x := interior [set y | split_ent E (x, y)].
-case/(_ T [set: T] fs).
-- by move=> i _; apply: open_interior.
-- move=> t _; exists t => //.
+move=> /(_ T [ set: T] fs)[t _|t _ |].
+- exact: open_interior.
+- exists t => //.
   by rewrite /fs /interior -nbhs_entourageE; exists (split_ent E).
-move=> M' _ Mcov; exists 
-  ((fun x => closure (fs x)) @` [set` M'] `|` [set [set t0];[set t1]]).
-move=> _; split.
-- rewrite finite_setU; split; first by exact/finite_image/finite_fset.
+move=> M' _ Mcov; exists
+  ((closure \o fs) @` [set` M'] `|` [set [set t0]; [set t1]]).
+move=> _; split=> [|A [|]| | |].
+- rewrite finite_setU; split; first exact/finite_image/finite_fset.
   exact: finite_set2.
-- move=> A []; first (case=> z M'z <-; exists z; split).
+- move=> [z M'z] <-; exists z; split.
   + apply: subset_closure; apply: nbhs_singleton; apply: nbhs_interior.
     by rewrite -nbhs_entourageE; exists (split_ent E).
-  + by apply:closure_subset; exact:interior_subset.
-  + by case => ->; [exists t0 | exists t1]; split => // t ->;
-      apply: subset_closure; exact:entourage_refl.
+  + by apply: closure_subset; exact: interior_subset.
+- by case => ->; [exists t0 | exists t1]; split => // t ->;
+    apply: subset_closure; exact: entourage_refl.
 - exists [set t0], [set t1]; split;[|split].
   + by right; left.
   + by right; right.
-  + apply/eqP; rewrite eqEsubset; case=> /(_ t0) => /(_ erefl).
-    by move: T2e => /[swap] ->/eqP.
+  + apply/eqP; rewrite eqEsubset => -[] /(_ t0 erefl).
+    by move: T2e => /[swap] -> /eqP.
 - rewrite -subTset => t /Mcov [t' M't' fsxt]; exists (closure (fs t')).
-    by left; by exists t' => //.
-  by apply: subset_closure.
-- move=> ? []; first by case=> ? ? <-; exact: closed_closure.
-  by case => ->; apply: accessible_closed_set1; apply: hausdorff_accessible.
+    by left; exists t'.
+  exact: subset_closure.
+- move=> ? [[? ?] <-|]; first exact: closed_closure.
+  by move=> [|] ->; exact/accessible_closed_set1/hausdorff_accessible.
 Qed.
 
 Let ent_balls E := projT1 (cid (ent_balls' E)).
 
-Let count_unif' := (cid2
-  ((iffLR countable_uniformityP) (@countable_uniformity_metric _ T))).
+Let count_unif' := cid2
+  ((iffLR countable_uniformityP) (@countable_uniformity_metric _ T)).
 
 Let count_unif := projT1 count_unif'.
 
@@ -453,24 +450,24 @@ Qed.
 
 Hint Resolve ent_count_unif : core.
 
-Let K' (n : nat) : Type := @sigT (set T) (ent_balls (count_unif n)).
+Let K' n : Type := @sigT (set T) (ent_balls (count_unif n)).
 
 Local Lemma K'p n :  K' n.
 Proof.
 apply: cid; have [//| _ _ _ + _] := projT2 (cid (ent_balls' (count_unif n))).
-by rewrite -subTset => /(_ point I) [W Q ?]; exists W; apply Q.
+by rewrite -subTset => /(_ point I) [W Q ?]; exists W; exact: Q.
 Qed.
 
 Let K n := PointedType (classicType_choiceType (K' n)) (K'p n).
-Let Tree := (@tree_of R K).
+Let Tree := @tree_of R K.
 
 Let embed_refine n (U : set T) (k : K n) :=
-  (if (pselect (projT1 k `&` U !=set0))
+  (if pselect (projT1 k `&` U !=set0)
   then projT1 k
-  else if (pselect (exists e : K n , projT1 e `&` U !=set0)) is left e
+  else if pselect (exists e : K n , projT1 e `&` U !=set0) is left e
     then projT1 (projT1 (cid e))
     else set0) `&` U.
-Let embed_invar (U : set T) := closed U /\ U!=set0.
+Let embed_invar (U : set T) := closed U /\ U !=set0.
 
 Local Lemma Kn_closed n (e : K n) : closed (projT1 e).
 Proof.
@@ -478,84 +475,83 @@ case: e => W; have [//| _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
 exact.
 Qed.
 
-Local Lemma cantor_surj_pt1 : exists (f : Tree -> T),
+Local Lemma cantor_surj_pt1 : exists f : Tree -> T,
   continuous f /\ set_surj [set: Tree] [set: T] f.
 Proof.
 pose entn n := projT2 (cid (ent_balls' (count_unif n))).
-have [] := (@tree_map_props (fun (n : nat) => @pointed_discrete R (K n))
-  T (embed_refine) (embed_invar) cptT hsdfT).
-- done.
-- move=> n U; rewrite eqEsubset; split; last by move => t [? ? []].
-  move=> t Ut; have [//|_ _ _ + _] := entn n; rewrite -subTset.
-  case/(_ t I) => W cbW Wt; exists (existT _ W cbW) => //.
+have [] := @tree_map_props (@pointed_discrete R \o K) T (embed_refine)
+    (embed_invar) cptT hsdfT.
+- by [].
+- move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
+  have [//|_ _ _ + _] := entn n; rewrite -subTset.
+  move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //.
   by rewrite /embed_refine; case: pselect => //=; apply: absurd; exists t.
 - move=> n U e [clU Un0]; split.
     apply: closedI => //; case: pselect => //= ?; first exact: Kn_closed.
-    case: pselect; last by move=> ?; exact: closed0.
-    move=> ?; exact: Kn_closed.
-  rewrite /embed_refine; case: pselect => //=  ?; case: pselect.
-    by case => i [z [pz bz]]; set P := cid _; have := projT2 P; apply.
+    by case: pselect => ?; [exact: Kn_closed|exact: closed0].
+  rewrite /embed_refine; case: pselect => //= ?; case: pselect.
+    by case=> i [z [pz bz]]; set P := cid _; have := projT2 P; apply.
   case: Un0 => z Uz; apply: absurd.
-  have [//|_ _ _ + _] := entn n; rewrite -subTset; case/(_ z I)=> i bi iz.
-  by exists (existT _ _ bi); exists z.
+  have [//|_ _ _ + _] := entn n; rewrite -subTset; move=> /(_ z I)[i bi iz].
+  by exists (existT _ _ bi), z.
 - by move => ? [].
 - by split; [exact: closedT | exists point].
 - by move => ? [].
 - move=> x y xny; move: hsdfT; rewrite open_hausdorff.
-  case/(_ _ _ xny); case => U V /= [/set_mem Ux /set_mem Vy] [oU oV UVI0].
-  move: oU; rewrite openE => /(_ _ Ux); rewrite /interior -nbhs_entourageE.
-  case => E entE ExU; have [//| n ctE] := 
+  move=> /(_ _ _ xny)[[U V]] /= [/set_mem Ux /set_mem Vy] [+ oV UVI0].
+  rewrite openE => /(_ _ Ux); rewrite /interior -nbhs_entourageE => -[E entE ExU].
+  have [//| n ctE] :=
     @count_unif_sub ((split_ent E) `&` ((split_ent E)^-1%classic)).
     exact: filterI.
-  exists n => B [C ebC]; have [//|_ Csub _ _ _] := entn n => embx emby.
-  have [[D cbD] /= [Dx Dy]] : exists (e : K n), projT1 e x /\ projT1 e y.
+  exists n => B [C ebC]; have [//|_ Csub _ _ _ embx emby] := entn n.
+  have [[D cbD] /= Dx Dy] : exists2 e : K n, projT1 e x & projT1 e y.
     move: embx emby; rewrite /embed_refine; case: pselect => /=.
-      by move => ? [? ?] [? ?]; exists (existT _ _ ebC); split.
-    case: pselect ; last by move => ? ? [].
+      by move=> ? [? ?] [? ?]; exists (existT _ _ ebC).
+    case: pselect; last by move => ? ? [].
     by move=> e _ [? ?] [? ?]; exists (projT1 (cid e)).
-  suff : E (x, y).
-    by move/ExU; move/eqP/disjoints_subset:UVI0 => /[apply].
+  suff : E (x, y) by move/ExU; move/eqP/disjoints_subset: UVI0 => /[apply].
   have [z [Dz DzE]] := Csub _ cbD.
-  have /ent_closure:= DzE _ Dx => /(_ (ent_count_unif n))/ctE [_ /= ?].
-  have /ent_closure:= DzE _ Dy => /(_ (ent_count_unif n))/ctE [? _].
+  have /ent_closure:= DzE _ Dx => /(_ (ent_count_unif n))/ctE [_ /= Exz].
+  have /ent_closure:= DzE _ Dy => /(_ (ent_count_unif n))/ctE [Ezy _].
   exact: (@entourage_split [uniformType of T] z).
 by move=> f [ctsf surjf _]; exists f.
 Qed.
 
 Local Lemma cantor_surj_pt2 :
-  exists (f : {surj [set: cantor_space] >->  [set: Tree]}), continuous f.
+  exists (f : {surj [set: cantor_space] >-> [set: Tree]}), continuous f.
 Proof.
-have [] := @homeomorphism_cantor_like R Tree; first last.
-  by move=> f [ctsf _]; exists f.
-apply: (@cantor_like_finite_prod _ (fun n => @pointed_discrete R (K n))).
-  move=> n /=; have [// | fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
+have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f.
+apply: (@cantor_like_finite_prod _ (@pointed_discrete R \o K)) => [n /=|n].
+  have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
   suff -> : [set: {classic K' n}] =
       (@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))).
-    by apply: finite_preimage => //; move=> ? ? _ _; apply: eq_sigT_hprop.
-  by rewrite eqEsubset; split => //; case=> W p.
-move=> n; have [// | _ _ [A [B [pA [pB AB]]]] _ _] :=
+    by apply: finite_preimage => // ? ? _ _; exact: eq_sigT_hprop.
+  by rewrite eqEsubset; split => // -[].
+have [//| _ _ [A [B [pA [pB AB]]]] _ _] :=
   projT2 (cid (ent_balls' (count_unif n))).
-simpl; exists ((existT _ _ pA), (existT _ _ pB)).
-by move: AB; apply: contra_neq; apply: EqdepFacts.eq_sigT_fst.
+exists (existT _ _ pA, existT _ _ pB) => /=.
+by move: AB; apply: contra_neq => -[].
 Qed.
 
 Local Lemma cantor_surj_twop :
-  exists (f : {surj [set: cantor_space] >->  [set: T]}), continuous f.
+  exists (f : {surj [set: cantor_space] >-> [set: T]}), continuous f.
 Proof.
-case: cantor_surj_pt2 => f ctsf; case: cantor_surj_pt1.
-move => g [ctsg /Psurj [sjg gsjg]]; exists [surj of sjg \o f].
-by move=> z; apply continuous_comp; [apply: ctsf|rewrite -gsjg; apply: ctsg].
+move: cantor_surj_pt2 cantor_surj_pt1 => -[f ctsf] [g [ctsg /Psurj [sjg gsjg]]].
+exists [surj of sjg \o f] => z.
+by apply continuous_comp; [exact: ctsf|rewrite -gsjg; exact: ctsg].
 Qed.
+
 End two_pointed.
 
 (* The Alexandroff-Hausdorff theorem*)
 Theorem cantor_surj :
   exists (f : {surj [set: cantor_space] >->  [set: T]}), continuous f.
 Proof.
-case: (pselect (exists (p : T), p != point)).
-  by case => p ppt; apply: cantor_surj_twop; exact: ppt.
-move=> /forallNP xpt; have : set_surj [set: cantor_space] [set: T] (cst point).
-  by move=> q _; exists point => //; have /negP := xpt q; rewrite negbK => /eqP.
-by case/Psurj => f cstf; exists f; rewrite -cstf; apply: cst_continuous.
+have [[p ppt]|/forallNP xpt] := pselect (exists p : T, p != point).
+  by apply: cantor_surj_twop; exact: ppt.
+have /Psurj[f cstf] : set_surj [set: cantor_space] [set: T] (cst point).
+  by move=> q _; exists point => //; have /negP/negPn/eqP -> := xpt q.
+by exists f; rewrite -cstf; exact: cst_continuous.
 Qed.
-End alexandroff_hausdorff.
\ No newline at end of file
+
+End alexandroff_hausdorff.
diff --git a/theories/topology.v b/theories/topology.v
index 2c375ff7cf..7005e51061 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3216,7 +3216,7 @@ Lemma compact_precompact (A B : set X) :
   hausdorff_space X -> compact A -> precompact A.
 Proof.
 move=> h c; rewrite precompactE ( _ : closure A = A)//.
-apply/esym/closure_id; exact: compact_closed.
+by apply/esym/closure_id; exact: compact_closed.
 Qed.
 
 Lemma precompact_closed (A : set X) : closed A -> precompact A = compact A.
@@ -3671,7 +3671,7 @@ exists (fun i => if i is false then A `\` C else A `&` C); split.
   + rewrite setIC; apply/disjoints_subset; rewrite closureC => x [? ?].
     by exists C => //; split=> //; rewrite setDE setCI setCK; right.
   + apply/disjoints_subset => y -[Ay Cy].
-    rewrite -BAC BAD=> /closureI[_]; rewrite -(proj1 (@closure_id _ _) cD)=> Dy.
+    rewrite -BAC BAD => /closureI[_]; move/closure_id : cD => <- Dy.
     by have : B y; [by rewrite BAD; split|rewrite BAC => -[]].
 Qed.
 
@@ -4363,14 +4363,6 @@ Qed.
 
 End uniform_closeness.
 
-Lemma ent_closure {X : uniformType} (x : X) E : entourage E ->
-  closure (to_set (split_ent E) x) `<=` to_set E x.
-Proof.
-pose E' := ((split_ent E) `&` ((split_ent E)^-1)%classic).
-move=> entE z /(_ [set y | E' (z, y)]) [].
-  by rewrite -nbhs_entourageE; exists E' => //; apply: filterI.
-by move=> y [/=] + [_]; apply: entourage_split.
-Qed.
 Definition unif_continuous (U V : uniformType) (f : U -> V) :=
   (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.