[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) quasi_convex_projection_small_gaps:
  assumes "continuous_on {a..(b::real)} f"
          "a \<le> b"
          "quasiconvex C G"
          "\<And>t. t \<in> {a..b} \<Longrightarrow> p t \<in> proj_set (f t) G"
          "delta > deltaG(TYPE('a))"
          "d \<in> {4 * delta + 2 * C..dist (p a) (p b)}"
  shows "\<exists>t \<in> {a..b}. (dist (p a) (p t) \<in> {d - 4 * delta - 2 * C .. d})
                    \<and> (\<forall>s \<in> {a..t}. dist (p a) (p s) \<le> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "delta > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < delta
[PROOF STEP]
using assms(5) local.delta_nonneg
[PROOF STATE]
proof (prove)
using this:
deltaG TYPE('a) < delta
0 \<le> deltaG TYPE('a)

goal (1 subgoal):
 1. 0 < delta
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < delta

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < delta

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
using quasiconvexC[OF assms(3)]
[PROOF STATE]
proof (prove)
using this:
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> C

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < delta
0 \<le> C
[PROOF STEP]
have "d \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < delta
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < delta
0 \<le> C
continuous_on {a..b} f
a \<le> b
quasiconvex C G
?t \<in> {a..b} \<Longrightarrow> p ?t \<in> proj_set (f ?t) G
deltaG TYPE('a) < delta
d \<in> {4 * delta + 2 * C..dist (p a) (p b)}

goal (1 subgoal):
 1. 0 \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> d

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
text \<open>The idea is to define the desired point as the last point $u$ for which there is a projection
  at distance at most $d$ of the starting point. Then the projection can not be much closer to
  the starting point, or one could point another such point further away by almost continuity, giving
  a contradiction. The technical implementation requires some care, as the "last point" may not
  satisfy the property, for lack of continuity. If it does, then fine. Otherwise, one should go just
  a little bit to its left to find the desired point.\<close>
[PROOF STATE]
proof (state)
this:
0 \<le> d

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
define I where "I = {t \<in> {a..b}. \<forall>s \<in> {a..t}. dist (p a) (p s) \<le> d}"
[PROOF STATE]
proof (state)
this:
I = {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "a \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> I
[PROOF STEP]
using \<open>a \<le> b\<close> \<open>d \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> b
0 \<le> d

goal (1 subgoal):
 1. a \<in> I
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
a \<le> b
0 \<le> d

goal (1 subgoal):
 1. a \<in> {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> I

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "bdd_above I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above I
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bdd_above I

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
define u where "u = Sup I"
[PROOF STATE]
proof (state)
this:
u = Sup I

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "a \<le> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> u
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> Sup I
[PROOF STEP]
apply (rule cSup_upper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<in> I
 2. bdd_above I
[PROOF STEP]
using \<open>a \<in> I\<close> \<open>bdd_above I\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> I
bdd_above I

goal (2 subgoals):
 1. a \<in> I
 2. bdd_above I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> u

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "u \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> b
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup I \<le> b
[PROOF STEP]
apply (rule cSup_least)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. I \<noteq> {}
 2. \<And>x. x \<in> I \<Longrightarrow> x \<le> b
[PROOF STEP]
using \<open>a \<in> I\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> I

goal (2 subgoals):
 1. I \<noteq> {}
 2. \<And>x. x \<in> I \<Longrightarrow> x \<le> b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> I; a \<in> I\<rbrakk> \<Longrightarrow> x \<le> b
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}; a \<in> {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}\<rbrakk> \<Longrightarrow> x \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<le> b

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have A: "dist (p a) (p s) \<le> d" if "s < u" "a \<le> s" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
have "\<exists>t\<in>I. s < t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>I. s < t
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>I. s < t
[PROOF STEP]
apply (subst less_cSup_iff[symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. I \<noteq> {}
 2. bdd_above I
 3. s < Sup I
[PROOF STEP]
using \<open>a \<in> I\<close> \<open>bdd_above I\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> I
bdd_above I

goal (3 subgoals):
 1. I \<noteq> {}
 2. bdd_above I
 3. s < Sup I
[PROOF STEP]
using \<open>s < u\<close>
[PROOF STATE]
proof (prove)
using this:
a \<in> I
bdd_above I
s < u

goal (3 subgoals):
 1. I \<noteq> {}
 2. bdd_above I
 3. s < Sup I
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
a \<in> I
bdd_above I
s < Sup I

goal (3 subgoals):
 1. I \<noteq> {}
 2. bdd_above I
 3. s < Sup I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>I. s < t

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t\<in>I. s < t
[PROOF STEP]
obtain t where t: "t \<in> I" "s < t"
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<in>I. s < t

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> I; s < t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> I
s < t

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> I
s < t
[PROOF STEP]
have "s \<in> {a..t}"
[PROOF STATE]
proof (prove)
using this:
t \<in> I
s < t

goal (1 subgoal):
 1. s \<in> {a..t}
[PROOF STEP]
using \<open>a \<le> s\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> I
s < t
a \<le> s

goal (1 subgoal):
 1. s \<in> {a..t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> {a..t}

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> {a..t}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> {a..t}

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
using t(1)
[PROOF STATE]
proof (prove)
using this:
s \<in> {a..t}
t \<in> I

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {a..t}
t \<in> {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p a) (p s) \<le> d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s < u; a \<le> ?s\<rbrakk> \<Longrightarrow> dist (p a) (p ?s) \<le> d

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "continuous (at u within {a..b}) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at u within {a..b}) f
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f

goal (1 subgoal):
 1. continuous (at u within {a..b}) f
[PROOF STEP]
by (simp add: \<open>a \<le> u\<close> \<open>u \<le> b\<close> continuous_on_eq_continuous_within)
[PROOF STATE]
proof (state)
this:
continuous (at u within {a..b}) f

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
continuous (at u within {a..b}) f
[PROOF STEP]
have "\<exists>i > 0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < (delta - deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
using this:
continuous (at u within {a..b}) f

goal (1 subgoal):
 1. \<exists>i>0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)
[PROOF STEP]
unfolding continuous_within_eps_delta
[PROOF STATE]
proof (prove)
using this:
\<forall>e>0. \<exists>d>0. \<forall>x'\<in>{a..b}. dist x' u < d \<longrightarrow> dist (f x') (f u) < e

goal (1 subgoal):
 1. \<exists>i>0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)
[PROOF STEP]
using \<open>deltaG(TYPE('a)) < delta\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>e>0. \<exists>d>0. \<forall>x'\<in>{a..b}. dist x' u < d \<longrightarrow> dist (f x') (f u) < e
deltaG TYPE('a) < delta

goal (1 subgoal):
 1. \<exists>i>0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
\<exists>i>0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i>0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)
[PROOF STEP]
obtain e0 where e0: "e0 > 0" "\<And>s. s \<in> {a..b} \<Longrightarrow> dist u s < e0 \<Longrightarrow> dist (f u) (f s) < (delta - deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i>0. \<forall>s\<in>{a..b}. dist u s < i \<longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)

goal (1 subgoal):
 1. (\<And>e0. \<lbrakk>0 < e0; \<And>s. \<lbrakk>s \<in> {a..b}; dist u s < e0\<rbrakk> \<Longrightarrow> dist (f u) (f s) < delta - deltaG TYPE('a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < e0
\<lbrakk>?s \<in> {a..b}; dist u ?s < e0\<rbrakk> \<Longrightarrow> dist (f u) (f ?s) < delta - deltaG TYPE('a)

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
proof (cases "dist (p a) (p u) > d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
text \<open>First, consider the case where $u$ does not satisfy the defining property. Then the
    desired point $t$ is taken slightly to its left.\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
d < dist (p a) (p u)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d < dist (p a) (p u)
[PROOF STEP]
have "u \<noteq> a"
[PROOF STATE]
proof (prove)
using this:
d < dist (p a) (p u)

goal (1 subgoal):
 1. u \<noteq> a
[PROOF STEP]
using \<open>d \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
d < dist (p a) (p u)
0 \<le> d

goal (1 subgoal):
 1. u \<noteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<noteq> a

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> a
[PROOF STEP]
have "a < u"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> a

goal (1 subgoal):
 1. a < u
[PROOF STEP]
using \<open>a \<le> u\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> a
a \<le> u

goal (1 subgoal):
 1. a < u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < u

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
define e::real where "e = min (e0/2) ((u-a)/2)"
[PROOF STATE]
proof (state)
this:
e = min (e0 / 2) ((u - a) / 2)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = min (e0 / 2) ((u - a) / 2)
[PROOF STEP]
have "e > 0"
[PROOF STATE]
proof (prove)
using this:
e = min (e0 / 2) ((u - a) / 2)

goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
using \<open>a < u\<close> \<open>e0 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
e = min (e0 / 2) ((u - a) / 2)
a < u
0 < e0

goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < e

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
define t where "t = u - e"
[PROOF STATE]
proof (state)
this:
t = u - e

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = u - e
[PROOF STEP]
have "t < u"
[PROOF STATE]
proof (prove)
using this:
t = u - e

goal (1 subgoal):
 1. t < u
[PROOF STEP]
using \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
t = u - e
0 < e

goal (1 subgoal):
 1. t < u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t < u

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "u - b \<le> e" "e \<le> u - a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u - b \<le> e &&& e \<le> u - a
[PROOF STEP]
using \<open>e > 0\<close> \<open>u \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e
u \<le> b

goal (1 subgoal):
 1. u - b \<le> e &&& e \<le> u - a
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
using this:
0 < min (e0 / 2) ((u - a) / 2)
u \<le> b

goal (1 subgoal):
 1. u - b \<le> min (e0 / 2) ((u - a) / 2) &&& min (e0 / 2) ((u - a) / 2) \<le> u - a
[PROOF STEP]
by (auto simp add: min_def)
[PROOF STATE]
proof (state)
this:
u - b \<le> e
e \<le> u - a

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u - b \<le> e
e \<le> u - a
[PROOF STEP]
have "t \<in> {a..b}" "t \<in> {a..t}"
[PROOF STATE]
proof (prove)
using this:
u - b \<le> e
e \<le> u - a

goal (1 subgoal):
 1. t \<in> {a..b} &&& t \<in> {a..t}
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
u - b \<le> e
e \<le> u - a

goal (1 subgoal):
 1. u - e \<in> {a..b} &&& u - e \<in> {a..u - e}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> {a..b}
t \<in> {a..t}

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "dist u t < e0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist u t < e0
[PROOF STEP]
unfolding t_def e_def dist_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u - (u - min (e0 / 2) ((u - a) / 2))\<bar> < e0
[PROOF STEP]
using \<open>e0 > 0\<close> \<open>a \<le> u\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e0
a \<le> u

goal (1 subgoal):
 1. \<bar>u - (u - min (e0 / 2) ((u - a) / 2))\<bar> < e0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist u t < e0

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have *: "\<forall>s \<in> {a..t}. dist (p a) (p s) \<le> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d
[PROOF STEP]
using A \<open>t < u\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s < u; a \<le> ?s\<rbrakk> \<Longrightarrow> dist (p a) (p ?s) \<le> d
t < u

goal (1 subgoal):
 1. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "dist (p t) (p u) \<le> dist (f t) (f u) + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p t) (p u) \<le> dist (f t) (f u) + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
apply (rule proj_along_quasiconvex_contraction'[OF \<open>quasiconvex C G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p t \<in> proj_set (f t) G
 2. p u \<in> proj_set (f u) G
[PROOF STEP]
using assms (4) \<open>t \<in> {a..b}\<close> \<open>a \<le> u\<close> \<open>u \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
?t \<in> {a..b} \<Longrightarrow> p ?t \<in> proj_set (f ?t) G
t \<in> {a..b}
a \<le> u
u \<le> b

goal (2 subgoals):
 1. p t \<in> proj_set (f t) G
 2. p u \<in> proj_set (f u) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p t) (p u) \<le> dist (f t) (f u) + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p t) (p u) \<le> dist (f t) (f u) + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "... \<le> (delta - deltaG(TYPE('a))) + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) (f u) + 4 * deltaG TYPE('a) + 2 * C \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) (f u) \<le> delta - deltaG TYPE('a)
[PROOF STEP]
using e0(2)[OF \<open>t \<in> {a..b}\<close> \<open>dist u t < e0\<close>]
[PROOF STATE]
proof (prove)
using this:
dist (f u) (f t) < delta - deltaG TYPE('a)

goal (1 subgoal):
 1. dist (f t) (f u) \<le> delta - deltaG TYPE('a)
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist (f t) (f u) + 4 * deltaG TYPE('a) + 2 * C \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (p t) (p u) \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have I: "dist (p t) (p u) \<le> 4 * delta + 2 * C"
[PROOF STATE]
proof (prove)
using this:
dist (p t) (p u) \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. dist (p t) (p u) \<le> 4 * delta + 2 * C
[PROOF STEP]
using \<open>delta > deltaG(TYPE('a))\<close>
[PROOF STATE]
proof (prove)
using this:
dist (p t) (p u) \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C
deltaG TYPE('a) < delta

goal (1 subgoal):
 1. dist (p t) (p u) \<le> 4 * delta + 2 * C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (p t) (p u) \<le> 4 * delta + 2 * C

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "d \<le> dist (p a) (p u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> dist (p a) (p u)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
d < dist (p a) (p u)

goal (1 subgoal):
 1. d \<le> dist (p a) (p u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> dist (p a) (p u)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d \<le> dist (p a) (p u)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "... \<le> dist (p a) (p t) + dist (p t) (p u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p u) \<le> dist (p a) (p t) + dist (p t) (p u)
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (p a) (p u) \<le> dist (p a) (p t) + dist (p t) (p u)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p a) (p u) \<le> dist (p a) (p t) + dist (p t) (p u)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have "... \<le> dist (p a) (p t) + 4 * delta + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p t) + dist (p t) (p u) \<le> dist (p a) (p t) + 4 * delta + 2 * C
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
dist (p t) (p u) \<le> 4 * delta + 2 * C

goal (1 subgoal):
 1. dist (p a) (p t) + dist (p t) (p u) \<le> dist (p a) (p t) + 4 * delta + 2 * C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (p a) (p t) + dist (p t) (p u) \<le> dist (p a) (p t) + 4 * delta + 2 * C

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d \<le> dist (p a) (p t) + 4 * delta + 2 * C
[PROOF STEP]
have **: "d - 4 * delta - 2 * C \<le> dist (p a) (p t)"
[PROOF STATE]
proof (prove)
using this:
d \<le> dist (p a) (p t) + 4 * delta + 2 * C

goal (1 subgoal):
 1. d - 4 * delta - 2 * C \<le> dist (p a) (p t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d - 4 * delta - 2 * C \<le> dist (p a) (p t)

goal (2 subgoals):
 1. d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
 2. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
apply (rule bexI[OF _ \<open>t \<in> {a..b}\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
using * ** \<open>t \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d
d - 4 * delta - 2 * C \<le> dist (p a) (p t)
t \<in> {a..b}

goal (1 subgoal):
 1. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)

goal (1 subgoal):
 1. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
text \<open>Next, consider the case where $u$ satisfies the defining property. Then we will take $t = u$.
    The only nontrivial point to check is that the distance of $f(u)$ to the starting point is not
    too small. For this, we need to separate the case where $u = b$ (in which case one argues directly)
    and the case where $u < b$, where one can use a point slightly to the right of $u$ which has a
    projection at distance $ > d$ of the starting point, and use almost continuity.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> d < dist (p a) (p u)

goal (1 subgoal):
 1. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have B: "dist (p a) (p s) \<le> d" if "s \<in> {a..u}" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
proof (cases "s = u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = u \<Longrightarrow> dist (p a) (p s) \<le> d
 2. s \<noteq> u \<Longrightarrow> dist (p a) (p s) \<le> d
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s = u

goal (2 subgoals):
 1. s = u \<Longrightarrow> dist (p a) (p s) \<le> d
 2. s \<noteq> u \<Longrightarrow> dist (p a) (p s) \<le> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p u) \<le> d
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> d < dist (p a) (p u)

goal (1 subgoal):
 1. dist (p a) (p u) \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p a) (p s) \<le> d

goal (1 subgoal):
 1. s \<noteq> u \<Longrightarrow> dist (p a) (p s) \<le> d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> u \<Longrightarrow> dist (p a) (p s) \<le> d
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s \<noteq> u

goal (1 subgoal):
 1. s \<noteq> u \<Longrightarrow> dist (p a) (p s) \<le> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<noteq> u

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
using that A
[PROOF STATE]
proof (prove)
using this:
s \<noteq> u
s \<in> {a..u}
\<lbrakk>?s < u; a \<le> ?s\<rbrakk> \<Longrightarrow> dist (p a) (p ?s) \<le> d

goal (1 subgoal):
 1. dist (p a) (p s) \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p a) (p s) \<le> d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?s \<in> {a..u} \<Longrightarrow> dist (p a) (p ?s) \<le> d

goal (1 subgoal):
 1. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
have C: "dist (p a) (p u) \<ge> d - 4 *delta - 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
proof (cases "u = b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = b

goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "d \<le> dist (p a) (p b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> dist (p a) (p b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f
a \<le> b
quasiconvex C G
?t \<in> {a..b} \<Longrightarrow> p ?t \<in> proj_set (f ?t) G
deltaG TYPE('a) < delta
d \<in> {4 * delta + 2 * C..dist (p a) (p b)}

goal (1 subgoal):
 1. d \<le> dist (p a) (p b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> dist (p a) (p b)

goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d \<le> dist (p a) (p b)

goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "... \<le> dist (p a) (p u) + dist (p u) (p b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p b) \<le> dist (p a) (p u) + dist (p u) (p b)
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (p a) (p b) \<le> dist (p a) (p u) + dist (p u) (p b)

goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p a) (p b) \<le> dist (p a) (p u) + dist (p u) (p b)

goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "... \<le> dist (p a) (p u) + (dist (f u) (f b) + 4 * deltaG TYPE('a) + 2 * C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p u) + dist (p u) (p b) \<le> dist (p a) (p u) + (dist (f u) (f b) + 4 * deltaG TYPE('a) + 2 * C)
[PROOF STEP]
apply (intro mono_intros proj_along_quasiconvex_contraction'[OF \<open>quasiconvex C G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p u \<in> proj_set (f u) G
 2. p b \<in> proj_set (f b) G
[PROOF STEP]
using assms \<open>a \<le> u\<close> \<open>u \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f
a \<le> b
quasiconvex C G
?t \<in> {a..b} \<Longrightarrow> p ?t \<in> proj_set (f ?t) G
deltaG TYPE('a) < delta
d \<in> {4 * delta + 2 * C..dist (p a) (p b)}
a \<le> u
u \<le> b

goal (2 subgoals):
 1. p u \<in> proj_set (f u) G
 2. p b \<in> proj_set (f b) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p a) (p u) + dist (p u) (p b) \<le> dist (p a) (p u) + (dist (f u) (f b) + 4 * deltaG TYPE('a) + 2 * C)

goal (2 subgoals):
 1. u = b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
 2. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d \<le> dist (p a) (p u) + (dist (f u) (f b) + 4 * deltaG TYPE('a) + 2 * C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d \<le> dist (p a) (p u) + (dist (f u) (f b) + 4 * deltaG TYPE('a) + 2 * C)

goal (1 subgoal):
 1. d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
using this:
d \<le> dist (p a) (p b) + (dist (f b) (f b) + 4 * deltaG TYPE('a) + 2 * C)

goal (1 subgoal):
 1. d - 4 * delta - 2 * C \<le> dist (p a) (p b)
[PROOF STEP]
using \<open>deltaG(TYPE('a)) < delta\<close>
[PROOF STATE]
proof (prove)
using this:
d \<le> dist (p a) (p b) + (dist (f b) (f b) + 4 * deltaG TYPE('a) + 2 * C)
deltaG TYPE('a) < delta

goal (1 subgoal):
 1. d - 4 * delta - 2 * C \<le> dist (p a) (p b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d - 4 * delta - 2 * C \<le> dist (p a) (p u)

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> b

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> b
[PROOF STEP]
have "u < b"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> b

goal (1 subgoal):
 1. u < b
[PROOF STEP]
using \<open>u \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> b
u \<le> b

goal (1 subgoal):
 1. u < b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u < b

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
define e::real where "e = min (e0/2) ((b-u)/2)"
[PROOF STATE]
proof (state)
this:
e = min (e0 / 2) ((b - u) / 2)

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e = min (e0 / 2) ((b - u) / 2)
[PROOF STEP]
have "e > 0"
[PROOF STATE]
proof (prove)
using this:
e = min (e0 / 2) ((b - u) / 2)

goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
using \<open>u < b\<close> \<open>e0 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
e = min (e0 / 2) ((b - u) / 2)
u < b
0 < e0

goal (1 subgoal):
 1. 0 < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
define v where "v = u + e"
[PROOF STATE]
proof (state)
this:
v = u + e

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = u + e
[PROOF STEP]
have "u < v"
[PROOF STATE]
proof (prove)
using this:
v = u + e

goal (1 subgoal):
 1. u < v
[PROOF STEP]
using \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
v = u + e
0 < e

goal (1 subgoal):
 1. u < v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u < v

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "e \<le> b - u" "a - u \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<le> b - u &&& a - u \<le> e
[PROOF STEP]
using \<open>e > 0\<close> \<open>a \<le> u\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e
a \<le> u

goal (1 subgoal):
 1. e \<le> b - u &&& a - u \<le> e
[PROOF STEP]
unfolding e_def
[PROOF STATE]
proof (prove)
using this:
0 < min (e0 / 2) ((b - u) / 2)
a \<le> u

goal (1 subgoal):
 1. min (e0 / 2) ((b - u) / 2) \<le> b - u &&& a - u \<le> min (e0 / 2) ((b - u) / 2)
[PROOF STEP]
by (auto simp add: min_def)
[PROOF STATE]
proof (state)
this:
e \<le> b - u
a - u \<le> e

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<le> b - u
a - u \<le> e
[PROOF STEP]
have "v \<in> {a..b}"
[PROOF STATE]
proof (prove)
using this:
e \<le> b - u
a - u \<le> e

goal (1 subgoal):
 1. v \<in> {a..b}
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
using this:
e \<le> b - u
a - u \<le> e

goal (1 subgoal):
 1. u + e \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> {a..b}

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> {a..b}

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "v \<notin> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> I
[PROOF STEP]
using \<open>u < v\<close> \<open>bdd_above I\<close> cSup_upper not_le
[PROOF STATE]
proof (prove)
using this:
u < v
bdd_above I
\<lbrakk>?x \<in> ?X; bdd_above ?X\<rbrakk> \<Longrightarrow> ?x \<le> Sup ?X
(\<not> ?x \<le> ?y) = (?y < ?x)

goal (1 subgoal):
 1. v \<notin> I
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
using this:
Sup I < v
bdd_above I
\<lbrakk>?x \<in> ?X; bdd_above ?X\<rbrakk> \<Longrightarrow> ?x \<le> Sup ?X
(\<not> ?x \<le> ?y) = (?y < ?x)

goal (1 subgoal):
 1. v \<notin> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<notin> I

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> {a..b}
v \<notin> I
[PROOF STEP]
have "\<exists>w \<in> {a..v}. dist (p a) (p w) > d"
[PROOF STATE]
proof (prove)
using this:
v \<in> {a..b}
v \<notin> I

goal (1 subgoal):
 1. \<exists>w\<in>{a..v}. d < dist (p a) (p w)
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {a..b}
v \<notin> {t \<in> {a..b}. \<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d}

goal (1 subgoal):
 1. \<exists>w\<in>{a..v}. d < dist (p a) (p w)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>w\<in>{a..v}. d < dist (p a) (p w)

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>w\<in>{a..v}. d < dist (p a) (p w)
[PROOF STEP]
obtain w where w: "w \<in> {a..v}" "dist (p a) (p w) > d"
[PROOF STATE]
proof (prove)
using this:
\<exists>w\<in>{a..v}. d < dist (p a) (p w)

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w \<in> {a..v}; d < dist (p a) (p w)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> {a..v}
d < dist (p a) (p w)

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> {a..v}
d < dist (p a) (p w)
[PROOF STEP]
have "w \<notin> {a..u}"
[PROOF STATE]
proof (prove)
using this:
w \<in> {a..v}
d < dist (p a) (p w)

goal (1 subgoal):
 1. w \<notin> {a..u}
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
w \<in> {a..v}
d < dist (p a) (p w)
?s \<in> {a..u} \<Longrightarrow> dist (p a) (p ?s) \<le> d

goal (1 subgoal):
 1. w \<notin> {a..u}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
w \<notin> {a..u}

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<notin> {a..u}
[PROOF STEP]
have "u < w"
[PROOF STATE]
proof (prove)
using this:
w \<notin> {a..u}

goal (1 subgoal):
 1. u < w
[PROOF STEP]
using w(1)
[PROOF STATE]
proof (prove)
using this:
w \<notin> {a..u}
w \<in> {a..v}

goal (1 subgoal):
 1. u < w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u < w

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "w \<in> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> {a..b}
[PROOF STEP]
using w(1) \<open>v \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> {a..v}
v \<in> {a..b}

goal (1 subgoal):
 1. w \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> {a..b}

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "dist u w = w - u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist u w = w - u
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>u - w\<bar> = w - u
[PROOF STEP]
using \<open>u < w\<close>
[PROOF STATE]
proof (prove)
using this:
u < w

goal (1 subgoal):
 1. \<bar>u - w\<bar> = w - u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist u w = w - u

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist u w = w - u

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "... \<le> v - u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w - u \<le> v - u
[PROOF STEP]
using w(1)
[PROOF STATE]
proof (prove)
using this:
w \<in> {a..v}

goal (1 subgoal):
 1. w - u \<le> v - u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w - u \<le> v - u

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w - u \<le> v - u

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "... < e0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v - u < e0
[PROOF STEP]
unfolding v_def e_def min_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u + (if e0 / 2 \<le> (b - u) / 2 then e0 / 2 else (b - u) / 2) - u < e0
[PROOF STEP]
using \<open>e0 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e0

goal (1 subgoal):
 1. u + (if e0 / 2 \<le> (b - u) / 2 then e0 / 2 else (b - u) / 2) - u < e0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v - u < e0

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist u w < e0
[PROOF STEP]
have "dist u w < e0"
[PROOF STATE]
proof (prove)
using this:
dist u w < e0

goal (1 subgoal):
 1. dist u w < e0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist u w < e0

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "dist (p u) (p w) \<le> dist (f u) (f w) + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p u) (p w) \<le> dist (f u) (f w) + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
apply (rule proj_along_quasiconvex_contraction'[OF \<open>quasiconvex C G\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p u \<in> proj_set (f u) G
 2. p w \<in> proj_set (f w) G
[PROOF STEP]
using assms \<open>a \<le> u\<close> \<open>u \<le> b\<close> \<open>w \<in> {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f
a \<le> b
quasiconvex C G
?t \<in> {a..b} \<Longrightarrow> p ?t \<in> proj_set (f ?t) G
deltaG TYPE('a) < delta
d \<in> {4 * delta + 2 * C..dist (p a) (p b)}
a \<le> u
u \<le> b
w \<in> {a..b}

goal (2 subgoals):
 1. p u \<in> proj_set (f u) G
 2. p w \<in> proj_set (f w) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p u) (p w) \<le> dist (f u) (f w) + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (p u) (p w) \<le> dist (f u) (f w) + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "... \<le> (delta - deltaG(TYPE('a))) + 4 * deltaG(TYPE('a)) + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f u) (f w) + 4 * deltaG TYPE('a) + 2 * C \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f u) (f w) \<le> delta - deltaG TYPE('a)
[PROOF STEP]
using e0(2)[OF \<open>w \<in> {a..b}\<close> \<open>dist u w < e0\<close>]
[PROOF STATE]
proof (prove)
using this:
dist (f u) (f w) < delta - deltaG TYPE('a)

goal (1 subgoal):
 1. dist (f u) (f w) \<le> delta - deltaG TYPE('a)
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist (f u) (f w) + 4 * deltaG TYPE('a) + 2 * C \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (p u) (p w) \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C
[PROOF STEP]
have I: "dist (p u) (p w) \<le> 4 * delta + 2 * C"
[PROOF STATE]
proof (prove)
using this:
dist (p u) (p w) \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C

goal (1 subgoal):
 1. dist (p u) (p w) \<le> 4 * delta + 2 * C
[PROOF STEP]
using \<open>delta > deltaG(TYPE('a))\<close>
[PROOF STATE]
proof (prove)
using this:
dist (p u) (p w) \<le> delta - deltaG TYPE('a) + 4 * deltaG TYPE('a) + 2 * C
deltaG TYPE('a) < delta

goal (1 subgoal):
 1. dist (p u) (p w) \<le> 4 * delta + 2 * C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (p u) (p w) \<le> 4 * delta + 2 * C

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "d \<le> dist (p a) (p u) + dist (p u) (p w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> dist (p a) (p u) + dist (p u) (p w)
[PROOF STEP]
using w(2) metric_space_class.dist_triangle[of "p a" "p w" "p u"]
[PROOF STATE]
proof (prove)
using this:
d < dist (p a) (p w)
dist (p a) (p w) \<le> dist (p a) (p u) + dist (p u) (p w)

goal (1 subgoal):
 1. d \<le> dist (p a) (p u) + dist (p u) (p w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> dist (p a) (p u) + dist (p u) (p w)

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d \<le> dist (p a) (p u) + dist (p u) (p w)

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
have "... \<le> dist (p a) (p u) + 4 * delta + 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p a) (p u) + dist (p u) (p w) \<le> dist (p a) (p u) + 4 * delta + 2 * C
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
dist (p u) (p w) \<le> 4 * delta + 2 * C

goal (1 subgoal):
 1. dist (p a) (p u) + dist (p u) (p w) \<le> dist (p a) (p u) + 4 * delta + 2 * C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (p a) (p u) + dist (p u) (p w) \<le> dist (p a) (p u) + 4 * delta + 2 * C

goal (1 subgoal):
 1. u \<noteq> b \<Longrightarrow> d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d \<le> dist (p a) (p u) + 4 * delta + 2 * C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d \<le> dist (p a) (p u) + 4 * delta + 2 * C

goal (1 subgoal):
 1. d - 4 * delta - 2 * C \<le> dist (p a) (p u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d - 4 * delta - 2 * C \<le> dist (p a) (p u)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d - 4 * delta - 2 * C \<le> dist (p a) (p u)

goal (1 subgoal):
 1. \<not> d < dist (p a) (p u) \<Longrightarrow> \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)
[PROOF STEP]
apply (rule bexI[of _ u])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist (p a) (p u) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..u}. dist (p a) (p s) \<le> d)
 2. u \<in> {a..b}
[PROOF STEP]
using B \<open>a \<le> u\<close> \<open>u \<le> b\<close> C
[PROOF STATE]
proof (prove)
using this:
?s \<in> {a..u} \<Longrightarrow> dist (p a) (p ?s) \<le> d
a \<le> u
u \<le> b
d - 4 * delta - 2 * C \<le> dist (p a) (p u)

goal (2 subgoals):
 1. dist (p a) (p u) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..u}. dist (p a) (p s) \<le> d)
 2. u \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>{a..b}. dist (p a) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{a..t}. dist (p a) (p s) \<le> d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) quasi_convex_projection_small_gaps':
  assumes "continuous_on {a..(b::real)} f"
          "a \<le> b"
          "quasiconvex C G"
          "\<And>x. x \<in> {a..b} \<Longrightarrow> p x \<in> proj_set (f x) G"
          "delta > deltaG(TYPE('a))"
          "d \<in> {4 * delta + 2 * C..dist (p a) (p b)}"
  shows "\<exists>t \<in> {a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C .. d}
                    \<and> (\<forall>s \<in> {t..b}. dist (p b) (p s) \<le> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
have *: "continuous_on {-b..-a} (\<lambda>t. f(-t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {- b..- a} (\<lambda>t. f (- t))
[PROOF STEP]
using continuous_on_compose[of "{-b..-a}" "\<lambda>t. -t" f]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on {- b..- a} uminus; continuous_on (uminus ` {- b..- a}) f\<rbrakk> \<Longrightarrow> continuous_on {- b..- a} (f \<circ> uminus)

goal (1 subgoal):
 1. continuous_on {- b..- a} (\<lambda>t. f (- t))
[PROOF STEP]
using assms(1) continuous_on_minus[OF continuous_on_id]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>continuous_on {- b..- a} uminus; continuous_on (uminus ` {- b..- a}) f\<rbrakk> \<Longrightarrow> continuous_on {- b..- a} (f \<circ> uminus)
continuous_on {a..b} f
continuous_on ?s uminus

goal (1 subgoal):
 1. continuous_on {- b..- a} (\<lambda>t. f (- t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
continuous_on {- b..- a} (\<lambda>t. f (- t))

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
define q where "q = (\<lambda>t. p(-t))"
[PROOF STATE]
proof (state)
this:
q = (\<lambda>t. p (- t))

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
have "\<exists>t \<in> {-b..-a}. (dist (q (-b)) (q t) \<in> {d - 4 * delta - 2 * C .. d})
                    \<and> (\<forall>s \<in> {-b..t}. dist (q (-b)) (q s) \<le> d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{- b..- a}. dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{- b..t}. dist (q (- b)) (q s) \<le> d)
[PROOF STEP]
apply (rule quasi_convex_projection_small_gaps[where ?f = "\<lambda>t. f(-t)" and ?G = G])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. continuous_on {- b..- a} (\<lambda>t. f (- t))
 2. - b \<le> - a
 3. quasiconvex C G
 4. \<And>t. t \<in> {- b..- a} \<Longrightarrow> q t \<in> proj_set (f (- t)) G
 5. deltaG TYPE('a) < delta
 6. d \<in> {4 * delta + 2 * C..dist (q (- b)) (q (- a))}
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. continuous_on {- b..- a} (\<lambda>t. f (- t))
 2. - b \<le> - a
 3. quasiconvex C G
 4. \<And>t. t \<in> {- b..- a} \<Longrightarrow> p (- t) \<in> proj_set (f (- t)) G
 5. deltaG TYPE('a) < delta
 6. d \<in> {4 * delta + 2 * C..dist (p (- (- b))) (p (- (- a)))}
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f
a \<le> b
quasiconvex C G
?x \<in> {a..b} \<Longrightarrow> p ?x \<in> proj_set (f ?x) G
deltaG TYPE('a) < delta
d \<in> {4 * delta + 2 * C..dist (p a) (p b)}
continuous_on {- b..- a} (\<lambda>t. f (- t))

goal (6 subgoals):
 1. continuous_on {- b..- a} (\<lambda>t. f (- t))
 2. - b \<le> - a
 3. quasiconvex C G
 4. \<And>t. t \<in> {- b..- a} \<Longrightarrow> p (- t) \<in> proj_set (f (- t)) G
 5. deltaG TYPE('a) < delta
 6. d \<in> {4 * delta + 2 * C..dist (p (- (- b))) (p (- (- a)))}
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>{- b..- a}. dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{- b..t}. dist (q (- b)) (q s) \<le> d)

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t\<in>{- b..- a}. dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{- b..t}. dist (q (- b)) (q s) \<le> d)
[PROOF STEP]
obtain t where t: "t \<in> {-b..-a}" "dist (q (-b)) (q t) \<in> {d - 4 * delta - 2 * C .. d}"
                      "\<And>s. s \<in> {-b..t} \<Longrightarrow> dist (q (-b)) (q s) \<le> d"
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<in>{- b..- a}. dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{- b..t}. dist (q (- b)) (q s) \<le> d)

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {- b..- a}; dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d}; \<And>s. s \<in> {- b..t} \<Longrightarrow> dist (q (- b)) (q s) \<le> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> {- b..- a}
dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d}
?s \<in> {- b..t} \<Longrightarrow> dist (q (- b)) (q ?s) \<le> d

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
have *: "dist (p b) (p s) \<le> d" if "s \<in> {-t..b}" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (p b) (p s) \<le> d
[PROOF STEP]
using t(3)[of "-s"] that q_def
[PROOF STATE]
proof (prove)
using this:
- s \<in> {- b..t} \<Longrightarrow> dist (q (- b)) (q (- s)) \<le> d
s \<in> {- t..b}
q = (\<lambda>t. p (- t))

goal (1 subgoal):
 1. dist (p b) (p s) \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?s \<in> {- t..b} \<Longrightarrow> dist (p b) (p ?s) \<le> d

goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)
[PROOF STEP]
apply (rule bexI[of _ "-t"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist (p b) (p (- t)) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{- t..b}. dist (p b) (p s) \<le> d)
 2. - t \<in> {a..b}
[PROOF STEP]
using t * q_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {- b..- a}
dist (q (- b)) (q t) \<in> {d - 4 * delta - 2 * C..d}
?s \<in> {- b..t} \<Longrightarrow> dist (q (- b)) (q ?s) \<le> d
?s \<in> {- t..b} \<Longrightarrow> dist (p b) (p ?s) \<le> d
q = (\<lambda>t. p (- t))

goal (2 subgoals):
 1. dist (p b) (p (- t)) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{- t..b}. dist (p b) (p s) \<le> d)
 2. - t \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>{a..b}. dist (p b) (p t) \<in> {d - 4 * delta - 2 * C..d} \<and> (\<forall>s\<in>{t..b}. dist (p b) (p s) \<le> d)

goal:
No subgoals!
[PROOF STEP]
qed