# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1572727914 0
# Node ID b86d307078377e01382e068135448d7e88f46174
# Parent  9d0712c748349904df89eb9016a42b21a21d7914
just tidied one proof

diff -r 9d0712c74834 -r b86d30707837 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sat Nov 02 18:47:00 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Sat Nov 02 20:51:54 2019 +0000
@@ -3162,14 +3162,8 @@
     assume "z \<in> ?lhs"
     have *: "z = (fst z, snd z)"
       by auto
-    have "z \<in> ?rhs"
-      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms \<open>z \<in> ?lhs\<close>
-      apply auto
-      apply (rule_tac x = "fst z" in exI)
-      apply (rule_tac x = x in exI)
-      using *
-      apply auto
-      done
+    then have "z \<in> ?rhs"
+      using rel_interior_convex_cone_aux[of S "fst z" "snd z"] assms \<open>z \<in> ?lhs\<close> by fastforce
   }
   moreover
   {