diff -r fba16c509af0 -r e8c96013ea8a src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Algebra/Coset.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -673,7 +673,7 @@
   interpret group G by fact
   show ?thesis
   proof (intro equivI)
-    have "rcong H \<subseteq> carrier G \<times> carrier G"
+    show "rcong H \<subseteq> carrier G \<times> carrier G"
       by (auto simp add: r_congruent_def)
     thus "refl_on (carrier G) (rcong H)"
       by (auto simp add: r_congruent_def refl_on_def)