src/HOL/Analysis/Linear_Algebra.thy

   show "f (a - b) = f a - f b" by (rule f.diff)
   show "f 0 = 0" by (rule f.zero)
   show "f (- a) = - f a" by (rule f.minus)
   show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
 qed
-
-lemma bounded_linearI:
-  assumes "\<And>x y. f (x + y) = f x + f y"
-    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
-    and "\<And>x. norm (f x) \<le> norm x * K"
-  shows "bounded_linear f"
-  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
 
 subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
 
 definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
   where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"

     and fi: "inj_on f B"
     and xsB: "x \<in> span B"
     and fx: "f x = 0"
   shows "x = 0"
   using fB ifB fi xsB fx
-proof (induct arbitrary: x rule: finite_induct[OF fB])
-  case 1
+proof (induction B arbitrary: x rule: finite_induct)
+  case empty
   then show ?case by auto
 next
-  case (2 a b x)
-  have fb: "finite b" using "2.prems" by simp
+  case (insert a b x)
   have th0: "f ` b \<subseteq> f ` (insert a b)"
-    apply (rule image_mono)
-    apply blast
-    done
-  from independent_mono[ OF "2.prems"(2) th0]
-  have ifb: "independent (f ` b)"  .
+    by (simp add: subset_insertI)
+  have ifb: "independent (f ` b)"
+    using independent_mono insert.prems(1) th0 by blast  
   have fib: "inj_on f b"
-    apply (rule subset_inj_on [OF "2.prems"(3)])
-    apply blast
-    done
-  from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)]
+    using insert.prems(2) by blast
+  from span_breakdown[of a "insert a b", simplified, OF insert.prems(3)]
   obtain k where k: "x - k*\<^sub>R a \<in> span (b - {a})"
     by blast
   have "f (x - k*\<^sub>R a) \<in> span (f ` b)"
     unfolding span_linear_image[OF lf]
-    apply (rule imageI)
-    using k span_mono[of "b - {a}" b]
-    apply blast
-    done
+    using "insert.hyps"(2) k by auto
   then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
     by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
   then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
-    using "2.prems"(5) by simp
+    using insert.prems(4) by simp
   have xsb: "x \<in> span b"
   proof (cases "k = 0")
     case True
     with k have "x \<in> span (b - {a})" by simp
     then show ?thesis using span_mono[of "b - {a}" b]
       by blast
   next
     case False
-    with span_mul[OF th, of "- 1/ k"]
-    have th1: "f a \<in> span (f ` b)"
-      by auto
-    from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
-    have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
-    from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
-    have "f a \<notin> span (f ` b)" using tha
-      using "2.hyps"(2)
-      "2.prems"(3) by auto
-    with th1 have False by blast
+    from inj_on_image_set_diff[OF insert.prems(2), of "insert a b " "{a}", symmetric]
+    have "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
+    then have "f a \<notin> span (f ` b)" 
+      using dependent_def insert.hyps(2) insert.prems(1) by fastforce
+    moreover have "f a \<in> span (f ` b)"
+      using False span_mul[OF th, of "- 1/ k"] by auto
+    ultimately have False
+      by blast
     then show ?thesis by blast
   qed
-  from "2.hyps"(3)[OF fb ifb fib xsb "2.prems"(5)] show "x = 0" .
+  show "x = 0" 
+    using ifb fib xsb insert.IH insert.prems(4) by blast
 qed
 
 text \<open>Can construct an isomorphism between spaces of same dimension.\<close>
 
 lemma subspace_isomorphism:

   shows "f x y = g x y"
 proof -
   let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
   from bf bg have sp: "subspace ?P"
     unfolding bilinear_def linear_iff subspace_def bf bg
