src/HOL/Multivariate_Analysis/Determinants.thy

   show ?case
     by metis
 qed
 
 
-lemma eq_id_iff[simp]: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
+lemma eq_id_iff: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
   by auto
 
 lemma det_linear_rows_setsum_lemma:
   assumes fS: "finite S"
     and fT: "finite T"

 proof (induct T arbitrary: a c set: finite)
   case empty
   have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)"
     by vector
   from empty.prems show ?case
-    unfolding th0 by simp
+    unfolding th0 by (simp add: eq_id_iff)
 next
   case (insert z T a c)
   let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
   let ?h = "\<lambda>(y,g) i. if i = z then y else g i"
   let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))"