--- a/src/HOL/Analysis/Determinants.thy Sun Jan 01 00:45:55 2023 +0000
+++ b/src/HOL/Analysis/Determinants.thy Sun Jan 01 01:43:02 2023 +0000
@@ -1026,7 +1026,7 @@
using \<open>A *v axis k 1 = a\<close> that by auto
next
from obtain_subset_with_card_n[OF 2] obtain h i::'n where "h \<noteq> i"
- by (auto simp add: eval_nat_numeral card_Suc_eq)
+ by (fastforce simp add: eval_nat_numeral card_Suc_eq)
then obtain j where "j \<noteq> k"
by (metis (full_types))
let ?TA = "transpose A"
--- a/src/HOL/Analysis/Path_Connected.thy Sun Jan 01 00:45:55 2023 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Sun Jan 01 01:43:02 2023 +0000
@@ -2497,8 +2497,7 @@
by (simp add: inner_commute)
qed
obtain S :: "'a set" where "S \<subseteq> Basis" and "card S = Suc (Suc 0)"
- using obtain_subset_with_card_n[OF assms]
- by auto
+ using obtain_subset_with_card_n[OF assms] by (force simp add: eval_nat_numeral)
then obtain b0 b1 :: 'a where "b0 \<in> Basis" and "b1 \<in> Basis" and "b0 \<noteq> b1"
unfolding card_Suc_eq by auto
then have "a + b0 - b1 \<in> ?A \<inter> ?B"