[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) quasiconvex_projection_exp_contracting:
  assumes "quasiconvex K G"
          "\<And>x y. x \<in> {a..b} \<Longrightarrow> y \<in> {a..b} \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C"
          "a \<le> b"
          "pa \<in> proj_set (f a) G"
          "pb \<in> proj_set (f b) G"
          "\<And>t. t \<in> {a..b} \<Longrightarrow> infdist (f t) G \<ge> D"
          "D \<ge> 15/2 * delta + K + C/2"
          "delta > deltaG(TYPE('a))"
          "C \<ge> 0"
          "lambda \<ge> 0"
  shows "dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG(TYPE('a))) ((4 * exp(1/2 * ln 2)) * lambda * (b-a) * exp(-(D - K - C/2) * ln 2 / (5 * delta)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
obtain H where H: "geodesic_segment_between H pa pb" "\<And>q. q \<in> H \<Longrightarrow> infdist q G \<le> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>H. \<lbrakk>geodesic_segment_between H pa pb; \<And>q. q \<in> H \<Longrightarrow> infdist q G \<le> K\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using quasiconvexD[OF assms(1) proj_setD(1)[OF \<open>pa \<in> proj_set (f a) G\<close>] proj_setD(1)[OF \<open>pb \<in> proj_set (f b) G\<close>]]
[PROOF STATE]
proof (prove)
using this:
\<exists>Ga. geodesic_segment_between Ga pa pb \<and> (\<forall>z\<in>Ga. infdist z G \<le> K)

