fix #1841

CHANGELOG_UNRELEASED.md

@@ -5,8 +5,6 @@
 ### Added
 - in order_topology.v
   + lemma `itv_closed_ends_closed`
-- in classical_sets.v
-  + lemma `in_set1_eq`
 
 - in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
@@ -165,7 +163,11 @@
 - moved from `convex.v` to `realfun.v`
   + lemma `second_derivative_convex`
 
+- in classical_sets.v
+  + lemma `in_set1` (statement changed)
+
 ### Renamed
+
 - in `set_interval.v`:
   + `itv_is_ray` -> `itv_is_open_unbounded`
   + `itv_is_bd_open` -> `itv_is_oo`

classical/classical_sets.v

@@ -422,10 +422,8 @@ Lemma nat_nonempty : [set: nat] !=set0. Proof. by exists 1%N. Qed.
 
 #[global] Hint Resolve nat_nonempty : core.
 
-Lemma in_set1_eq {T : eqType} (a : T) (x : T) : x \in [set a] = (x == a).
-Proof.
-by apply/(sameP _ idP)/(equivP idP); rewrite inE eq_opE.
-Qed.
+Lemma in_set1 {T : eqType} (a : T) (x : T) : x \in [set a] = (x == a).
+Proof. by apply/(sameP _ idP)/(equivP idP); rewrite inE eq_opE. Qed.
 
 Lemma itv_sub_in2 d (T : porderType d) (P : T -> T -> Prop) (i j : interval T) :
   [set` j] `<=` [set` i] ->
@@ -2201,9 +2199,6 @@ Proof. by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed.
 
 End bigcup_seq.
 
-Lemma in_set1 [T : finType] (x y : T) : (x \in [set y]) = (x \in [set y]%SET).
-Proof. by apply/idP/idP; rewrite !inE /= => /eqP. Qed.
-
 Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) :
   \bigcup_(t in [set` P]) f t = \big[setU/set0]_(t in P) f t.
 Proof.

theories/probability_theory/random_variable.v

@@ -189,12 +189,12 @@ have [rS|nrS] := boolP (r \in [set h k | k in S]).
     move=> [Sk]; apply: contra_neq.
     by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij).
   rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite inE; exact/invS/set_mem.
-  by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1_eq;
+  by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1;
     [rewrite pinvK// eqxx mulr1 addr0|move/negPf => ->; rewrite mulr0].
 - rewrite /sfun eseries0 => [|k k_ge0 Sk]/=.
     apply: le_anti; rewrite !lee_fin pmf_ge0/= leNgt; apply: contraNN nrS.
     by rewrite (surj_image_eq _ (set_bij_surj h_bij)) ?inE//; exact:set_bij_sub.
-  rewrite indicE in_set1_eq (_ : (r == h k) = false) ?mulr0//.
+  rewrite indicE in_set1 (_ : (r == h k) = false) ?mulr0//.
   by apply: contraNF nrS => /eqP ->; exact/image_f.
 Qed.