src/HOL/Analysis/Starlike.thy

       obtain e where e: "e > 0" "cball z e \<inter> affine hull closure S \<le> closure S"
         using z rel_interior_cball[of "closure S"] by auto
       hence *: "0 < e/norm(z-x)" using e False by auto
       define y where "y = z + (e/norm(z-x)) *\<^sub>R (z-x)"
       have yball: "y \<in> cball z e"
-        using mem_cball y_def dist_norm[of z y] e by auto
+        using y_def dist_norm[of z y] e by auto
       have "x \<in> affine hull closure S"
         using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
       moreover have "z \<in> affine hull closure S"
         using z rel_interior_subset hull_subset[of "closure S"] by blast
       ultimately have "y \<in> affine hull closure S"