goal (1 subgoal):
 1. (\<And>H. \<lbrakk>geodesic_segment_between H pa pb; \<And>q. q \<in> H \<Longrightarrow> infdist q G \<le> K\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between H pa pb
?q \<in> H \<Longrightarrow> infdist ?q G \<le> K

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
obtain qa where qa: "qa \<in> proj_set (f a) H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>qa. qa \<in> proj_set (f a) H \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using proj_set_nonempty_of_proper[of H "f a"] geodesic_segment_topology[OF geodesic_segmentI[OF H(1)]]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>proper H; H \<noteq> {}\<rbrakk> \<Longrightarrow> proj_set (f a) H \<noteq> {}
compact H
connected H
path_connected H
bounded H
closed H
H \<noteq> {}
proper H

goal (1 subgoal):
 1. (\<And>qa. qa \<in> proj_set (f a) H \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qa \<in> proj_set (f a) H

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
obtain qb where qb: "qb \<in> proj_set (f b) H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>qb. qb \<in> proj_set (f b) H \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using proj_set_nonempty_of_proper[of H "f b"] geodesic_segment_topology[OF geodesic_segmentI[OF H(1)]]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>proper H; H \<noteq> {}\<rbrakk> \<Longrightarrow> proj_set (f b) H \<noteq> {}
compact H
connected H
path_connected H
bounded H
closed H
H \<noteq> {}
proper H

goal (1 subgoal):
 1. (\<And>qb. qb \<in> proj_set (f b) H \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qb \<in> proj_set (f b) H

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have I: "infdist (f t) H \<ge> D - K" if "t \<in> {a..b}" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D - K \<le> infdist (f t) H
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D - K \<le> infdist (f t) H
[PROOF STEP]
have *: "D - K \<le> dist (f t) h" if "h \<in> H" for h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D - K \<le> dist (f t) h
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D - K \<le> dist (f t) h
[PROOF STEP]
have "D - K - dist (f t) h \<le> e" if "e > 0" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
have *: "infdist h G < K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist h G < K + e
[PROOF STEP]
using H(2)[OF \<open>h \<in> H\<close>] \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
infdist h G \<le> K
0 < e

goal (1 subgoal):
 1. infdist h G < K + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist h G < K + e

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
obtain g where g: "g \<in> G" "dist h g < K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; dist h g < K + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infdist_almost_attained[OF *] proj_setD(1)[OF \<open>pa \<in> proj_set (f a) G\<close>]
[PROOF STATE]
proof (prove)
using this:
G \<noteq> {} \<Longrightarrow> \<exists>y\<in>G. dist h y < K + e
pa \<in> G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; dist h g < K + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> G
dist h g < K + e

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
have "D \<le> dist (f t) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<le> dist (f t) g
[PROOF STEP]
using \<open>\<And>t. t \<in> {a..b} \<Longrightarrow> infdist (f t) G \<ge> D\<close>[OF \<open>t \<in> {a..b}\<close>] infdist_le[OF \<open>g \<in> G\<close>, of "f t"]
[PROOF STATE]
proof (prove)
using this:
D \<le> infdist (f t) G
infdist (f t) G \<le> dist (f t) g

goal (1 subgoal):
 1. D \<le> dist (f t) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<le> dist (f t) g

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D \<le> dist (f t) g

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
have "... \<le> dist (f t) h + dist h g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) g \<le> dist (f t) h + dist h g
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (f t) g \<le> dist (f t) h + dist h g

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f t) g \<le> dist (f t) h + dist h g

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
have "... \<le> dist (f t) h + K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) h + dist h g \<le> dist (f t) h + K + e
[PROOF STEP]
using g(2)
[PROOF STATE]
proof (prove)
using this:
dist h g < K + e

goal (1 subgoal):
 1. dist (f t) h + dist h g \<le> dist (f t) h + K + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f t) h + dist h g \<le> dist (f t) h + K + e

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
D \<le> dist (f t) h + K + e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
D \<le> dist (f t) h + K + e

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D - K - dist (f t) h \<le> e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> D - K - dist (f t) h \<le> ?e

goal (1 subgoal):
 1. D - K \<le> dist (f t) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?e \<Longrightarrow> D - K - dist (f t) h \<le> ?e
[PROOF STEP]
have *: "D - K - dist (f t) h \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> D - K - dist (f t) h \<le> ?e

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> 0
[PROOF STEP]
using dense_ge
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> D - K - dist (f t) h \<le> ?e
(\<And>x. ?z < x \<Longrightarrow> ?y \<le> x) \<Longrightarrow> ?y \<le> ?z

goal (1 subgoal):
 1. D - K - dist (f t) h \<le> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D - K - dist (f t) h \<le> 0

goal (1 subgoal):
 1. D - K \<le> dist (f t) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D - K - dist (f t) h \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
D - K - dist (f t) h \<le> 0

goal (1 subgoal):
 1. D - K \<le> dist (f t) h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D - K \<le> dist (f t) h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?h \<in> H \<Longrightarrow> D - K \<le> dist (f t) ?h

goal (1 subgoal):
 1. D - K \<le> infdist (f t) H
[PROOF STEP]
have "D - K \<le> Inf (dist (f t) ` H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D - K \<le> Inf (dist (f t) ` H)
[PROOF STEP]
apply (rule cInf_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist (f t) ` H \<noteq> {}
 2. \<And>x. x \<in> dist (f t) ` H \<Longrightarrow> D - K \<le> x
[PROOF STEP]
using * H(1)
[PROOF STATE]
proof (prove)
using this:
?h \<in> H \<Longrightarrow> D - K \<le> dist (f t) ?h
geodesic_segment_between H pa pb

goal (2 subgoals):
 1. dist (f t) ` H \<noteq> {}
 2. \<And>x. x \<in> dist (f t) ` H \<Longrightarrow> D - K \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D - K \<le> Inf (dist (f t) ` H)

goal (1 subgoal):
 1. D - K \<le> infdist (f t) H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
D - K \<le> Inf (dist (f t) ` H)
[PROOF STEP]
show "D - K \<le> infdist (f t) H"
[PROOF STATE]
proof (prove)
using this:
D - K \<le> Inf (dist (f t) ` H)

goal (1 subgoal):
 1. D - K \<le> infdist (f t) H
[PROOF STEP]
apply (subst infdist_notempty)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. D - K \<le> Inf (dist (f t) ` H) \<Longrightarrow> H \<noteq> {}
 2. D - K \<le> Inf (dist (f t) ` H) \<Longrightarrow> D - K \<le> Inf (dist (f t) ` H)
[PROOF STEP]
using H(1)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between H pa pb

goal (2 subgoals):
 1. D - K \<le> Inf (dist (f t) ` H) \<Longrightarrow> H \<noteq> {}
 2. D - K \<le> Inf (dist (f t) ` H) \<Longrightarrow> D - K \<le> Inf (dist (f t) ` H)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D - K \<le> infdist (f t) H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?t \<in> {a..b} \<Longrightarrow> D - K \<le> infdist (f ?t) H

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have Q: "dist qa qb \<le> max (5 * deltaG(TYPE('a))) ((4 * exp(1/2 * ln 2)) * lambda * (b-a) * exp(-((D - K)-C/2 ) * ln 2 / (5 * delta)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist qa qb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
apply (rule geodesic_projection_exp_contracting[OF geodesic_segmentI[OF \<open>geodesic_segment_between H pa pb\<close>] assms(2) assms(3)])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}\<rbrakk> \<Longrightarrow> x \<in> {a..b}
 2. \<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}\<rbrakk> \<Longrightarrow> y \<in> {a..b}
 3. qa \<in> proj_set (f a) H
 4. qb \<in> proj_set (f b) H
 5. \<And>t. t \<in> {a..b} \<Longrightarrow> D - K \<le> infdist (f t) H
 6. 15 / 2 * delta + C / 2 \<le> D - K
 7. deltaG TYPE('a) < delta
 8. 0 \<le> C
 9. 0 \<le> lambda
[PROOF STEP]
using qa qb I assms
[PROOF STATE]
proof (prove)
using this:
qa \<in> proj_set (f a) H
qb \<in> proj_set (f b) H
?t \<in> {a..b} \<Longrightarrow> D - K \<le> infdist (f ?t) H
quasiconvex K G
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
a \<le> b
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G
?t \<in> {a..b} \<Longrightarrow> D \<le> infdist (f ?t) G
15 / 2 * delta + K + C / 2 \<le> D
deltaG TYPE('a) < delta
0 \<le> C
0 \<le> lambda

goal (9 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}\<rbrakk> \<Longrightarrow> x \<in> {a..b}
 2. \<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}\<rbrakk> \<Longrightarrow> y \<in> {a..b}
 3. qa \<in> proj_set (f a) H
 4. qb \<in> proj_set (f b) H
 5. \<And>t. t \<in> {a..b} \<Longrightarrow> D - K \<le> infdist (f t) H
 6. 15 / 2 * delta + C / 2 \<le> D - K
 7. deltaG TYPE('a) < delta
 8. 0 \<le> C
 9. 0 \<le> lambda
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist qa qb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have A: "dist pa qa \<le> 4 * delta + K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
have "dist (f a) pa - dist (f a) qa - K \<le> e" if "e > 0" for e::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
have *: "infdist qa G < K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist qa G < K + e
[PROOF STEP]
using H(2)[OF proj_setD(1)[OF qa]] \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
infdist qa G \<le> K
0 < e

goal (1 subgoal):
 1. infdist qa G < K + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist qa G < K + e

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
obtain g where g: "g \<in> G" "dist qa g < K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; dist qa g < K + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infdist_almost_attained[OF *] proj_setD(1)[OF \<open>pa \<in> proj_set (f a) G\<close>]
[PROOF STATE]
proof (prove)
using this:
G \<noteq> {} \<Longrightarrow> \<exists>y\<in>G. dist qa y < K + e
pa \<in> G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; dist qa g < K + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> G
dist qa g < K + e

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
have "dist (f a) pa \<le> dist (f a) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) pa \<le> dist (f a) g
[PROOF STEP]
unfolding proj_setD(2)[OF \<open>pa \<in> proj_set (f a) G\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f a) G \<le> dist (f a) g
[PROOF STEP]
using infdist_le[OF \<open>g \<in> G\<close>, of "f a"]
[PROOF STATE]
proof (prove)
using this:
infdist (f a) G \<le> dist (f a) g

goal (1 subgoal):
 1. infdist (f a) G \<le> dist (f a) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f a) pa \<le> dist (f a) g

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f a) pa \<le> dist (f a) g

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
have "... \<le> dist (f a) qa + dist qa g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) g \<le> dist (f a) qa + dist qa g
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (f a) g \<le> dist (f a) qa + dist qa g

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f a) g \<le> dist (f a) qa + dist qa g

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
have "... \<le> dist (f a) qa + K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) qa + dist qa g \<le> dist (f a) qa + K + e
[PROOF STEP]
using g(2)
[PROOF STATE]
proof (prove)
using this:
dist qa g < K + e

goal (1 subgoal):
 1. dist (f a) qa + dist qa g \<le> dist (f a) qa + K + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f a) qa + dist qa g \<le> dist (f a) qa + K + e

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f a) pa \<le> dist (f a) qa + K + e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (f a) pa \<le> dist (f a) qa + K + e

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f a) pa - dist (f a) qa - K \<le> e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> dist (f a) pa - dist (f a) qa - K \<le> ?e

goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?e \<Longrightarrow> dist (f a) pa - dist (f a) qa - K \<le> ?e
[PROOF STEP]
have I: "dist (f a) pa - dist (f a) qa - K \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> dist (f a) pa - dist (f a) qa - K \<le> ?e

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> 0
[PROOF STEP]
using dense_ge
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> dist (f a) pa - dist (f a) qa - K \<le> ?e
(\<And>x. ?z < x \<Longrightarrow> ?y \<le> x) \<Longrightarrow> ?y \<le> ?z

goal (1 subgoal):
 1. dist (f a) pa - dist (f a) qa - K \<le> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist (f a) pa - dist (f a) qa - K \<le> 0

goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
have "dist (f a) qa + dist qa pa \<le> dist (f a) pa + 4 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) qa + dist qa pa \<le> dist (f a) pa + 4 * deltaG TYPE('a)
[PROOF STEP]
apply (rule dist_along_geodesic[OF geodesic_segmentI[OF H(1)]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. qa \<in> proj_set (f a) H
 2. pa \<in> H
[PROOF STEP]
using qa H(1)
[PROOF STATE]
proof (prove)
using this:
qa \<in> proj_set (f a) H
geodesic_segment_between H pa pb

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

goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f a) qa + dist qa pa \<le> dist (f a) pa + 4 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
have "... \<le> dist (f a) qa + K + 4 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) pa + 4 * deltaG TYPE('a) \<le> dist (f a) qa + K + 4 * delta
[PROOF STEP]
using I assms
[PROOF STATE]
proof (prove)
using this:
dist (f a) pa - dist (f a) qa - K \<le> 0
quasiconvex K G
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
a \<le> b
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G
?t \<in> {a..b} \<Longrightarrow> D \<le> infdist (f ?t) G
15 / 2 * delta + K + C / 2 \<le> D
deltaG TYPE('a) < delta
0 \<le> C
0 \<le> lambda

goal (1 subgoal):
 1. dist (f a) pa + 4 * deltaG TYPE('a) \<le> dist (f a) qa + K + 4 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f a) pa + 4 * deltaG TYPE('a) \<le> dist (f a) qa + K + 4 * delta

goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f a) qa + dist qa pa \<le> dist (f a) qa + K + 4 * delta
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (f a) qa + dist qa pa \<le> dist (f a) qa + K + 4 * delta

goal (1 subgoal):
 1. dist pa qa \<le> 4 * delta + K
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist pa qa \<le> 4 * delta + K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist pa qa \<le> 4 * delta + K

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have B: "dist qb pb \<le> 4 * delta + K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
have "dist (f b) pb - dist (f b) qb - K \<le> e" if "e > 0" for e::real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
have *: "infdist qb G < K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist qb G < K + e
[PROOF STEP]
using H(2)[OF proj_setD(1)[OF qb]] \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
infdist qb G \<le> K
0 < e

goal (1 subgoal):
 1. infdist qb G < K + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist qb G < K + e

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
obtain g where g: "g \<in> G" "dist qb g < K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; dist qb g < K + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infdist_almost_attained[OF *] proj_setD(1)[OF \<open>pa \<in> proj_set (f a) G\<close>]
[PROOF STATE]
proof (prove)
using this:
G \<noteq> {} \<Longrightarrow> \<exists>y\<in>G. dist qb y < K + e
pa \<in> G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; dist qb g < K + e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> G
dist qb g < K + e

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
have "dist (f b) pb \<le> dist (f b) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f b) pb \<le> dist (f b) g
[PROOF STEP]
unfolding proj_setD(2)[OF \<open>pb \<in> proj_set (f b) G\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f b) G \<le> dist (f b) g
[PROOF STEP]
using infdist_le[OF \<open>g \<in> G\<close>, of "f b"]
[PROOF STATE]
proof (prove)
using this:
infdist (f b) G \<le> dist (f b) g

goal (1 subgoal):
 1. infdist (f b) G \<le> dist (f b) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f b) pb \<le> dist (f b) g

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f b) pb \<le> dist (f b) g

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
have "... \<le> dist (f b) qb + dist qb g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f b) g \<le> dist (f b) qb + dist qb g
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist (f b) g \<le> dist (f b) qb + dist qb g

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f b) g \<le> dist (f b) qb + dist qb g

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
have "... \<le> dist (f b) qb + K + e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f b) qb + dist qb g \<le> dist (f b) qb + K + e
[PROOF STEP]
using g(2)
[PROOF STATE]
proof (prove)
using this:
dist qb g < K + e

goal (1 subgoal):
 1. dist (f b) qb + dist qb g \<le> dist (f b) qb + K + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f b) qb + dist qb g \<le> dist (f b) qb + K + e

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f b) pb \<le> dist (f b) qb + K + e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (f b) pb \<le> dist (f b) qb + K + e

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f b) pb - dist (f b) qb - K \<le> e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> dist (f b) pb - dist (f b) qb - K \<le> ?e

goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?e \<Longrightarrow> dist (f b) pb - dist (f b) qb - K \<le> ?e
[PROOF STEP]
have I: "dist (f b) pb - dist (f b) qb - K \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> dist (f b) pb - dist (f b) qb - K \<le> ?e

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> 0
[PROOF STEP]
using dense_ge
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> dist (f b) pb - dist (f b) qb - K \<le> ?e
(\<And>x. ?z < x \<Longrightarrow> ?y \<le> x) \<Longrightarrow> ?y \<le> ?z

goal (1 subgoal):
 1. dist (f b) pb - dist (f b) qb - K \<le> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist (f b) pb - dist (f b) qb - K \<le> 0

goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
have "dist (f b) qb + dist qb pb \<le> dist (f b) pb + 4 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f b) qb + dist qb pb \<le> dist (f b) pb + 4 * deltaG TYPE('a)
[PROOF STEP]
apply (rule dist_along_geodesic[OF geodesic_segmentI[OF H(1)]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. qb \<in> proj_set (f b) H
 2. pb \<in> H
[PROOF STEP]
using qb H(1)
[PROOF STATE]
proof (prove)
using this:
qb \<in> proj_set (f b) H
geodesic_segment_between H pa pb

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

goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f b) qb + dist qb pb \<le> dist (f b) pb + 4 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
have "... \<le> dist (f b) qb + K + 4 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f b) pb + 4 * deltaG TYPE('a) \<le> dist (f b) qb + K + 4 * delta
[PROOF STEP]
using I assms
[PROOF STATE]
proof (prove)
using this:
dist (f b) pb - dist (f b) qb - K \<le> 0
quasiconvex K G
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
a \<le> b
pa \<in> proj_set (f a) G
pb \<in> proj_set (f b) G
?t \<in> {a..b} \<Longrightarrow> D \<le> infdist (f ?t) G
15 / 2 * delta + K + C / 2 \<le> D
deltaG TYPE('a) < delta
0 \<le> C
0 \<le> lambda

goal (1 subgoal):
 1. dist (f b) pb + 4 * deltaG TYPE('a) \<le> dist (f b) qb + K + 4 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f b) pb + 4 * deltaG TYPE('a) \<le> dist (f b) qb + K + 4 * delta

goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f b) qb + dist qb pb \<le> dist (f b) qb + K + 4 * delta
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (f b) qb + dist qb pb \<le> dist (f b) qb + K + 4 * delta

goal (1 subgoal):
 1. dist qb pb \<le> 4 * delta + K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist qb pb \<le> 4 * delta + K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist qb pb \<le> 4 * delta + K

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
have "dist pa pb \<le> dist pa qa + dist qa qb + dist qb pb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist pa pb \<le> dist pa qa + dist qa qb + dist qb pb
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist pa pb \<le> dist pa qa + dist qa qb + dist qb pb

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist pa pb \<le> dist pa qa + dist qa qb + dist qb pb
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist pa pb \<le> dist pa qa + dist qa qb + dist qb pb

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
using Q A B
[PROOF STATE]
proof (prove)
using this:
dist pa pb \<le> dist pa qa + dist qa qb + dist qb pb
dist qa qb \<le> max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
dist pa qa \<le> 4 * delta + K
dist qb pb \<le> 4 * delta + K

goal (1 subgoal):
 1. dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist pa pb \<le> 2 * K + 8 * delta + max (5 * deltaG TYPE('a)) (4 * exp (1 / 2 * ln 2) * lambda * (b - a) * exp (- (D - K - C / 2) * ln 2 / (5 * delta)))

goal:
No subgoals!
[PROOF STEP]
qed