--- a/src/HOL/Algebra/Free_Abelian_Groups.thy Mon Mar 01 14:47:08 2021 +0000
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy Mon Mar 01 17:59:17 2021 +0000
@@ -682,7 +682,7 @@
by (auto simp: PiE_def Pi_def in_keys_iff)
then show "(\<lambda>i\<in>I. Abs_poly_mapping (?f i))
\<in> {x \<in> \<Pi>\<^sub>E i\<in>I. {c. Poly_Mapping.keys c \<subseteq> S i}. finite {i \<in> I. x i \<noteq> 0}}"
- using fin unfolding J_def by (simp add: eq in_keys_iff cong: conj_cong)
+ using fin unfolding J_def by (force simp add: eq in_keys_iff cong: conj_cong)
qed
qed
then show "carrier ?H \<subseteq> ?h ` carrier ?G"