src/HOL/Multivariate_Analysis/Determinants.thy

     also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
     proof-
       {fix i assume i: "i \<in> ?U"
         from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
         have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)"
-          unfolding transpose_def by (simp add: expand_fun_eq)}
+          unfolding transpose_def by (simp add: ext_iff)}
       then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
     qed
     finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
       by simp}
   then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse)

   have fU: "finite ?U" by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .
   have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
   {fix p assume p: "p \<in> ?PU - {id}"
     then have "p \<noteq> id" by simp
-    then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto
+    then obtain i where i: "p i \<noteq> i" unfolding ext_iff by auto
     from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
     from setprod_zero [OF fU ex] have "?pp p = 0" by simp}
   then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"  by blast
   from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
     unfolding det_def by (simp add: sign_id)