diff -r b87b14e885af -r 43f5dfb7fa35 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Equiv_Relations.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -264,11 +264,10 @@
   assume cd: "(c,d) \<in> r1"
   then have "c \<in> A1" "d \<in> A1"
     using \<open>equiv A1 r1\<close> by (auto elim!: equiv_type [THEN subsetD, THEN SigmaE2])
-  with assms show "\<Union> (f c ` r2 `` {a}) = \<Union> (f d ` r2 `` {a})"
-  proof (simp add: UN_equiv_class congruent2_implies_congruent)
-    show "f c a = f d a"
-      using assms cd unfolding congruent2_def equiv_def refl_on_def by blast
-  qed
+  moreover have "f c a = f d a"
+    using assms cd unfolding congruent2_def equiv_def refl_on_def by blast
+  ultimately show "\<Union> (f c ` r2 `` {a}) = \<Union> (f d ` r2 `` {a})"
+    using assms by (simp add: UN_equiv_class congruent2_implies_congruent)
 qed
 
 lemma UN_equiv_class2:
@@ -368,7 +367,7 @@
   assume ?lhs
   then show ?rhs
     unfolding proj_def quotient_def
-  proof clarsimp
+  proof safe
     fix y
     assume y: "y \<in> A" and "r `` {x} = r `` {y}"
     moreover have "y \<in> r `` {y}"