-    by (auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def
+    by (auto simp add: bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add 
       intro: bilinear_ladd[OF bf])
-
   have sfg: "\<And>x. x \<in> B \<Longrightarrow> subspace {a. f x a = g x a}"
     apply (auto simp add: subspace_def)
     using bf bg unfolding bilinear_def linear_iff
     apply (auto simp add: bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add 
       intro: bilinear_ladd[OF bf])
     done
   have "\<forall>y\<in> span C. f x y = g x y" if "x \<in> span B" for x
     apply (rule span_induct [OF that sp])
-    apply (rule ballI)
-    apply (erule span_induct)
-    apply (simp_all add: sfg fg)
-    done
+    using fg sfg span_induct by blast
   then show ?thesis
     using SB TC assms by auto
 qed
 
 lemma bilinear_eq_stdbasis:

     and ST: "f ` S \<subseteq> T"
   shows "(\<forall>y \<in> T. \<exists>x \<in> S. f x = y) \<longleftrightarrow> inj_on f S"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume h: "?lhs"
-  {
-    fix x y
-    assume x: "x \<in> S"
-    assume y: "y \<in> S"
-    assume f: "f x = f y"
+  { fix x y
+    assume x: "x \<in> S" and y: "y \<in> S" and f: "f x = f y"
     from x fS have S0: "card S \<noteq> 0"
       by auto
     have "x = y"
     proof (rule ccontr)
       assume xy: "\<not> ?thesis"
       have th: "card S \<le> card (f ` (S - {y}))"
         unfolding c
-        apply (rule card_mono)
-        apply (rule finite_imageI)
-        using fS apply simp
-        using h xy x y f unfolding subset_eq image_iff
-        apply auto
-        apply (case_tac "xa = f x")
-        apply (rule bexI[where x=x])
-        apply auto
-        done
+      proof (rule card_mono)
+        show "finite (f ` (S - {y}))"
+          by (simp add: fS)
+        show "T \<subseteq> f ` (S - {y})"
+          using h xy x y f unfolding subset_eq image_iff
+          by (metis member_remove remove_def)
+      qed
       also have " \<dots> \<le> card (S - {y})"
         apply (rule card_image_le)
         using fS by simp
       also have "\<dots> \<le> card S - 1" using y fS by simp
       finally show False using S0 by arith

   then show ?rhs
     unfolding inj_on_def by blast
 next
   assume h: ?rhs
   have "f ` S = T"
-    apply (rule card_subset_eq[OF fT ST])
-    unfolding card_image[OF h]
-    apply (rule c)
-    done
+    by (simp add: ST c card_image card_subset_eq fT h)
   then show ?lhs by blast
 qed
 
 lemma linear_surjective_imp_injective:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
-  assumes lf: "linear f"
-    and sf: "surj f"
+  assumes lf: "linear f" and sf: "surj f"
   shows "inj f"
 proof -
   let ?U = "UNIV :: 'a set"
   from basis_exists[of ?U] obtain B
     where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" and d: "card B = dim ?U"
     by blast
   {
     fix x
-    assume x: "x \<in> span B"
-    assume fx: "f x = 0"
+    assume x: "x \<in> span B" and fx: "f x = 0"
     from B(2) have fB: "finite B"
       using independent_bound by auto
+    have Uspan: "UNIV \<subseteq> span (f ` B)"
+      by (simp add: B(3) lf sf spanning_surjective_image)
     have fBi: "independent (f ` B)"
-      apply (rule card_le_dim_spanning[of "f ` B" ?U])
-      apply blast
-      using sf B(3)
-      unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
-      apply blast
-      using fB apply blast
-      unfolding d[symmetric]
-      apply (rule card_image_le)
-      apply (rule fB)
-      done
+    proof (rule card_le_dim_spanning)
+      show "card (f ` B) \<le> dim ?U"
+        using card_image_le d fB by fastforce
+    qed (use fB Uspan in auto)
     have th0: "dim ?U \<le> card (f ` B)"
-      apply (rule span_card_ge_dim)
-      apply blast
-      unfolding span_linear_image[OF lf]
-      apply (rule subset_trans[where B = "f ` UNIV"])
-      using sf unfolding surj_def
-      apply blast
-      apply (rule image_mono)
-      apply (rule B(3))
-      apply (metis finite_imageI fB)
-      done
+      by (rule span_card_ge_dim) (use Uspan fB in auto)
     moreover have "card (f ` B) \<le> card B"
       by (rule card_image_le, rule fB)
     ultimately have th1: "card B = card (f ` B)"
       unfolding d by arith
     have fiB: "inj_on f B"
-      unfolding surjective_iff_injective_gen[OF fB finite_imageI[OF fB] th1 subset_refl, symmetric]
-      by blast
+      by (simp add: eq_card_imp_inj_on fB th1)
     from linear_indep_image_lemma[OF lf fB fBi fiB x] fx
     have "x = 0" by blast
   }
   then show ?thesis
-    unfolding linear_injective_0[OF lf]
-    using B(3)
-    by blast
+    unfolding linear_injective_0[OF lf] using B(3) by blast
 qed
 
 text \<open>Hence either is enough for isomorphism.\<close>
 
 lemma left_right_inverse_eq:

   {
     fix f f':: "'a \<Rightarrow> 'a"
     assume lf: "linear f" "linear f'"
     assume f: "f \<circ> f' = id"
     from f have sf: "surj f"
-      apply (auto simp add: o_def id_def surj_def)
-      apply metis
-      done
+      by (auto simp add: o_def id_def surj_def) metis
     from linear_surjective_isomorphism[OF lf(1) sf] lf f
     have "f' \<circ> f = id"
       unfolding fun_eq_iff o_def id_def by metis
   }
   then show ?thesis

   assumes lf: "linear f"
     and gf: "g \<circ> f = id"
   shows "linear g"
 proof -
   from gf have fi: "inj f"
-    apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
-    apply metis
-    done
+    by (auto simp add: inj_on_def o_def id_def fun_eq_iff) 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"
+  obtain h :: "'a \<Rightarrow> 'a" where "linear h" and 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 fun_eq_iff)
-    apply metis
-    done
-  with h(1) show ?thesis by blast
+    by (metis gf h isomorphism_expand left_right_inverse_eq)
+  with \<open>linear h\<close> show ?thesis by blast
 qed
 
 lemma inj_linear_imp_inv_linear:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes "linear f" "inj f" shows "linear (inv f)"

 
 lemma infnorm_0: "infnorm 0 = 0"
   by (simp add: infnorm_eq_0)
 
 lemma infnorm_neg: "infnorm (- x) = infnorm x"
-  unfolding infnorm_def
-  apply (rule cong[of "Sup" "Sup"])
-  apply blast
-  apply auto
-  done
+  unfolding infnorm_def by simp
 
 lemma infnorm_sub: "infnorm (x - y) = infnorm (y - x)"
-proof -
-  have "y - x = - (x - y)" by simp
-  then show ?thesis
-    by (metis infnorm_neg)
-qed
-
-lemma real_abs_sub_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
-proof -
-  have th: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
+  by (metis infnorm_neg minus_diff_eq)
+
+lemma absdiff_infnorm: "\<bar>infnorm x - infnorm y\<bar> \<le> infnorm (x - y)"
+proof -
+  have *: "\<And>(nx::real) n ny. nx \<le> n + ny \<Longrightarrow> ny \<le> n + nx \<Longrightarrow> \<bar>nx - ny\<bar> \<le> n"
     by arith
-  from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
-  have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
-    "infnorm y \<le> infnorm (x - y) + infnorm x"
-    by (simp_all add: field_simps infnorm_neg)
-  from th[OF ths] show ?thesis .
+  show ?thesis
+  proof (rule *)
+    from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
+    show "infnorm x \<le> infnorm (x - y) + infnorm y" "infnorm y \<le> infnorm (x - y) + infnorm x"
+      by (simp_all add: field_simps infnorm_neg)
+  qed
 qed
 
 lemma real_abs_infnorm: "\<bar>infnorm x\<bar> = infnorm x"
   using infnorm_pos_le[of x] by arith
 

 
 lemma infnorm_mul: "infnorm (a *\<^sub>R x) = \<bar>a\<bar> * infnorm x"
   unfolding infnorm_Max
 proof (safe intro!: Max_eqI)
   let ?B = "(\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
-  {
-    fix b :: 'a
+  { fix b :: 'a
     assume "b \<in> Basis"
     then show "\<bar>a *\<^sub>R x \<bullet> b\<bar> \<le> \<bar>a\<bar> * Max ?B"
       by (simp add: abs_mult mult_left_mono)
   next
     from Max_in[of ?B] obtain b where "b \<in> Basis" "Max ?B = \<bar>x \<bullet> b\<bar>"

   by (simp add: Basis_le_norm infnorm_Max)
 
 lemma norm_le_infnorm:
   fixes x :: "'a::euclidean_space"
   shows "norm x \<le> sqrt DIM('a) * infnorm x"
-proof -
-  let ?d = "DIM('a)"
-  have "real ?d \<ge> 0"
-    by simp
-  then have d2: "(sqrt (real ?d))\<^sup>2 = real ?d"
-    by (auto intro: real_sqrt_pow2)
-  have th: "sqrt (real ?d) * infnorm x \<ge> 0"
+  unfolding norm_eq_sqrt_inner id_def 
+proof (rule real_le_lsqrt[OF inner_ge_zero])
+  show "sqrt DIM('a) * infnorm x \<ge> 0"
     by (simp add: zero_le_mult_iff infnorm_pos_le)
-  have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)\<^sup>2"
-    unfolding power_mult_distrib d2
-    apply (subst euclidean_inner)
-    apply (subst power2_abs[symmetric])
-    apply (rule order_trans[OF sum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
-    apply (auto simp add: power2_eq_square[symmetric])
-    apply (subst power2_abs[symmetric])
-    apply (rule power_mono)
-    apply (auto simp: infnorm_Max)
-    done
-  from real_le_lsqrt[OF inner_ge_zero th th1]
-  show ?thesis
-    unfolding norm_eq_sqrt_inner id_def .
+  have "x \<bullet> x \<le> (\<Sum>b\<in>Basis. x \<bullet> b * (x \<bullet> b))"
+    by (metis euclidean_inner order_refl)
+  also have "... \<le> DIM('a) * \<bar>infnorm x\<bar>\<^sup>2"
+    by (rule sum_bounded_above) (metis Basis_le_infnorm abs_le_square_iff power2_eq_square real_abs_infnorm)
+  also have "... \<le> (sqrt DIM('a) * infnorm x)\<^sup>2"
+    by (simp add: power_mult_distrib)
+  finally show "x \<bullet> x \<le> (sqrt DIM('a) * infnorm x)\<^sup>2" .
 qed
 
 lemma tendsto_infnorm [tendsto_intros]:
   assumes "(f \<longlongrightarrow> a) F"
   shows "((\<lambda>x. infnorm (f x)) \<longlongrightarrow> infnorm a) F"
 proof (rule tendsto_compose [OF LIM_I assms])
   fix r :: real
   assume "r > 0"
   then show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (infnorm x - infnorm a) < r"
-    by (metis real_norm_def le_less_trans real_abs_sub_infnorm infnorm_le_norm)
+    by (metis real_norm_def le_less_trans absdiff_infnorm infnorm_le_norm)
 qed
 
 text \<open>Equality in Cauchy-Schwarz and triangle inequalities.\<close>
 
 lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof -
-  {
-    assume h: "x = 0"
-    then have ?thesis by simp
-  }
-  moreover
-  {
-    assume h: "y = 0"
-    then have ?thesis by simp
-  }
-  moreover
-  {
-    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
-    from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
-    have "?rhs \<longleftrightarrow>
+proof (cases "x=0")
+  case True
+  then show ?thesis 
+    by auto
+next
+  case False
+  from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"]
+  have "?rhs \<longleftrightarrow>
       (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) -
         norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) =  0)"
-      using x y
-      unfolding inner_simps
-      unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
-      apply (simp add: inner_commute)
-      apply (simp add: field_simps)
-      apply metis
-      done
-    also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
-      by (simp add: field_simps inner_commute)
-    also have "\<dots> \<longleftrightarrow> ?lhs" using x y
-      apply simp
-      apply metis
-      done
-    finally have ?thesis by blast
-  }
-  ultimately show ?thesis by blast
+    using False unfolding inner_simps
+    by (auto simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
+  also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" 
+    using False  by (simp add: field_simps inner_commute)
+  also have "\<dots> \<longleftrightarrow> ?lhs" 
+    using False by auto
+  finally show ?thesis by metis
 qed
 
 lemma norm_cauchy_schwarz_abs_eq:
   "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow>
     norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm x *\<^sub>R y = - norm y *\<^sub>R x"

 proof -
   have th: "\<And>(x::real) a. a \<ge> 0 \<Longrightarrow> \<bar>x\<bar> = a \<longleftrightarrow> x = a \<or> x = - a"
     by arith
   have "?rhs \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x \<or> norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)"
     by simp
-  also have "\<dots> \<longleftrightarrow>(x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
+  also have "\<dots> \<longleftrightarrow> (x \<bullet> y = norm x * norm y \<or> (- x) \<bullet> y = norm x * norm y)"
     unfolding norm_cauchy_schwarz_eq[symmetric]
     unfolding norm_minus_cancel norm_scaleR ..
   also have "\<dots> \<longleftrightarrow> ?lhs"
     unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps
     by auto

 qed
 
 lemma norm_triangle_eq:
   fixes x y :: "'a::real_inner"
   shows "norm (x + y) = norm x + norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
-proof -
-  {
-    assume x: "x = 0 \<or> y = 0"
-    then have ?thesis
-      by (cases "x = 0") simp_all
-  }
-  moreover
-  {
-    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
-    then have "norm x \<noteq> 0" "norm y \<noteq> 0"
-      by simp_all
-    then have n: "norm x > 0" "norm y > 0"
-      using norm_ge_zero[of x] norm_ge_zero[of y] by arith+
-    have th: "\<And>(a::real) b c. a + b + c \<noteq> 0 \<Longrightarrow> a = b + c \<longleftrightarrow> a\<^sup>2 = (b + c)\<^sup>2"
-      by algebra
-    have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
-      apply (rule th)
-      using n norm_ge_zero[of "x + y"]
-      apply arith
-      done
-    also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
-      unfolding norm_cauchy_schwarz_eq[symmetric]
-      unfolding power2_norm_eq_inner inner_simps
-      by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
-    finally have ?thesis .
-  }
-  ultimately show ?thesis by blast
+proof (cases "x = 0 \<or> y = 0")
+  case True
+  then show ?thesis 
+    by force
+next
+  case False
+  then have n: "norm x > 0" "norm y > 0"
+    by auto
+  have "norm (x + y) = norm x + norm y \<longleftrightarrow> (norm (x + y))\<^sup>2 = (norm x + norm y)\<^sup>2"
+    by simp
+  also have "\<dots> \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x"
+    unfolding norm_cauchy_schwarz_eq[symmetric]
+    unfolding power2_norm_eq_inner inner_simps
+    by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps)
+  finally show ?thesis .
 qed
 
 
 subsection \<open>Collinearity\<close>
 

   by (simp add: collinear_def)
 
 lemma collinear_2 [iff]: "collinear {x, y}"
   apply (simp add: collinear_def)
   apply (rule exI[where x="x - y"])
-  apply auto
-  apply (rule exI[where x=1], simp)
-  apply (rule exI[where x="- 1"], simp)
-  done
+  by (metis minus_diff_eq scaleR_left.minus scaleR_one)
 
 lemma collinear_lemma: "collinear {0, x, y} \<longleftrightarrow> x = 0 \<or> y = 0 \<or> (\<exists>c. y = c *\<^sub>R x)"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof -
-  {
-    assume "x = 0 \<or> y = 0"
-    then have ?thesis
-      by (cases "x = 0") (simp_all add: collinear_2 insert_commute)
-  }
-  moreover
-  {
-    assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
-    have ?thesis
-    proof
-      assume h: "?lhs"
-      then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
-        unfolding collinear_def by blast
-      from u[rule_format, of x 0] u[rule_format, of y 0]
-      obtain cx and cy where
-        cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
-        by auto
-      from cx x have cx0: "cx \<noteq> 0" by auto
-      from cy y have cy0: "cy \<noteq> 0" by auto
-      let ?d = "cy / cx"
-      from cx cy cx0 have "y = ?d *\<^sub>R x"
-        by simp
-      then show ?rhs using x y by blast
-    next
-      assume h: "?rhs"
-      then obtain c where c: "y = c *\<^sub>R x"
-        using x y by blast
-      show ?lhs
-        unfolding collinear_def c
-        apply (rule exI[where x=x])
-        apply auto
-        apply (rule exI[where x="- 1"], simp)
-        apply (rule exI[where x= "-c"], simp)
+proof (cases "x = 0 \<or> y = 0")
+  case True
+  then show ?thesis
+    by (auto simp: insert_commute)
+next
+  case False
+  show ?thesis 
+  proof
+    assume h: "?lhs"
+    then obtain u where u: "\<forall> x\<in> {0,x,y}. \<forall>y\<in> {0,x,y}. \<exists>c. x - y = c *\<^sub>R u"
+      unfolding collinear_def by blast
+    from u[rule_format, of x 0] u[rule_format, of y 0]
+    obtain cx and cy where
+      cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u"
+      by auto
+    from cx cy False have cx0: "cx \<noteq> 0" and cy0: "cy \<noteq> 0" by auto
+    let ?d = "cy / cx"
+    from cx cy cx0 have "y = ?d *\<^sub>R x"
+      by simp
+    then show ?rhs using False by blast
+  next
+    assume h: "?rhs"
+    then obtain c where c: "y = c *\<^sub>R x"
+      using False by blast
+    show ?lhs
+      unfolding collinear_def c
+      apply (rule exI[where x=x])
+      apply auto
+          apply (rule exI[where x="- 1"], simp)
+         apply (rule exI[where x= "-c"], simp)
         apply (rule exI[where x=1], simp)
-        apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
-        apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
-        done
-    qed
-  }
-  ultimately show ?thesis by blast
+       apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib)
+      apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib)
+      done
+  qed
 qed
 
 lemma norm_cauchy_schwarz_equal: "\<bar>x \<bullet> y\<bar> = norm x * norm y \<longleftrightarrow> collinear {0, x, y}"
-  unfolding norm_cauchy_schwarz_abs_eq
-  apply (cases "x=0", simp_all)
-  apply (cases "y=0", simp_all add: insert_commute)
-  unfolding collinear_lemma
-  apply simp
-  apply (subgoal_tac "norm x \<noteq> 0")
-  apply (subgoal_tac "norm y \<noteq> 0")
-  apply (rule iffI)
-  apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x")
-  apply (rule exI[where x="(1/norm x) * norm y"])
-  apply (drule sym)
-  unfolding scaleR_scaleR[symmetric]
-  apply (simp add: field_simps)
-  apply (rule exI[where x="(1/norm x) * - norm y"])
-  apply clarify
-  apply (drule sym)
-  unfolding scaleR_scaleR[symmetric]
-  apply (simp add: field_simps)
-  apply (erule exE)
-  apply (erule ssubst)
-  unfolding scaleR_scaleR
-  unfolding norm_scaleR
-  apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
-  apply (auto simp add: field_simps)
-  done
+proof (cases "x=0")
+  case True
+  then show ?thesis
+    by (auto simp: insert_commute)
+next
+  case False
+  then have nnz: "norm x \<noteq> 0"
+    by auto
+  show ?thesis
+  proof
+    assume "\<bar>x \<bullet> y\<bar> = norm x * norm y"
+    then show "collinear {0, x, y}"
+      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma 
+      by (meson eq_vector_fraction_iff nnz)
+  next
+    assume "collinear {0, x, y}"
+    with False show "\<bar>x \<bullet> y\<bar> = norm x * norm y"
+      unfolding norm_cauchy_schwarz_abs_eq collinear_lemma  by (auto simp: abs_if)
+  qed
+qed
 
 end