src/HOL/Multivariate_Analysis/Euclidean_Space.thy

       apply (rule span_setsum[OF C(1)])
       apply clarify
       apply (rule span_mul)
       by (rule span_superset)}
   then have SC: "span ?C = span (insert a B)"
-    unfolding expand_set_eq span_breakdown_eq C(3)[symmetric] by auto
+    unfolding set_ext_iff span_breakdown_eq C(3)[symmetric] by auto
   thm pairwise_def
   {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
     {assume xa: "x = ?a" and ya: "y = ?a"
       have "orthogonal x y" using xa ya xy by blast}
     moreover

   from linear_independent_extend[OF independent_injective_image, OF independent_basis, OF lf fi]
   obtain h:: "'b => 'a" where h: "linear h"
     " \<forall>x \<in> f ` basis ` {..<DIM('a)}. h x = inv f x" by blast
   from h(2)
   have th: "\<forall>i<DIM('a). (h \<circ> f) (basis i) = id (basis i)"
-    using inv_o_cancel[OF fi, unfolded expand_fun_eq id_def o_def]
+    using inv_o_cancel[OF fi, unfolded ext_iff id_def o_def]
     by auto
 
   from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]
   have "h o f = id" .
   then show ?thesis using h(1) by blast

   from linear_independent_extend[OF independent_basis[where 'a='b],of "inv f"]
   obtain h:: "'b \<Rightarrow> 'a" where
     h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
   from h(2)
   have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
-    using sf by(auto simp add: surj_iff o_def expand_fun_eq)
+    using sf by(auto simp add: surj_iff o_def ext_iff)
   from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
   have "f o h = id" .
   then show ?thesis using h(1) by blast
 qed
 

   finally show "f = h" unfolding fg by simp
 qed
 
 lemma isomorphism_expand:
   "f o g = id \<and> g o f = id \<longleftrightarrow> (\<forall>x. f(g x) = x) \<and> (\<forall>x. g(f x) = x)"
-  by (simp add: expand_fun_eq o_def id_def)
+  by (simp add: ext_iff o_def id_def)
 
 lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space"
   assumes lf: "linear f" and fi: "inj f"
   shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
 unfolding isomorphism_expand[symmetric]

   shows "f o f' = id \<longleftrightarrow> f' o f = id"
 proof-
   {fix f f':: "'a => 'a"
     assume lf: "linear f" "linear f'" and f: "f o f' = id"
     from f have sf: "surj f"
-      apply (auto simp add: o_def expand_fun_eq id_def surj_def)
+      apply (auto simp add: o_def ext_iff id_def surj_def)
       by metis
     from linear_surjective_isomorphism[OF lf(1) sf] lf f
-    have "f' o f = id" unfolding expand_fun_eq o_def id_def
+    have "f' o f = id" unfolding ext_iff o_def id_def
       by metis}
   then show ?thesis using lf lf' by metis
 qed
 
 text {* Moreover, a one-sided inverse is automatically linear. *}
 
 lemma left_inverse_linear: fixes f::"'a::euclidean_space => 'a::euclidean_space"
   assumes lf: "linear f" and gf: "g o f = id"
   shows "linear g"
 proof-
-  from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def expand_fun_eq)
+  from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def ext_iff)
     by metis
   from linear_injective_isomorphism[OF lf fi]
   obtain h:: "'a \<Rightarrow> 'a" where
     h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
   have "h = g" apply (rule ext) using gf h(2,3)
-    apply (simp add: o_def id_def expand_fun_eq)
+    apply (simp add: o_def id_def ext_iff)
     by metis
   with h(1) show ?thesis by blast
 qed
 
 subsection {* Infinity norm *}