From 146ef806dc9620783cfd7064f73173267bcd1d3a Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 17 Dec 2020 13:19:52 +0900
Subject: [PATCH] predeqP missing, as mentioned on Zulip, statement found in
 PR#282

---
 CHANGELOG_UNRELEASED.md   |  3 +++
 theories/classical_sets.v | 22 ++++++++++++++--------
 2 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bdc8..a45c8f0b4 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `classical_sets.v`:
+  + lemmas `predeqP`, `seteqP`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index be57d1fb4..9166fd088 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -259,13 +259,19 @@ Notation "f @^-1` A" := (preimage f A) : classical_set_scope.
 Notation "f @` A" := (image f A) : classical_set_scope.
 Notation "A !=set0" := (nonempty A) : classical_set_scope.
 
-Lemma eqEsubset T (F G : set T) : (F = G) = (F `<=` G /\ G `<=` F).
+Lemma predeqP {T} (P Q : set T) : (P = Q) <-> (forall x, P x <-> Q x).
+Proof. by rewrite predeqE. Qed.
+
+Lemma eqEsubset T (F G : set T) : (F = G) = (F `<=>` G).
 Proof.
 rewrite propeqE; split => [->|[FG GF]]; [by split|].
 by rewrite predeqE => t; split=> [/FG|/GF].
 Qed.
 
-Lemma eq_set T (P Q : T -> Prop): (forall x : T, P x = Q x) ->
+Lemma seteqP T (A B : set T) : (A = B) <-> (A `<=>` B).
+Proof. by rewrite eqEsubset. Qed.
+
+Lemma eq_set T (P Q : T -> Prop) : (forall x : T, P x = Q x) ->
   [set x | P x] = [set x | Q x].
 Proof. by move=> /funext->. Qed.
 
@@ -374,7 +380,7 @@ Lemma image_subset A B (f : A -> B) (X Y : set A) :
 Proof. by move=> XY _ [a Xa <-]; exists a => //; apply/XY. Qed.
 
 Lemma preimage_set0 T U (f : T -> U) : f @^-1` set0 = set0.
-Proof. by rewrite predeqE. Qed.
+Proof. exact/predeqP. Qed.
 
 Lemma nonempty_preimage {A B} (f : A -> B) (X : set B) :
   f @^-1` X !=set0 -> X !=set0.
@@ -398,7 +404,7 @@ Qed.
 
 Lemma preimage_setU {A B} (f : A -> B) (X Y : set B) :
   f @^-1` (X `|` Y) = f @^-1` X `|` f @^-1` Y.
-Proof. by rewrite predeqE. Qed.
+Proof. exact/predeqP. Qed.
 
 Lemma bigcup_sup A I j (P : set I) (F : I -> set A) :
   P j -> F j `<=` \bigcup_(i in P) F i.
@@ -406,15 +412,15 @@ Proof. by move=> Pj a Fja; exists j. Qed.
 
 Lemma preimage_bigcup {A B I} (P : set I) (f : A -> B) F :
   f @^-1` (\bigcup_ (i in P) F i) = \bigcup_(i in P) (f @^-1` F i).
-Proof. by rewrite predeqE. Qed.
+Proof. exact/predeqP. Qed.
 
 Lemma preimage_setI {A B} (f : A -> B) (X Y : set B) :
   f @^-1` (X `&` Y) = f @^-1` X `&` f @^-1` Y.
-Proof. by rewrite predeqE. Qed.
+Proof. exact/predeqP. Qed.
 
 Lemma preimage_bigcap {A B I} (P : set I) (f : A -> B) F :
   f @^-1` (\bigcap_ (i in P) F i) = \bigcap_(i in P) (f @^-1` F i).
-Proof. by rewrite predeqE. Qed.
+Proof. exact/predeqP. Qed.
 
 Lemma preimage_setC A B (f : A -> B) (X : set B) :
   ~` (f @^-1` X) = f @^-1` (~` X).
@@ -677,7 +683,7 @@ Lemma set0M T U (B : set U) : @set0 T `*` B = set0.
 Proof. by rewrite predeqE => -[t u]; split => // -[]. Qed.
 
 Lemma setMT {A B} : (@setT A) `*` (@setT B) = setT.
-Proof. by rewrite predeqE. Qed.
+Proof. exact/predeqP. Qed.
 
 Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
 Definition is_fun {A B} (f : A -> B -> Prop) := Logic.all (is_subset1 \o f).