lint compact_normal_local

theories/topology.v

@@ -3653,48 +3653,45 @@ have /closure_id -> : closed (~` B); first by exact: open_closedC.
 by apply/closure_subset/disjoints_subset; rewrite setIC.
 Qed.
 
-Lemma compact_normal_local (K : set T) : compact K -> 
+Lemma compact_normal_local (K : set T) : compact K ->
   forall A : set T, A `<=` interior K ->
   {for A, normal_space}.
 Proof.
-move=> cptV A AK clA B; have /compact_near_coveringP cvA : compact A. 
-  apply: (subclosed_compact _ cptV) => //.
-  by apply: subset_trans; last exact: interior_subset.
-have snbC : forall (U : set T), Filter (filter_from (set_nbhs U) closure).
-  move=> U; apply: filter_from_filter; first by exists setT; apply: filterT.
-  move=> P Q  sAP sAQ; exists (P `&` Q); last exact: closureI.
-  exact: (@filterI _ _ (@set_nbhs_filter _ U)).
-move=> snAB; case : (pselect (~`B!=set0)); first last.
-  move=> nB0; suff -> : B = setT by exact: (@filterT _ _ (snbC A)).
-  by rewrite -subTset => t _; move: nB0; apply: contra_notP => nBt; exists t.
-case=> b0 B0; have PsnA : ProperFilter (filter_from (set_nbhs (~`B)) closure).
-  apply:filter_from_proper; move=> ? P. 
+move=> cptV A AK clA B snAB; have /compact_near_coveringP cvA : compact A.
+  apply/(subclosed_compact clA cptV)/(subset_trans AK).
+  exact: interior_subset.
+have snbC (U : set T) : Filter (filter_from (set_nbhs U) closure).
+  apply: filter_from_filter; first by exists setT; apply: filterT.
+  by move=> P Q sAP sAQ; exists (P `&` Q); [apply filterI|exact: closureI].
+have [/(congr1 setC)|/set0P[b0 B0]] := eqVneq (~` B) set0.
+  by rewrite setCK setC0 => ->; exact: filterT.
+have PsnA : ProperFilter (filter_from (set_nbhs (~`B)) closure).
+  apply: filter_from_proper => ? P.
   by exists b0; apply/subset_closure; apply: nbhs_singleton; apply: P.
 pose F := powerset_filter_from (filter_from (set_nbhs (~` B)) closure).
 have PF : Filter F by exact: powerset_filter_from_filter.
-have cvP : (forall x, A x -> \forall x' \near x & i \near F, (~` i) x').
-  move=> x Ax; near_simpl; case/set_nbhsP: snAB => C [oC AC CB].
+have cvP (x : T) : A x -> \forall x' \near x & i \near F, (~` i) x'.
+  move=> Ax; case/set_nbhsP: snAB => C [oC AC CB].
   have [] := @compact_regular x _ cptV _ C; first exact: AK.
     by rewrite nbhsE /=; exists C => //; split => //; apply: AC.
-  move=> D /nbhs_interior nD cDC. 
+  move=> D /nbhs_interior nD cDC.
   have snBD : filter_from (set_nbhs (~` B)) closure (closure (~` (closure D))).
-    exists (closure (~` closure D)) => z.
+    exists (closure (~` closure D)) => [z|].
       move=> nBZ; apply: filterS; first exact: subset_closure.
-      apply: open_nbhs_nbhs; split => //; first exact/closed_openC/closed_closure.
-      by move=> nCD; apply: nBZ; apply/CB/cDC.
-    by have := (@closed_closure _ (~` closure D)); rewrite closure_id => <-.
+      apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure.
+      exact/(subsetC _ nBZ)/(subset_trans cDC).
+    by have := @closed_closure _ (~` closure D); rewrite closure_id => <-.
   near=> y U => /=; have Dy : interior D y by exact: (near nD _).
   have UclD : U `<=` closure (~` closure D).
     exact: (near (small_set_sub snBD) U).
   move=> Uy; have [z [/= + Dz]] := UclD _ Uy _ Dy.
   by apply; apply: subset_closure.
-case/(_ _ _ _ _ cvP): cvA => R /= [RA Rmono [U RU] RBx]. 
+case/(_ _ _ _ _ cvP): cvA => R /= [RA Rmono [U RU] RBx].
 have [V /set_nbhsP [W [oW cBW WV] clVU]] := RA _ RU; exists (~` W).
-  apply/set_nbhsP; exists (~` closure W); split => //.
-    exact/closed_openC/closed_closure.
-  move=> y Ay; have := RBx _ RU y Ay => Uy Wy.
-  by apply: Uy; apply: clVU; apply: (closure_subset WV).
-  apply: subsetC; apply: subset_closure.
+  apply/set_nbhsP; exists (~` closure W); split.
+  - exact/closed_openC/closed_closure.
+  - by move=> y /(RBx _ RU) + Wy; apply; exact/clVU/(closure_subset WV).
+  - by apply: subsetC; exact/subset_closure.
 have : closed (~` W) by exact: open_closedC.
 by rewrite closure_id => <-; apply: subsetCl.
 Unshelve. all: by end_near. Qed.
@@ -7345,4 +7342,4 @@ move=> lcpt hsdfX [x|] [y|] //=.
   by case => ? /[swap] /Some_inj <-.
 Qed.
 
-End one_point_compactification.
+End one_point_compactification.