merged
authorpaulson
Fri Jul 13 17:27:05 2018 +0100 (2 months ago)
changeset 68627e371784becd9
parent 68623 b942da0962c2
parent 68626 330c0ec897a4
child 68628 958511f53de8
merged
src/HOL/Vector_Spaces.thy
     1.1 --- a/src/HOL/Divides.thy	Fri Jul 13 15:42:18 2018 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Jul 13 17:27:05 2018 +0100
     1.3 @@ -26,16 +26,17 @@
     1.4      simp add: ac_simps sgn_1_pos sgn_1_neg)
     1.5  
     1.6  lemma unique_quotient_lemma:
     1.7 -  "b * q' + r' \<le> b * q + r \<Longrightarrow> 0 \<le> r' \<Longrightarrow> r' < b \<Longrightarrow> r < b \<Longrightarrow> q' \<le> (q::int)"
     1.8 -apply (subgoal_tac "r' + b * (q'-q) \<le> r")
     1.9 - prefer 2 apply (simp add: right_diff_distrib)
    1.10 -apply (subgoal_tac "0 < b * (1 + q - q') ")
    1.11 -apply (erule_tac [2] order_le_less_trans)
    1.12 - prefer 2 apply (simp add: right_diff_distrib distrib_left)
    1.13 -apply (subgoal_tac "b * q' < b * (1 + q) ")
    1.14 - prefer 2 apply (simp add: right_diff_distrib distrib_left)
    1.15 -apply (simp add: mult_less_cancel_left)
    1.16 -done
    1.17 +  assumes "b * q' + r' \<le> b * q + r" "0 \<le> r'" "r' < b" "r < b" shows "q' \<le> (q::int)"
    1.18 +proof -
    1.19 +  have "r' + b * (q'-q) \<le> r"
    1.20 +    using assms by (simp add: right_diff_distrib)
    1.21 +  moreover have "0 < b * (1 + q - q') "
    1.22 +    using assms by (simp add: right_diff_distrib distrib_left)
    1.23 +  moreover have "b * q' < b * (1 + q)"
    1.24 +    using assms by (simp add: right_diff_distrib distrib_left)
    1.25 +  ultimately show ?thesis
    1.26 +    using assms by (simp add: mult_less_cancel_left)
    1.27 +qed
    1.28  
    1.29  lemma unique_quotient_lemma_neg:
    1.30    "b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
    1.31 @@ -43,10 +44,9 @@
    1.32  
    1.33  lemma unique_quotient:
    1.34    "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
    1.35 -  apply (simp add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
    1.36 -  apply (blast intro: order_antisym
    1.37 -    dest: order_eq_refl [THEN unique_quotient_lemma]
    1.38 -    order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
    1.39 +  apply (rule order_antisym)
    1.40 +   apply (simp_all add: eucl_rel_int_iff linorder_neq_iff split: if_split_asm)
    1.41 +     apply (blast intro: order_eq_refl [THEN unique_quotient_lemma] order_eq_refl [THEN unique_quotient_lemma_neg] sym)+
    1.42    done
    1.43  
    1.44  lemma unique_remainder:
     2.1 --- a/src/HOL/Vector_Spaces.thy	Fri Jul 13 15:42:18 2018 +0200
     2.2 +++ b/src/HOL/Vector_Spaces.thy	Fri Jul 13 17:27:05 2018 +0100
     2.3 @@ -281,16 +281,9 @@
     2.4  qed
     2.5  
     2.6  lemma in_span_delete:
     2.7 -  assumes a: "a \<in> span S"
     2.8 -    and na: "a \<notin> span (S - {b})"
     2.9 +  assumes a: "a \<in> span S" and na: "a \<notin> span (S - {b})"
    2.10    shows "b \<in> span (insert a (S - {b}))"
    2.11 -  apply (rule in_span_insert)
    2.12 -  apply (rule set_rev_mp)
    2.13 -  apply (rule a)
    2.14 -  apply (rule span_mono)
    2.15 -  apply blast
    2.16 -  apply (rule na)
    2.17 -  done
    2.18 +  by (metis Diff_empty Diff_insert0 a in_span_insert insert_Diff na)
    2.19  
    2.20  lemma span_redundant: "x \<in> span S \<Longrightarrow> span (insert x S) = span S"
    2.21    unfolding span_def by (rule hull_redundant)
    2.22 @@ -484,7 +477,7 @@
    2.23        have \<open>b \<in> span C\<close>
    2.24          using \<open>b \<in> B\<close> unfolding eq[symmetric] by (rule span_base)
    2.25        have \<open>(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) =
    2.26 -          (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s (\<Sum>w | ?R v w \<noteq> 0. ?R v w *s w))\<close>
    2.27 +           (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s (\<Sum>w | ?R v w \<noteq> 0. ?R v w *s w))\<close>
    2.28          by (simp add: scale_sum_right)
    2.29        also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. ?R' b v *s v)\<close>
    2.30          by (auto simp: sum_nonzero_representation_eq B eq span_base representation_ne_zero)
    2.31 @@ -492,15 +485,13 @@
    2.32          by (rule sum_nonzero_representation_eq[OF C \<open>b \<in> span C\<close>])
    2.33        finally have "?R b b = ?R (\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. (?R' b v * ?R v w) *s w) b"
    2.34          by simp
    2.35 +      also have "... = (\<Sum>i\<in>{v. ?R' b v \<noteq> 0}. ?R (\<Sum>w | ?R i w \<noteq> 0. (?R' b i * ?R i w) *s w) b)"
    2.36 +        by (subst representation_sum[OF B])  (auto intro: span_sum span_scale span_base representation_ne_zero)
    2.37 +      also have "... = (\<Sum>i\<in>{v. ?R' b v \<noteq> 0}.
    2.38 +           \<Sum>j \<in> {w. ?R i w \<noteq> 0}. ?R ((?R' b i * ?R i j ) *s  j ) b)"
    2.39 +        by (subst representation_sum[OF B]) (auto simp add: span_sum span_scale span_base representation_ne_zero)
    2.40        also have \<open>\<dots> = (\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. ?R' b v * ?R v w * ?R w b)\<close>
    2.41 -        using B \<open>b \<in> B\<close>
    2.42 -        apply (subst representation_sum[OF B])
    2.43 -         apply (fastforce intro: span_sum span_scale span_base representation_ne_zero)
    2.44 -        apply (rule sum.cong[OF refl])
    2.45 -        apply (subst representation_sum[OF B])
    2.46 -         apply (simp add: span_sum span_scale span_base representation_ne_zero)
    2.47 -        apply (simp add: representation_scale[OF B] span_base representation_ne_zero)
    2.48 -        done
    2.49 +        using B \<open>b \<in> B\<close> by (simp add: representation_scale[OF B] span_base representation_ne_zero)
    2.50        finally have "(\<Sum>v | ?R' b v \<noteq> 0. \<Sum>w | ?R v w \<noteq> 0. ?R' b v * ?R v w * ?R w b) \<noteq> 0"
    2.51          using representation_basis[OF B \<open>b \<in> B\<close>] by auto
    2.52        then obtain v w where bv: "?R' b v \<noteq> 0" and vw: "?R v w \<noteq> 0" and "?R' b v * ?R v w * ?R w b \<noteq> 0"
    2.53 @@ -516,7 +507,7 @@
    2.54      proof (subst B_eq, rule card_of_UNION_ordLeq_infinite[OF \<open>infinite C\<close>])
    2.55        show "ordLeq3 (card_of C) (card_of C)"
    2.56          by (intro ordLeq_refl card_of_Card_order)
    2.57 -      show "\<forall>c\<in>C. ordLeq3 (card_of {v. representation B c v \<noteq> 0}) (card_of C)"
    2.58 +      show "\<forall>c\<in>C. ordLeq3 (card_of {v. ?R c v \<noteq> 0}) (card_of C)"
    2.59          by (intro ballI ordLeq3_finite_infinite \<open>infinite C\<close> finite_representation)
    2.60      qed }
    2.61    from this[of B C] this[of C B] B C eq \<open>infinite C\<close> \<open>infinite B\<close>
    2.62 @@ -584,10 +575,9 @@
    2.63  
    2.64  lemma subspace_sums: "\<lbrakk>subspace S; subspace T\<rbrakk> \<Longrightarrow> subspace {x + y|x y. x \<in> S \<and> y \<in> T}"
    2.65    apply (simp add: subspace_def)
    2.66 -  apply (intro conjI impI allI)
    2.67 -  using add.right_neutral apply blast
    2.68 -   apply clarify
    2.69 -   apply (metis add.assoc add.left_commute)
    2.70 +  apply (intro conjI impI allI; clarsimp simp: algebra_simps)
    2.71 +  using add.left_neutral apply blast
    2.72 +   apply (metis add.assoc)
    2.73    using scale_right_distrib by blast
    2.74  
    2.75  end
    2.76 @@ -876,10 +866,10 @@
    2.77      proof (rule vector_space_pair.linear_eq_on[where x=v])
    2.78        show "vector_space_pair ( *a) ( *a)" by unfold_locales
    2.79        show "linear ( *a) ( *a) (?g \<circ> f)"
    2.80 -        apply (rule Vector_Spaces.linear_compose[of _ "( *b)"])
    2.81 -        subgoal by unfold_locales
    2.82 -        apply fact
    2.83 -        done
    2.84 +      proof (rule Vector_Spaces.linear_compose[of _ "( *b)"])
    2.85 +        show "linear ( *a) ( *b) f"
    2.86 +          by unfold_locales
    2.87 +      qed fact
    2.88        show "linear ( *a) ( *a) id" by (rule vs1.linear_id)
    2.89        show "v \<in> vs1.span B" by fact
    2.90        show "b \<in> B \<Longrightarrow> (p.construct (f ` B) (the_inv_into B f) \<circ> f) b = id b" for b
    2.91 @@ -915,10 +905,7 @@
    2.92      proof (rule vector_space_pair.linear_eq_on[where x=v])
    2.93        show "vector_space_pair ( *b) ( *b)" by unfold_locales
    2.94        show "linear ( *b) ( *b) (f \<circ> ?g)"
    2.95 -        apply (rule Vector_Spaces.linear_compose[of _ "( *a)"])
    2.96 -        apply fact
    2.97 -        subgoal by fact
    2.98 -        done
    2.99 +        by (rule Vector_Spaces.linear_compose[of _ "( *a)"]) fact+
   2.100        show "linear ( *b) ( *b) id" by (rule vs2.linear_id)
   2.101        have "vs2.span (f ` B) = vs2.span C"
   2.102          using fB_C vs2.span_mono[of C "f ` B"] vs2.span_minimal[of "f`B" "vs2.span C"]
   2.103 @@ -1035,8 +1022,7 @@
   2.104            by (metis member_remove remove_def)
   2.105        qed
   2.106        also have " \<dots> \<le> card (S - {y})"
   2.107 -        apply (rule card_image_le)
   2.108 -        using fS by simp
   2.109 +        by (simp add: card_image_le fS)
   2.110        also have "\<dots> \<le> card S - 1" using y fS by simp
   2.111        finally show False using S0 by arith
   2.112      qed
   2.113 @@ -1076,22 +1062,23 @@
   2.114      case False
   2.115      obtain B where B: "B \<subseteq> span S" "independent B" "span S \<subseteq> span B" "card B = dim (span S)"
   2.116        using basis_exists [of "span S"] by blast
   2.117 -    have 1: "insert x B \<subseteq> span (insert x S)"
   2.118 -      by (meson B(1) insertI1 insert_subset order_trans span_base span_mono subset_insertI)
   2.119 -    have 2: "span (insert x S) \<subseteq> span (insert x B)"
   2.120 -      by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
   2.121 -    have 3: "independent (insert x B)"
   2.122 -      by (metis B(1-3) independent_insert span_subspace subspace_span False)
   2.123      have "dim (span (insert x S)) = Suc (dim S)"
   2.124 -      apply (rule dim_unique [OF 1 2 3])
   2.125 -      by (metis B False card_insert_disjoint dim_span finiteI_independent span_base span_eq span_span)
   2.126 +    proof (rule dim_unique)
   2.127 +      show "insert x B \<subseteq> span (insert x S)"
   2.128 +        by (meson B(1) insertI1 insert_subset order_trans span_base span_mono subset_insertI)
   2.129 +      show "span (insert x S) \<subseteq> span (insert x B)"
   2.130 +        by (metis \<open>B \<subseteq> span S\<close> \<open>span S \<subseteq> span B\<close> span_breakdown_eq span_subspace subsetI subspace_span)
   2.131 +      show "independent (insert x B)"
   2.132 +        by (metis B(1-3) independent_insert span_subspace subspace_span False)
   2.133 +      show "card (insert x B) = Suc (dim S)"
   2.134 +        using B False finiteI_independent by force
   2.135 +    qed
   2.136      then show ?thesis
   2.137        by (metis False Suc_eq_plus1 dim_span)
   2.138    qed
   2.139  qed
   2.140  
   2.141 -lemma dim_singleton [simp]:
   2.142 -  "dim{x} = (if x = 0 then 0 else 1)"
   2.143 +lemma dim_singleton [simp]: "dim{x} = (if x = 0 then 0 else 1)"
   2.144    by (simp add: dim_insert)
   2.145  
   2.146  proposition choose_subspace_of_subspace:
   2.147 @@ -1109,9 +1096,10 @@
   2.148      then show ?case
   2.149      proof (cases "span S \<subseteq> span T")
   2.150        case True
   2.151 -      have "dim S = dim T"
   2.152 -        apply (rule span_eq_dim [OF subset_antisym [OF True]])
   2.153 +      have "span T \<subseteq> span S"
   2.154          by (simp add: \<open>T \<subseteq> span S\<close> span_minimal)
   2.155 +      then have "dim S = dim T"
   2.156 +        by (rule span_eq_dim [OF subset_antisym [OF True]])
   2.157        then show ?thesis
   2.158          using Suc.prems \<open>dim T = n\<close> by linarith
   2.159      next
   2.160 @@ -1122,8 +1110,7 @@
   2.161          by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_superset span_mono span_span)
   2.162        with \<open>dim T = n\<close>  \<open>subspace T\<close> y show ?thesis
   2.163          apply (rule_tac x="span(insert y T)" in exI)
   2.164 -        apply (auto simp: dim_insert)
   2.165 -        using span_eq_iff by blast
   2.166 +        using span_eq_iff by (fastforce simp: dim_insert)
   2.167      qed
   2.168    qed
   2.169    with that show ?thesis by blast
   2.170 @@ -1268,15 +1255,12 @@
   2.171  
   2.172  lemma independent_explicit:
   2.173    shows "independent B \<longleftrightarrow> finite B \<and> (\<forall>c. (\<Sum>v\<in>B. c v *s v) = 0 \<longrightarrow> (\<forall>v \<in> B. c v = 0))"
   2.174 -  apply (cases "finite B")
   2.175 -   apply (force simp: dependent_finite)
   2.176    using independent_bound_general
   2.177 -  apply auto
   2.178 -  done
   2.179 +  by (fastforce simp: dependent_finite)
   2.180  
   2.181  proposition dim_sums_Int:
   2.182    assumes "subspace S" "subspace T"
   2.183 -  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T"
   2.184 +  shows "dim {x + y |x y. x \<in> S \<and> y \<in> T} + dim(S \<inter> T) = dim S + dim T" (is "dim ?ST + _ = _")
   2.185  proof -
   2.186    obtain B where B: "B \<subseteq> S \<inter> T" "S \<inter> T \<subseteq> span B"
   2.187               and indB: "independent B"
   2.188 @@ -1289,29 +1273,28 @@
   2.189    then have "finite B" "finite C" "finite D"
   2.190      by (simp_all add: finiteI_independent indB independent_bound_general)
   2.191    have Beq: "B = C \<inter> D"
   2.192 -    apply (rule sym)
   2.193 -    apply (rule spanning_subset_independent)
   2.194 -    using \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> apply blast
   2.195 -    apply (meson \<open>independent C\<close> independent_mono inf.cobounded1)
   2.196 -    using B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> apply auto
   2.197 -    done
   2.198 +  proof (rule spanning_subset_independent [symmetric])
   2.199 +    show "independent (C \<inter> D)"
   2.200 +      by (meson \<open>independent C\<close> independent_mono inf.cobounded1)
   2.201 +  qed (use B \<open>C \<subseteq> S\<close> \<open>D \<subseteq> T\<close> \<open>B \<subseteq> C\<close> \<open>B \<subseteq> D\<close> in auto)
   2.202    then have Deq: "D = B \<union> (D - C)"
   2.203      by blast
   2.204 -  have CUD: "C \<union> D \<subseteq> {x + y |x y. x \<in> S \<and> y \<in> T}"
   2.205 -    apply safe
   2.206 -    apply (metis add.right_neutral subsetCE \<open>C \<subseteq> S\<close> \<open>subspace T\<close> set_eq_subset span_zero span_minimal)
   2.207 -    apply (metis add.left_neutral subsetCE \<open>D \<subseteq> T\<close> \<open>subspace S\<close> set_eq_subset span_zero span_minimal)
   2.208 -    done
   2.209 +  have CUD: "C \<union> D \<subseteq> ?ST"
   2.210 +  proof (simp, intro conjI)
   2.211 +    show "C \<subseteq> ?ST"
   2.212 +      using span_zero span_minimal [OF _ \<open>subspace T\<close>] \<open>C \<subseteq> S\<close> by force
   2.213 +    show "D \<subseteq> ?ST"
   2.214 +      using span_zero span_minimal [OF _ \<open>subspace S\<close>] \<open>D \<subseteq> T\<close> by force
   2.215 +  qed
   2.216    have "a v = 0" if 0: "(\<Sum>v\<in>C. a v *s v) + (\<Sum>v\<in>D - C. a v *s v) = 0"
   2.217                   and v: "v \<in> C \<union> (D-C)" for a v
   2.218    proof -
   2.219 +    have CsS: "\<And>x. x \<in> C \<Longrightarrow> a x *s x \<in> S"
   2.220 +      using \<open>C \<subseteq> S\<close> \<open>subspace S\<close> subspace_scale by auto
   2.221      have eq: "(\<Sum>v\<in>D - C. a v *s v) = - (\<Sum>v\<in>C. a v *s v)"
   2.222        using that add_eq_0_iff by blast
   2.223      have "(\<Sum>v\<in>D - C. a v *s v) \<in> S"
   2.224 -      apply (subst eq)
   2.225 -      apply (rule subspace_neg [OF \<open>subspace S\<close>])
   2.226 -      apply (rule subspace_sum [OF \<open>subspace S\<close>])
   2.227 -      by (meson subsetCE subspace_scale \<open>C \<subseteq> S\<close> \<open>subspace S\<close>)
   2.228 +      by (simp add: eq CsS \<open>subspace S\<close> subspace_neg subspace_sum)
   2.229      moreover have "(\<Sum>v\<in>D - C. a v *s v) \<in> T"
   2.230        apply (rule subspace_sum [OF \<open>subspace T\<close>])
   2.231        by (meson DiffD1 \<open>D \<subseteq> T\<close> \<open>subspace T\<close> subset_eq subspace_def)
   2.232 @@ -1350,8 +1333,7 @@
   2.233          using Beq \<open>(\<Sum>x\<in>C - B. a x *s x) = 0\<close> f3 f4 by auto
   2.234      qed
   2.235      with 0 have Dcc0: "(\<Sum>v\<in>D. a v *s v) = 0"
   2.236 -      apply (subst Deq)
   2.237 -      by (simp add: \<open>finite B\<close> \<open>finite D\<close> sum_Un)
   2.238 +      by (subst Deq) (simp add: \<open>finite B\<close> \<open>finite D\<close> sum_Un)
   2.239      then have D0: "\<And>v. v \<in> D \<Longrightarrow> a v = 0"
   2.240        using independent_explicit \<open>independent D\<close> \<open>finite D\<close> by blast
   2.241      show ?thesis
   2.242 @@ -1368,10 +1350,13 @@
   2.243      by (metis \<open>C \<subseteq> S\<close> \<open>independent C\<close> \<open>S \<subseteq> span C\<close> basis_card_eq_dim)
   2.244    moreover have "dim T = card D"
   2.245      by (metis \<open>D \<subseteq> T\<close> \<open>independent D\<close> \<open>T \<subseteq> span D\<close> basis_card_eq_dim)
   2.246 -  moreover have "dim {x + y |x y. x \<in> S \<and> y \<in> T} = card(C \<union> D)"
   2.247 -    apply (rule dim_unique [OF CUD _ indCUD refl], clarify)
   2.248 -    apply (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_superset span_minimal subsetCE subspace_span sup.bounded_iff)
   2.249 -    done
   2.250 +  moreover have "dim ?ST = card(C \<union> D)"
   2.251 +  proof -
   2.252 +    have *: "\<And>x y. \<lbrakk>x \<in> S; y \<in> T\<rbrakk> \<Longrightarrow> x + y \<in> span (C \<union> D)"
   2.253 +      by (meson \<open>S \<subseteq> span C\<close> \<open>T \<subseteq> span D\<close> span_add span_mono subsetCE sup.cobounded1 sup.cobounded2)
   2.254 +    show ?thesis
   2.255 +      by (auto intro: * dim_unique [OF CUD _ indCUD refl])
   2.256 +  qed
   2.257    ultimately show ?thesis
   2.258      using \<open>B = C \<inter> D\<close> [symmetric]
   2.259      by (simp add:  \<open>independent C\<close> \<open>independent D\<close> card_Un_Int finiteI_independent)
   2.260 @@ -1396,20 +1381,16 @@
   2.261      by blast
   2.262    from B(4) have d: "dim UNIV = card B"
   2.263      by simp
   2.264 -  have th: "UNIV \<subseteq> span (f ` B)"
   2.265 -    apply (rule card_ge_dim_independent)
   2.266 -      apply blast
   2.267 -    using B(2) inj_on_subset[OF fi]
   2.268 -     apply (rule lf.independent_inj_on_image)
   2.269 -     apply blast
   2.270 -    apply (rule order_eq_refl)
   2.271 -    apply (rule sym)
   2.272 -    unfolding d
   2.273 -    apply (rule card_image)
   2.274 -    apply (rule subset_inj_on[OF fi])
   2.275 -    apply blast
   2.276 -    done
   2.277 -  from th show ?thesis
   2.278 +  have "UNIV \<subseteq> span (f ` B)"
   2.279 +  proof (rule card_ge_dim_independent)
   2.280 +    show "independent (f ` B)"
   2.281 +      by (simp add: B(2) fi lf.independent_inj_image)
   2.282 +    have "card (f ` B) = dim UNIV"
   2.283 +      by (metis B(1) card_image d fi inj_on_subset)
   2.284 +    then show "dim UNIV \<le> card (f ` B)"
   2.285 +      by simp
   2.286 +  qed blast
   2.287 +  then show ?thesis
   2.288      unfolding lf.span_image surj_def
   2.289      using B(3) by blast
   2.290  qed
   2.291 @@ -1535,38 +1516,19 @@
   2.292      and fi: "inj f"
   2.293      and dims: "vs2.dim UNIV = vs1.dim UNIV"
   2.294    shows "\<exists>f'. linear s2 s1 f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
   2.295 -proof -
   2.296 -  show ?thesis
   2.297 -    unfolding isomorphism_expand[symmetric]
   2.298 -    using linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
   2.299 -      linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV fi]
   2.300 -    apply (auto simp: module_hom_iff_linear)
   2.301 -    subgoal for f' f''
   2.302 -      apply (rule exI[where x=f''])
   2.303 -      using linear_injective_imp_surjective[OF lf fi dims]
   2.304 -      apply auto
   2.305 -      by (metis comp_apply eq_id_iff surj_def)
   2.306 -    done
   2.307 -qed
   2.308 +  unfolding isomorphism_expand[symmetric]
   2.309 +  using linear_injective_imp_surjective[OF lf fi dims]
   2.310 +  using fi left_right_inverse_eq lf linear_injective_left_inverse linear_surjective_right_inverse by blast
   2.311  
   2.312  lemma linear_surjective_isomorphism:
   2.313    assumes lf: "linear s1 s2 f"
   2.314      and sf: "surj f"
   2.315      and dims: "vs2.dim UNIV = vs1.dim UNIV"
   2.316    shows "\<exists>f'. linear s2 s1 f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
   2.317 -proof -
   2.318 -  show ?thesis
   2.319 -    unfolding isomorphism_expand[symmetric]
   2.320 -    using linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
   2.321 -      linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV]
   2.322 -    using linear_surjective_imp_injective[OF lf sf dims] sf
   2.323 -    apply (auto simp: module_hom_iff_linear)
   2.324 -    subgoal for f' f''
   2.325 -      apply (rule exI[where x=f''])
   2.326 -      apply auto
   2.327 -      by (metis isomorphism_expand)
   2.328 -    done
   2.329 -qed
   2.330 +  using linear_surjective_imp_injective[OF lf sf dims] sf
   2.331 +    linear_exists_right_inverse_on[OF lf vs1.subspace_UNIV]
   2.332 +    linear_exists_left_inverse_on[OF lf vs1.subspace_UNIV]
   2.333 +    dims lf linear_injective_isomorphism by auto
   2.334  
   2.335  lemma basis_to_basis_subspace_isomorphism:
   2.336    assumes s: "vs1.subspace S"
   2.337 @@ -1674,12 +1636,8 @@
   2.338    from linear_surjective_isomorphism[OF lf fi]
   2.339    obtain h:: "'b \<Rightarrow> 'b" where h: "linear scale scale h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x"
   2.340      by blast
   2.341 -  have "h = g"
   2.342 -    apply (rule ext)
   2.343 -    using gf h(2,3)
   2.344 -    apply (simp add: o_def id_def fun_eq_iff)
   2.345 -    apply metis
   2.346 -    done
   2.347 +  then have "h = g"
   2.348 +    by (metis gf isomorphism_expand left_right_inverse_eq)
   2.349    with h(1) show ?thesis by blast
   2.350  qed
   2.351