--- a/src/HOL/Homology/Brouwer_Degree.thy	Thu Feb 22 21:42:02 2024 +0100
+++ b/src/HOL/Homology/Brouwer_Degree.thy	Fri Feb 23 09:11:31 2024 +0100
@@ -1299,7 +1299,7 @@
     if x: "x \<in> carrier ?G" for x
   proof -
     obtain n::int where xeq: "x = pow ?G a n"
-      using carra x aeq by moura
+      using carra x aeq by auto
     show ?thesis
       by (simp add: xeq a d hom_int_pow int_pow_pow mult.commute)
   qed