From 289a383669d5312466b3c05cdef48f82189c6e82 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 24 Feb 2026 12:00:10 +0900
Subject: [PATCH] fix #1841

---
 CHANGELOG_UNRELEASED.md                       | 6 ++++--
 classical/classical_sets.v                    | 9 ++-------
 theories/probability_theory/random_variable.v | 4 ++--
 3 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4aa1cac785..7d273caaaf 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/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`
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 167c0368f8..7ab2a157c7 100644
--- a/classical/classical_sets.v
+++ b/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.
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index c77a576774..98c8f1ad69 100644
--- a/theories/probability_theory/random_variable.v
+++ b/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.