diff -r 5bf9a1b78f93 -r c8597292cd41 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Mon Jan 30 10:15:01 2023 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Mon Jan 30 15:24:17 2023 +0000
@@ -805,17 +805,15 @@
     using h unfolding ring_iso_def bij_betw_def inj_on_def by auto
 
   have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
-      using bij_betw_inv_into h ring_iso_def by fastforce
+    by (simp add: bij_betw_inv_into h ring_iso_memE(5))
 
-  show "inv_into (carrier R) h \<in> ring_iso S R"
-    apply (rule ring_iso_memI)
-    apply (simp add: h_surj inv_into_into)
-       apply (auto simp add: h_inv_bij)
-    using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] 
-    apply (simp_all add: \<open>ring R\<close> bij_betw_def bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules(5))
-    using ring_iso_memE [OF h] bij_betw_inv_into_right [of h "carrier R" "carrier S"]
-    apply (simp add: \<open>ring R\<close> inv_into_f_eq ring.ring_simprules(1))
-    by (simp add: \<open>ring R\<close> inv_into_f_eq ring.ring_simprules(6))
+  have "inv_into (carrier R) h \<in> ring_hom S R"
+    using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] \<open>ring R\<close>
+    by (simp add: bij_betw_imp_inj_on bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules ring_hom_memI)
+  moreover have "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
+    using h_inv_bij by force
+    ultimately show "inv_into (carrier R) h \<in> ring_iso S R"
+      by (simp add: ring_iso_def)
 qed
 
 corollary ring_iso_sym: