[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) geodesic_projection_exp_contracting_aux:
  assumes "geodesic_segment G"
          "px \<in> proj_set x G"
          "py \<in> proj_set y G"
          "delta \<ge> deltaG(TYPE('a))"
          "dist x y \<le> 10 * delta + C"
          "M \<ge> 15/2 * delta"
          "dist px x \<ge> M + 5 * delta + C/2"
          "dist py y \<ge> M + 5 * delta + C/2"
          "C \<ge> 0"
  shows "dist (geodesic_segment_param {px--x} px M)
              (geodesic_segment_param {py--y} py M) \<le> 5 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist px x \<le> dist py x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x \<le> dist py x
[PROOF STEP]
using proj_setD(2)[OF assms(2)] infdist_le[OF proj_setD(1)[OF assms(3)], of x]
[PROOF STATE]
proof (prove)
using this:
dist x px = infdist x G
infdist x G \<le> dist x py

goal (1 subgoal):
 1. dist px x \<le> dist py x
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist px x \<le> dist py x

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist py y \<le> dist px y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py y \<le> dist px y
[PROOF STEP]
using proj_setD(2)[OF assms(3)] infdist_le[OF proj_setD(1)[OF assms(2)], of y]
[PROOF STATE]
proof (prove)
using this:
dist y py = infdist y G
infdist y G \<le> dist y px

