redefined FSet.fmember as an abbreviation based on Set.member

--- a/src/HOL/Library/FSet.thy	Tue May 16 14:16:20 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Tue May 16 22:23:05 2023 +0200
@@ -170,17 +170,20 @@
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
 
-lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
-  parametric member_transfer .
-
-lemma fmember_iff_member_fset: "x |\<in>| A \<longleftrightarrow> x \<in> fset A"
-  by (rule fmember.rep_eq)
-
-abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
+abbreviation fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) where
+  "a |\<in>| A \<equiv> a \<in> fset A"
+
+abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
+  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
 context includes lifting_syntax
 begin
 
+lemma fmember_transfer0[transfer_rule]:
+  assumes [transfer_rule]: "bi_unique A"
+  shows "(A ===> pcr_fset A ===> (=)) (\<in>) (|\<in>|)"
+  by transfer_prover
+
 lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
   parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
 
@@ -1011,9 +1014,6 @@
   shows "fset (ffilter P xs) = Collect P \<inter> fset xs"
   by transfer auto
 
-lemma notin_fset: "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
-  by (simp add: fmember_iff_member_fset)
-
 lemma inter_fset[simp]: "fset (A |\<inter>| B) = fset A \<inter> fset B"
   by (rule inf_fset.rep_eq)
 

--- a/src/HOL/Probability/Fin_Map.thy	Tue May 16 14:16:20 2023 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Tue May 16 22:23:05 2023 +0200
@@ -232,7 +232,7 @@
       case (UN B)
       then obtain b where "x \<in> b" "b \<in> B" by auto
       hence "\<exists>a\<in>?A. a \<subseteq> b" using UN by simp
-      thus ?case using \<open>b \<in> B\<close> by blast
+      thus ?case using \<open>b \<in> B\<close> by (metis Sup_upper2)
     next
       case (Basis s)
       then obtain a b where xs: "x\<in> Pi' a b" "s = Pi' a b" "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto