--- a/src/HOL/Vector_Spaces.thy Fri Sep 25 12:05:21 2020 +0100
+++ b/src/HOL/Vector_Spaces.thy Fri Sep 25 14:11:48 2020 +0100
@@ -1453,7 +1453,7 @@
have "b \<notin> f ` B1" using vs2.span_base[of b "f ` B1"] b by auto
then have "Suc (card B1) = card (insert b (f ` B1))"
- using sf[THEN inj_on_subset, of B1] by (subst card_insert) (auto intro: vs1.finite_Basis simp: card_image)
+ using sf[THEN inj_on_subset, of B1] by (subst card.insert_remove) (auto intro: vs1.finite_Basis simp: card_image)
also have "\<dots> = vs2.dim (insert b (f ` B1))"
using vs2.dim_eq_card_independent[OF **] by simp
also have "vs2.dim (insert b (f ` B1)) \<le> vs2.dim B2"