goal (1 subgoal):
 1. dist py y \<le> dist px y
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist py y \<le> dist px y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "delta \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> delta
[PROOF STEP]
using assms local.delta_nonneg
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C
0 \<le> deltaG TYPE('a)

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

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> delta
[PROOF STEP]
have M: "M \<ge> 0" "M \<le> dist px x" "M \<le> dist px y" "M \<le> dist py x" "M \<le> dist py y"
[PROOF STATE]
proof (prove)
using this:
0 \<le> delta

goal (1 subgoal):
 1. (0 \<le> M &&& M \<le> dist px x) &&& M \<le> dist px y &&& M \<le> dist py x &&& M \<le> dist py y
[PROOF STEP]
using assms \<open>dist px x \<le> dist py x\<close> \<open>dist py y \<le> dist px y \<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> delta
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C
dist px x \<le> dist py x
dist py y \<le> dist px y

goal (1 subgoal):
 1. (0 \<le> M &&& M \<le> dist px x) &&& M \<le> dist px y &&& M \<le> dist py x &&& M \<le> dist py y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "px \<in> G" "py \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. px \<in> G &&& py \<in> G
[PROOF STEP]
using assms proj_setD
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C
?y \<in> proj_set ?x ?A \<Longrightarrow> ?y \<in> ?A
?y \<in> proj_set ?x ?A \<Longrightarrow> dist ?x ?y = infdist ?x ?A

goal (1 subgoal):
 1. px \<in> G &&& py \<in> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
px \<in> G
py \<in> G

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
define x' where "x' = geodesic_segment_param {px--x} px M"
[PROOF STATE]
proof (state)
this:
x' = geodesic_segment_param {px--x} px M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
define y' where "y' = geodesic_segment_param {py--y} py M"
[PROOF STATE]
proof (state)
this:
y' = geodesic_segment_param {py--y} py M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
text \<open>First step: the distance between $px$ and $py$ is at most $5\delta$.\<close>
[PROOF STATE]
proof (state)
this:
y' = geodesic_segment_param {py--y} py M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist px py \<le> max (5 * deltaG(TYPE('a))) (dist x y - dist px x - dist py y + 10 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a))
[PROOF STEP]
by (rule proj_along_geodesic_contraction[OF assms(1) assms(2) assms(3)])
[PROOF STATE]
proof (state)
this:
dist px py \<le> max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist px py \<le> max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> max (5 * deltaG(TYPE('a))) (5 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a)) \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. deltaG TYPE('a) \<le> deltaG TYPE('a)
 2. 0 \<le> 5
 3. dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
using assms \<open>delta \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C
0 \<le> delta

goal (3 subgoals):
 1. deltaG TYPE('a) \<le> deltaG TYPE('a)
 2. 0 \<le> 5
 3. dist x y - dist px x - dist py y + 10 * deltaG TYPE('a) \<le> 5 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (5 * deltaG TYPE('a)) (dist x y - dist px x - dist py y + 10 * deltaG TYPE('a)) \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist px py \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))
[PROOF STEP]
have "dist px py \<le> 5 * delta"
[PROOF STATE]
proof (prove)
using this:
dist px py \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))

goal (1 subgoal):
 1. dist px py \<le> 5 * delta
[PROOF STEP]
using \<open>delta \<ge> deltaG(TYPE('a))\<close>
[PROOF STATE]
proof (prove)
using this:
dist px py \<le> max (5 * deltaG TYPE('a)) (5 * deltaG TYPE('a))
deltaG TYPE('a) \<le> delta

goal (1 subgoal):
 1. dist px py \<le> 5 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist px py \<le> 5 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
text \<open>Second step: show that all the interesting Gromov products at bounded below by $M$.\<close>
[PROOF STATE]
proof (state)
this:
dist px py \<le> 5 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have *: "x' \<in> {px--x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<in> {px--x}
[PROOF STEP]
unfolding x'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param {px--x} px M \<in> {px--x}
[PROOF STEP]
by (simp add: geodesic_segment_param_in_segment)
[PROOF STATE]
proof (state)
this:
x' \<in> {px--x}

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "px \<in> proj_set x' G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. px \<in> proj_set x' G
[PROOF STEP]
by (rule proj_set_geodesic_same_basepoint[OF \<open>px \<in> proj_set x G\<close> _ *], auto)
[PROOF STATE]
proof (state)
this:
px \<in> proj_set x' G

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist px x' = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x' = M
[PROOF STEP]
unfolding x'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px (geodesic_segment_param {px--x} px M) = M
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. dist px (geodesic_segment_param {px--x} px M) = M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist px x' = M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist px x' \<le> dist py x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x' \<le> dist py x'
[PROOF STEP]
using proj_setD(2)[OF \<open>px \<in> proj_set x' G\<close>] infdist_le[OF proj_setD(1)[OF assms(3)], of x']
[PROOF STATE]
proof (prove)
using this:
dist x' px = infdist x' G
infdist x' G \<le> dist x' py

goal (1 subgoal):
 1. dist px x' \<le> dist py x'
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist px x' \<le> dist py x'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have **: "dist px x = dist px x' + dist x' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x = dist px x' + dist x' x
[PROOF STEP]
using geodesic_segment_dist[OF _ *, of px x]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between {px--x} px x \<Longrightarrow> dist px x' + dist x' x = dist px x

goal (1 subgoal):
 1. dist px x = dist px x' + dist x' x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist px x = dist px x' + dist x' x

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have Ixx: "Gromov_product_at px x' x = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gromov_product_at px x' x = M
[PROOF STEP]
unfolding Gromov_product_at_def ** x'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dist px (geodesic_segment_param {px--x} px M) + (dist px (geodesic_segment_param {px--x} px M) + dist (geodesic_segment_param {px--x} px M) x) - dist (geodesic_segment_param {px--x} px M) x) / 2 = M
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. (dist px (geodesic_segment_param {px--x} px M) + (dist px (geodesic_segment_param {px--x} px M) + dist (geodesic_segment_param {px--x} px M) x) - dist (geodesic_segment_param {px--x} px M) x) / 2 = M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gromov_product_at px x' x = M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "2 * M = dist px x' + dist px x - dist x' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M = dist px x' + dist px x - dist x' x
[PROOF STEP]
unfolding ** x'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M = dist px (geodesic_segment_param {px--x} px M) + (dist px (geodesic_segment_param {px--x} px M) + dist (geodesic_segment_param {px--x} px M) x) - dist (geodesic_segment_param {px--x} px M) x
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. 2 * M = dist px (geodesic_segment_param {px--x} px M) + (dist px (geodesic_segment_param {px--x} px M) + dist (geodesic_segment_param {px--x} px M) x) - dist (geodesic_segment_param {px--x} px M) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M = dist px x' + dist px x - dist x' x

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * M = dist px x' + dist px x - dist x' x

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> dist py x' + dist py x - dist x' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x' + dist px x - dist x' x \<le> dist py x' + dist py x - dist x' x
[PROOF STEP]
apply (intro mono_intros, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist px x' \<le> dist py x'
 2. dist px x \<le> dist py x
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
dist px x' + dist px x - dist x' x \<le> dist py x' + dist py x - dist x' x

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist px x' + dist px x - dist x' x \<le> dist py x' + dist py x - dist x' x

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... = 2 * Gromov_product_at py x x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py x' + dist py x - dist x' x = 2 * Gromov_product_at py x x'
[PROOF STEP]
unfolding Gromov_product_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py x' + dist py x - dist x' x = 2 * ((dist py x + dist py x' - dist x x') / 2)
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist py x' + dist py x - dist x' x = 2 * Gromov_product_at py x x'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * M \<le> 2 * Gromov_product_at py x x'
[PROOF STEP]
have Iyx: "Gromov_product_at py x x' \<ge> M"
[PROOF STATE]
proof (prove)
using this:
2 * M \<le> 2 * Gromov_product_at py x x'

goal (1 subgoal):
 1. M \<le> Gromov_product_at py x x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<le> Gromov_product_at py x x'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have *: "y' \<in> {py--y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y' \<in> {py--y}
[PROOF STEP]
unfolding y'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param {py--y} py M \<in> {py--y}
[PROOF STEP]
by (simp add: geodesic_segment_param_in_segment)
[PROOF STATE]
proof (state)
this:
y' \<in> {py--y}

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "py \<in> proj_set y' G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. py \<in> proj_set y' G
[PROOF STEP]
by (rule proj_set_geodesic_same_basepoint[OF \<open>py \<in> proj_set y G\<close> _ *], auto)
[PROOF STATE]
proof (state)
this:
py \<in> proj_set y' G

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist py y' = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py y' = M
[PROOF STEP]
unfolding y'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py (geodesic_segment_param {py--y} py M) = M
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. dist py (geodesic_segment_param {py--y} py M) = M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist py y' = M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist py y' \<le> dist px y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py y' \<le> dist px y'
[PROOF STEP]
using proj_setD(2)[OF \<open>py \<in> proj_set y' G\<close>] infdist_le[OF proj_setD(1)[OF assms(2)], of y']
[PROOF STATE]
proof (prove)
using this:
dist y' py = infdist y' G
infdist y' G \<le> dist y' px

goal (1 subgoal):
 1. dist py y' \<le> dist px y'
[PROOF STEP]
by (simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist py y' \<le> dist px y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have **: "dist py y = dist py y' + dist y' y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py y = dist py y' + dist y' y
[PROOF STEP]
using geodesic_segment_dist[OF _ *, of py y]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between {py--y} py y \<Longrightarrow> dist py y' + dist y' y = dist py y

goal (1 subgoal):
 1. dist py y = dist py y' + dist y' y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist py y = dist py y' + dist y' y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have Iyy: "Gromov_product_at py y' y = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gromov_product_at py y' y = M
[PROOF STEP]
unfolding Gromov_product_at_def ** y'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dist py (geodesic_segment_param {py--y} py M) + (dist py (geodesic_segment_param {py--y} py M) + dist (geodesic_segment_param {py--y} py M) y) - dist (geodesic_segment_param {py--y} py M) y) / 2 = M
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. (dist py (geodesic_segment_param {py--y} py M) + (dist py (geodesic_segment_param {py--y} py M) + dist (geodesic_segment_param {py--y} py M) y) - dist (geodesic_segment_param {py--y} py M) y) / 2 = M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gromov_product_at py y' y = M

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "2 * M = dist py y' + dist py y - dist y' y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M = dist py y' + dist py y - dist y' y
[PROOF STEP]
unfolding ** y'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M = dist py (geodesic_segment_param {py--y} py M) + (dist py (geodesic_segment_param {py--y} py M) + dist (geodesic_segment_param {py--y} py M) y) - dist (geodesic_segment_param {py--y} py M) y
[PROOF STEP]
using M
[PROOF STATE]
proof (prove)
using this:
0 \<le> M
M \<le> dist px x
M \<le> dist px y
M \<le> dist py x
M \<le> dist py y

goal (1 subgoal):
 1. 2 * M = dist py (geodesic_segment_param {py--y} py M) + (dist py (geodesic_segment_param {py--y} py M) + dist (geodesic_segment_param {py--y} py M) y) - dist (geodesic_segment_param {py--y} py M) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M = dist py y' + dist py y - dist y' y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * M = dist py y' + dist py y - dist y' y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> dist px y' + dist px y - dist y' y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py y' + dist py y - dist y' y \<le> dist px y' + dist px y - dist y' y
[PROOF STEP]
apply (intro mono_intros, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist py y' \<le> dist px y'
 2. dist py y \<le> dist px y
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
dist py y' + dist py y - dist y' y \<le> dist px y' + dist px y - dist y' y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist py y' + dist py y - dist y' y \<le> dist px y' + dist px y - dist y' y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... = 2 * Gromov_product_at px y y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px y' + dist px y - dist y' y = 2 * Gromov_product_at px y y'
[PROOF STEP]
unfolding Gromov_product_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px y' + dist px y - dist y' y = 2 * ((dist px y + dist px y' - dist y y') / 2)
[PROOF STEP]
by (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (state)
this:
dist px y' + dist px y - dist y' y = 2 * Gromov_product_at px y y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * M \<le> 2 * Gromov_product_at px y y'
[PROOF STEP]
have Ixy: "Gromov_product_at px y y' \<ge> M"
[PROOF STATE]
proof (prove)
using this:
2 * M \<le> 2 * Gromov_product_at px y y'

goal (1 subgoal):
 1. M \<le> Gromov_product_at px y y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<le> Gromov_product_at px y y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "2 * M \<le> dist px x + dist py y - dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M \<le> dist px x + dist py y - dist x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C

goal (1 subgoal):
 1. 2 * M \<le> dist px x + dist py y - dist x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M \<le> dist px x + dist py y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * M \<le> dist px x + dist py y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> dist px x + dist px y - dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x + dist py y - dist x y \<le> dist px x + dist px y - dist x y
[PROOF STEP]
by (intro mono_intros, fact)
[PROOF STATE]
proof (state)
this:
dist px x + dist py y - dist x y \<le> dist px x + dist px y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist px x + dist py y - dist x y \<le> dist px x + dist px y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... = 2 * Gromov_product_at px x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x + dist px y - dist x y = 2 * Gromov_product_at px x y
[PROOF STEP]
unfolding Gromov_product_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x + dist px y - dist x y = 2 * ((dist px x + dist px y - dist x y) / 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist px x + dist px y - dist x y = 2 * Gromov_product_at px x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * M \<le> 2 * Gromov_product_at px x y
[PROOF STEP]
have Ix: "Gromov_product_at px x y \<ge> M"
[PROOF STATE]
proof (prove)
using this:
2 * M \<le> 2 * Gromov_product_at px x y

goal (1 subgoal):
 1. M \<le> Gromov_product_at px x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<le> Gromov_product_at px x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "2 * M \<le> dist px x + dist py y - dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M \<le> dist px x + dist py y - dist x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C

goal (1 subgoal):
 1. 2 * M \<le> dist px x + dist py y - dist x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M \<le> dist px x + dist py y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * M \<le> dist px x + dist py y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> dist py x + dist py y - dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px x + dist py y - dist x y \<le> dist py x + dist py y - dist x y
[PROOF STEP]
by (intro mono_intros, fact)
[PROOF STATE]
proof (state)
this:
dist px x + dist py y - dist x y \<le> dist py x + dist py y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist px x + dist py y - dist x y \<le> dist py x + dist py y - dist x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... = 2 * Gromov_product_at py x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py x + dist py y - dist x y = 2 * Gromov_product_at py x y
[PROOF STEP]
unfolding Gromov_product_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist py x + dist py y - dist x y = 2 * ((dist py x + dist py y - dist x y) / 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist py x + dist py y - dist x y = 2 * Gromov_product_at py x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * M \<le> 2 * Gromov_product_at py x y
[PROOF STEP]
have Iy: "Gromov_product_at py x y \<ge> M"
[PROOF STATE]
proof (prove)
using this:
2 * M \<le> 2 * Gromov_product_at py x y

goal (1 subgoal):
 1. M \<le> Gromov_product_at py x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<le> Gromov_product_at py x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
text \<open>Third step: prove the estimate\<close>
[PROOF STATE]
proof (state)
this:
M \<le> Gromov_product_at py x y

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "M - 2 * delta \<le> Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M - 2 * delta \<le> Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG TYPE('a)
[PROOF STEP]
using Ixx Ixy Ix \<open>delta \<ge> deltaG(TYPE('a))\<close>
[PROOF STATE]
proof (prove)
using this:
Gromov_product_at px x' x = M
M \<le> Gromov_product_at px y y'
M \<le> Gromov_product_at px x y
deltaG TYPE('a) \<le> delta

goal (1 subgoal):
 1. M - 2 * delta \<le> Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M - 2 * delta \<le> Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M - 2 * delta \<le> Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> Gromov_product_at px x' y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG TYPE('a) \<le> Gromov_product_at px x' y'
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
Min {Gromov_product_at px x' x, Gromov_product_at px x y, Gromov_product_at px y y'} - 2 * deltaG TYPE('a) \<le> Gromov_product_at px x' y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M - 2 * delta \<le> Gromov_product_at px x' y'
[PROOF STEP]
have A: "M - 4 * delta + dist x' y' \<le> dist px y'"
[PROOF STATE]
proof (prove)
using this:
M - 2 * delta \<le> Gromov_product_at px x' y'

goal (1 subgoal):
 1. M - 4 * delta + dist x' y' \<le> dist px y'
[PROOF STEP]
unfolding Gromov_product_at_def \<open>dist px x' = M\<close>
[PROOF STATE]
proof (prove)
using this:
M - 2 * delta \<le> (M + dist px y' - dist x' y') / 2

goal (1 subgoal):
 1. M - 4 * delta + dist x' y' \<le> dist px y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M - 4 * delta + dist x' y' \<le> dist px y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "M - 2 * delta \<le> Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M - 2 * delta \<le> Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG TYPE('a)
[PROOF STEP]
using Iyx Iyy Iy \<open>delta \<ge> deltaG(TYPE('a))\<close>
[PROOF STATE]
proof (prove)
using this:
M \<le> Gromov_product_at py x x'
Gromov_product_at py y' y = M
M \<le> Gromov_product_at py x y
deltaG TYPE('a) \<le> delta

goal (1 subgoal):
 1. M - 2 * delta \<le> Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG TYPE('a)
[PROOF STEP]
by (auto simp add: Gromov_product_commute)
[PROOF STATE]
proof (state)
this:
M - 2 * delta \<le> Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M - 2 * delta \<le> Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> Gromov_product_at py x' y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG TYPE('a) \<le> Gromov_product_at py x' y'
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
Min {Gromov_product_at py x' x, Gromov_product_at py x y, Gromov_product_at py y y'} - 2 * deltaG TYPE('a) \<le> Gromov_product_at py x' y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M - 2 * delta \<le> Gromov_product_at py x' y'
[PROOF STEP]
have B: "M - 4 * delta + dist x' y' \<le> dist py x'"
[PROOF STATE]
proof (prove)
using this:
M - 2 * delta \<le> Gromov_product_at py x' y'

goal (1 subgoal):
 1. M - 4 * delta + dist x' y' \<le> dist py x'
[PROOF STEP]
unfolding Gromov_product_at_def \<open>dist py y' = M\<close>
[PROOF STATE]
proof (prove)
using this:
M - 2 * delta \<le> (dist py x' + M - dist x' y') / 2

goal (1 subgoal):
 1. M - 4 * delta + dist x' y' \<le> dist py x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M - 4 * delta + dist x' y' \<le> dist py x'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "dist px py \<le> 2 * M - 10 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px py \<le> 2 * M - 10 * delta
[PROOF STEP]
using assms \<open>dist px py \<le> 5 * delta\<close>
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
px \<in> proj_set x G
py \<in> proj_set y G
deltaG TYPE('a) \<le> delta
dist x y \<le> 10 * delta + C
15 / 2 * delta \<le> M
M + 5 * delta + C / 2 \<le> dist px x
M + 5 * delta + C / 2 \<le> dist py y
0 \<le> C
dist px py \<le> 5 * delta

goal (1 subgoal):
 1. dist px py \<le> 2 * M - 10 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist px py \<le> 2 * M - 10 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "2 * M - 8 * delta + 2 * dist x' y' \<le> dist px y' + dist py x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M - 8 * delta + 2 * dist x' y' \<le> dist px y' + dist py x'
[PROOF STEP]
using A B
[PROOF STATE]
proof (prove)
using this:
M - 4 * delta + dist x' y' \<le> dist px y'
M - 4 * delta + dist x' y' \<le> dist py x'

goal (1 subgoal):
 1. 2 * M - 8 * delta + 2 * dist x' y' \<le> dist px y' + dist py x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M - 8 * delta + 2 * dist x' y' \<le> dist px y' + dist py x'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * M - 8 * delta + 2 * dist x' y' \<le> dist px y' + dist py x'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist px y' + dist py x' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a)
[PROOF STEP]
by (rule hyperb_quad_ineq)
[PROOF STATE]
proof (state)
this:
dist px y' + dist py x' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist px y' + dist py x' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
have "... \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a) \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta
[PROOF STEP]
using \<open>deltaG(TYPE('a)) \<le> delta\<close>
[PROOF STATE]
proof (prove)
using this:
deltaG TYPE('a) \<le> delta

goal (1 subgoal):
 1. max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a) \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * deltaG TYPE('a) \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * M - 8 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta
[PROOF STEP]
have "2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py)"
[PROOF STATE]
proof (prove)
using this:
2 * M - 8 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py) + 2 * delta

goal (1 subgoal):
 1. 2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py)

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py)
[PROOF STEP]
have "2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'"
[PROOF STATE]
proof (prove)
using this:
2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist y' x') (dist px x' + dist y' py)

goal (1 subgoal):
 1. 2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'
[PROOF STEP]
apply (auto simp add: metric_space_class.dist_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist x' y') (dist px x' + dist py y') \<Longrightarrow> 2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'
[PROOF STEP]
using \<open>0 \<le> delta\<close> \<open>dist px py \<le> 2 * M - 10 * delta\<close> \<open>dist px x' = M\<close> \<open>dist py y' = M\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> delta
dist px py \<le> 2 * M - 10 * delta
dist px x' = M
dist py y' = M

goal (1 subgoal):
 1. 2 * M - 10 * delta + 2 * dist x' y' \<le> max (dist px py + dist x' y') (dist px x' + dist py y') \<Longrightarrow> 2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'
[PROOF STEP]
have "dist x' y' \<le> 5 * delta"
[PROOF STATE]
proof (prove)
using this:
2 * M - 10 * delta + 2 * dist x' y' \<le> dist px x' + dist py y'

goal (1 subgoal):
 1. dist x' y' \<le> 5 * delta
[PROOF STEP]
unfolding \<open>dist px x' = M\<close> \<open>dist py y' = M\<close>
[PROOF STATE]
proof (prove)
using this:
2 * M - 10 * delta + 2 * dist x' y' \<le> M + M

goal (1 subgoal):
 1. dist x' y' \<le> 5 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x' y' \<le> 5 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x' y' \<le> 5 * delta
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x' y' \<le> 5 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
unfolding x'_def y'_def
[PROOF STATE]
proof (prove)
using this:
dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta

goal (1 subgoal):
 1. dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param {px--x} px M) (geodesic_segment_param {py--y} py M) \<le> 5 * delta

goal:
No subgoals!
[PROOF STEP]
qed