From 0de8ae2be7a04a044bd752b0d9e9cb017b922d8b Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Thu, 9 Dec 2021 00:38:43 +0100
Subject: [PATCH] fix

- removed useless `setC1E` (it is convertible and `inE` yields the same result)
- removed `mem_setC_subset` which was a duplicate of `setC_subset_set1C`
- generalized and renamed the latter to `subsetC1`
- removed all uses of `-in_setE`
---
 CHANGELOG_UNRELEASED.md   |  4 +++-
 theories/classical_sets.v | 19 ++++++-------------
 theories/topology.v       | 10 +++++-----
 3 files changed, 14 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 334111628a..e1ec6449e8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,12 +8,14 @@
   + lemma `setDIr`
   + lemmas `setMT`, `setTM`, `setMI`
   + lemmas `setSM`, `setM_bigcupr`, `setM_bigcupl`
-  + lemmas `setC1E`, `mem_setC_subset`
 - in `topology.v`:
   + definitions `kolmogorov`, `accessible`
   + lemmas `accessible_closed_set1`, `accessible_kolmogorov`
 
 ### Changed
+- in `topology.v`:
+  + renamed and generalized `setC_subset_set1C` implication to
+    equivalence `subsetC1`
 
 - in `normedtype.v`:
   + `nbhs_minfty_lt` renamed to `nbhs_ninfty_lt_pos` and changed to not use `{posnum R}`
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index fe61f2b518..5603535fb5 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -44,7 +44,7 @@ Require Import boolp.
 (*                        A.`2 == set of points a such that there exists b so *)
 (*                                that A (b, a).                              *)
 (*                        ~` A == complement of A.                            *)
-(*                   [set ~ a] == complement of [set a].                      *)
+(*                    [set~ a] == complement of [set a].                      *)
 (*                     A `\` B == complement of B in A.                       *)
 (*                      A `\ a == A deprived of a.                            *)
 (*          \bigcup_(i in P) F == union of the elements of the family F whose *)
@@ -492,10 +492,11 @@ Proof. by rewrite subsets_disjoint setCK. Qed.
 
 Lemma setCT : ~` setT = set0 :> set T. Proof. by rewrite -setC0 setCK. Qed.
 
-Lemma setC1E (x : T) : [set ~ x] = [set y | y <> x]. Proof. by []. Qed.
-
-Lemma mem_setC_subset (x : T) A : x \in ~` A -> A `<=` [set ~ x].
-Proof. by rewrite in_setE => + y Ay; apply: contra_not => <-. Qed.
+Lemma subsetC1 x A : (A `<=` [set~ x]) = (x \in ~` A).
+Proof.
+rewrite !inE; apply/propext; split; first by move/[apply]; apply.
+by move=> NAx y; apply: contraPnot => ->.
+Qed.
 
 Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.
 
@@ -600,14 +601,6 @@ Qed.
 Lemma nonsubset A B : ~ (A `<=` B) -> A `&` ~` B !=set0.
 Proof. by rewrite -setD_eq0 setDE -set0P => /eqP. Qed.
 
-Lemma setC_subset_set1C (x : T) (A : set T) : x \in ~` A -> A `<=` [set ~ x].
-Proof.
-  rewrite in_setE /set1 => ? y yInH //= ; rewrite /setC => //= xEqy.
-  have: (A `&` ~` A) y.
-     rewrite /setI => //= ; split; by [rewrite xEqy|].
-  by rewrite setICr.
-Qed.
-
 Lemma setU_eq0 A B : (A `|` B = set0) = ((A = set0) /\ (B = set0)).
 Proof. by rewrite -!subset0 subUset. Qed.
 
diff --git a/theories/topology.v b/theories/topology.v
index e9f55ce1d1..67bc7f9053 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -2924,15 +2924,15 @@ Definition accessible := forall x y, x != y ->
 Lemma accessible_closed_set1 : accessible -> forall x, closed [set x].
 Proof.
 move=> T1 x; rewrite -[X in closed X]setCK; apply: closedC.
-rewrite openE setC1E => y /eqP /T1 [U [oU [yU xU]]].
-rewrite /interior nbhsE /=; exists U; split; last exact: mem_setC_subset.
-by split => //; rewrite -in_setE.
+rewrite openE => y /eqP /T1 [U [oU [yU xU]]].
+rewrite /interior nbhsE /=; exists U; split; last by rewrite subsetC1.
+by split=> //; rewrite inE in yU.
 Qed.
 
 Definition accessible_kolmogorov : accessible -> kolmogorov.
 Proof.
-move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split => //.
-by rewrite nbhsE inE /=; exists A; split => //; split => //; rewrite -in_setE.
+move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //.
+by rewrite nbhsE inE; exists A; do !split=> //; rewrite inE in xA.
 Qed.
 
 Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.