[STATEMENT]
lemma unique_x_axis_poincare_distance_positive:
  assumes "d \<ge> 0"
  shows "\<exists>! z. is_real z \<and> Re z \<ge> 0 \<and> Re z < 1 \<and>
               poincare_distance 0\<^sub>h (of_complex z) = d" (is "\<exists>! z. is_real z \<and> Re z \<ge> 0 \<and> Re z < 1 \<and> ?P z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
obtain z where *: "is_real z" "Re z \<le> 0" "Re z > -1" "?P z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>is_real z; Re z \<le> 0; - 1 < Re z; poincare_distance 0\<^sub>h (of_complex z) = d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using unique_x_axis_poincare_distance_negative[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>is_real z; Re z \<le> 0; - 1 < Re z; poincare_distance 0\<^sub>h (of_complex z) = d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real z
Re z \<le> 0
- 1 < Re z
poincare_distance 0\<^sub>h (of_complex z) = d

goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
hence **: "of_complex z \<in> unit_disc" "of_complex z \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
is_real z
Re z \<le> 0
- 1 < Re z
poincare_distance 0\<^sub>h (of_complex z) = d

goal (1 subgoal):
 1. of_complex z \<in> unit_disc &&& of_complex z \<in> circline_set x_axis
[PROOF STEP]
by (auto simp add: cmod_eq_Re circline_set_x_axis)
[PROOF STATE]
proof (state)
this:
of_complex z \<in> unit_disc
of_complex z \<in> circline_set x_axis

goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_real ?a \<and> 0 \<le> Re ?a \<and> Re ?a < 1 \<and> poincare_distance 0\<^sub>h (of_complex ?a) = d
 2. \<And>z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d \<Longrightarrow> z = ?a
[PROOF STEP]
show "is_real (-z) \<and> Re (-z) \<ge> 0 \<and> Re (-z) < 1 \<and> ?P (-z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (- z) \<and> 0 \<le> Re (- z) \<and> Re (- z) < 1 \<and> poincare_distance 0\<^sub>h (of_complex (- z)) = d
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
is_real z
Re z \<le> 0
- 1 < Re z
poincare_distance 0\<^sub>h (of_complex z) = d
of_complex z \<in> unit_disc
of_complex z \<in> circline_set x_axis

goal (1 subgoal):
 1. is_real (- z) \<and> 0 \<le> Re (- z) \<and> Re (- z) < 1 \<and> poincare_distance 0\<^sub>h (of_complex (- z)) = d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_real (- z) \<and> 0 \<le> Re (- z) \<and> Re (- z) < 1 \<and> poincare_distance 0\<^sub>h (of_complex (- z)) = d

goal (1 subgoal):
 1. \<And>za. is_real za \<and> 0 \<le> Re za \<and> Re za < 1 \<and> poincare_distance 0\<^sub>h (of_complex za) = d \<Longrightarrow> za = - z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>za. is_real za \<and> 0 \<le> Re za \<and> Re za < 1 \<and> poincare_distance 0\<^sub>h (of_complex za) = d \<Longrightarrow> za = - z
[PROOF STEP]
fix z'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>za. is_real za \<and> 0 \<le> Re za \<and> Re za < 1 \<and> poincare_distance 0\<^sub>h (of_complex za) = d \<Longrightarrow> za = - z
[PROOF STEP]
assume "is_real z' \<and> Re z' \<ge> 0 \<and> Re z' < 1 \<and> ?P z'"
[PROOF STATE]
proof (state)
this:
is_real z' \<and> 0 \<le> Re z' \<and> Re z' < 1 \<and> poincare_distance 0\<^sub>h (of_complex z') = d

goal (1 subgoal):
 1. \<And>za. is_real za \<and> 0 \<le> Re za \<and> Re za < 1 \<and> poincare_distance 0\<^sub>h (of_complex za) = d \<Longrightarrow> za = - z
[PROOF STEP]
hence "is_real (-z') \<and> Re (-z') \<le> 0 \<and> Re (-z') > -1 \<and> ?P (-z')"
[PROOF STATE]
proof (prove)
using this:
is_real z' \<and> 0 \<le> Re z' \<and> Re z' < 1 \<and> poincare_distance 0\<^sub>h (of_complex z') = d

goal (1 subgoal):
 1. is_real (- z') \<and> Re (- z') \<le> 0 \<and> - 1 < Re (- z') \<and> poincare_distance 0\<^sub>h (of_complex (- z')) = d
[PROOF STEP]
by (auto simp add: circline_set_x_axis cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
is_real (- z') \<and> Re (- z') \<le> 0 \<and> - 1 < Re (- z') \<and> poincare_distance 0\<^sub>h (of_complex (- z')) = d

goal (1 subgoal):
 1. \<And>za. is_real za \<and> 0 \<le> Re za \<and> Re za < 1 \<and> poincare_distance 0\<^sub>h (of_complex za) = d \<Longrightarrow> za = - z
[PROOF STEP]
hence "-z' = z"
[PROOF STATE]
proof (prove)
using this:
is_real (- z') \<and> Re (- z') \<le> 0 \<and> - 1 < Re (- z') \<and> poincare_distance 0\<^sub>h (of_complex (- z')) = d

goal (1 subgoal):
 1. - z' = z
[PROOF STEP]
using unique_x_axis_poincare_distance_negative[OF assms] *
[PROOF STATE]
proof (prove)
using this:
is_real (- z') \<and> Re (- z') \<le> 0 \<and> - 1 < Re (- z') \<and> poincare_distance 0\<^sub>h (of_complex (- z')) = d
\<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
is_real z
Re z \<le> 0
- 1 < Re z
poincare_distance 0\<^sub>h (of_complex z) = d

goal (1 subgoal):
 1. - z' = z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- z' = z

goal (1 subgoal):
 1. \<And>za. is_real za \<and> 0 \<le> Re za \<and> Re za < 1 \<and> poincare_distance 0\<^sub>h (of_complex za) = d \<Longrightarrow> za = - z
[PROOF STEP]
thus "z' = -z"
[PROOF STATE]
proof (prove)
using this:
- z' = z

goal (1 subgoal):
 1. z' = - z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z' = - z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poincare_distance_eq_ex_moebius:
  assumes in_disc: "u \<in> unit_disc" and "v \<in> unit_disc" and "u' \<in> unit_disc" and "v' \<in> unit_disc"
  assumes "poincare_distance u v = poincare_distance u' v'"
  shows "\<exists> M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'" (is "?P' u v u' v'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
proof (cases "u = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
 2. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
 2. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
using assms poincare_distance_eq_0_iff[of u' v']
[PROOF STATE]
proof (prove)
using this:
u = v
u \<in> unit_disc
v \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
\<lbrakk>u' \<in> unit_disc; v' \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance u' v' = 0) = (u' = v')

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
by (simp add: unit_disc_fix_transitive)
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
have "\<forall> u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow>
                 ?P' u' v' u v" (is "?P u v")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
proof (rule wlog_positive_x_axis[where P="?P"])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>u' v'. 0\<^sub>h \<noteq> of_complex x \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>u' v'. 0\<^sub>h \<noteq> of_complex x \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x)
[PROOF STEP]
assume "is_real x" "0 < Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 < Re x
Re x < 1

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>u' v'. 0\<^sub>h \<noteq> of_complex x \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x)
[PROOF STEP]
hence "of_complex x \<in> unit_disc" "of_complex x \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. of_complex x \<in> unit_disc &&& of_complex x \<in> circline_set x_axis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. of_complex x \<in> unit_disc &&& of_complex x \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
of_complex x \<in> unit_disc
of_complex x \<in> circline_set x_axis

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>u' v'. 0\<^sub>h \<noteq> of_complex x \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x)
[PROOF STEP]
show "?P 0\<^sub>h (of_complex x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u' v'. 0\<^sub>h \<noteq> of_complex x \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
fix u' v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
assume "0\<^sub>h \<noteq> of_complex x" and in_disc: "u' \<in> unit_disc" "v' \<in> unit_disc" and
             "poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'"
[PROOF STATE]
proof (state)
this:
0\<^sub>h \<noteq> of_complex x
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
hence "u' \<noteq> v'" "poincare_distance u' v' > 0"
[PROOF STATE]
proof (prove)
using this:
0\<^sub>h \<noteq> of_complex x
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'

goal (1 subgoal):
 1. u' \<noteq> v' &&& 0 < poincare_distance u' v'
[PROOF STEP]
using poincare_distance_eq_0_iff[of "0\<^sub>h" "of_complex x"] \<open>of_complex x \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
0\<^sub>h \<noteq> of_complex x
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
\<lbrakk>0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance 0\<^sub>h (of_complex x) = 0) = (0\<^sub>h = of_complex x)
of_complex x \<in> unit_disc

goal (1 subgoal):
 1. u' \<noteq> v' &&& 0 < poincare_distance u' v'
[PROOF STEP]
using poincare_distance_ge0[of "0\<^sub>h" "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
0\<^sub>h \<noteq> of_complex x
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
\<lbrakk>0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance 0\<^sub>h (of_complex x) = 0) = (0\<^sub>h = of_complex x)
of_complex x \<in> unit_disc
\<lbrakk>0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> 0 \<le> poincare_distance 0\<^sub>h (of_complex x)

goal (1 subgoal):
 1. u' \<noteq> v' &&& 0 < poincare_distance u' v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' \<noteq> v'
0 < poincare_distance u' v'

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u' \<noteq> v'
0 < poincare_distance u' v'
[PROOF STEP]
obtain M where M: "unit_disc_fix M" "moebius_pt M u' = 0\<^sub>h" "moebius_pt M v' \<in> positive_x_axis"
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> v'
0 < poincare_distance u' v'

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>unit_disc_fix M; moebius_pt M u' = 0\<^sub>h; moebius_pt M v' \<in> positive_x_axis\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_unit_disc_fix_to_zero_positive_x_axis[of u' v'] in_disc
[PROOF STATE]
proof (prove)
using this:
u' \<noteq> v'
0 < poincare_distance u' v'
\<lbrakk>u' \<in> unit_disc; v' \<in> unit_disc; u' \<noteq> v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' \<in> positive_x_axis
u' \<in> unit_disc
v' \<in> unit_disc

goal (1 subgoal):
 1. (\<And>M. \<lbrakk>unit_disc_fix M; moebius_pt M u' = 0\<^sub>h; moebius_pt M v' \<in> positive_x_axis\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> positive_x_axis

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> positive_x_axis
[PROOF STEP]
obtain Mv' where Mv': "moebius_pt M v' = of_complex Mv'"
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> positive_x_axis

goal (1 subgoal):
 1. (\<And>Mv'. moebius_pt M v' = of_complex Mv' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of "moebius_pt M v'"] in_disc unit_disc_fix_iff[of M]
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> positive_x_axis
moebius_pt M v' = \<infinity>\<^sub>h \<or> (\<exists>x. moebius_pt M v' = of_complex x)
u' \<in> unit_disc
v' \<in> unit_disc
unit_disc_fix M \<Longrightarrow> moebius_pt M ` unit_disc = unit_disc

goal (1 subgoal):
 1. (\<And>Mv'. moebius_pt M v' = of_complex Mv' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis image_eqI inf_notin_unit_disc)
[PROOF STATE]
proof (state)
this:
moebius_pt M v' = of_complex Mv'

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
have "moebius_pt M v' \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt M v' \<in> unit_disc
[PROOF STEP]
using M(1) \<open>v' \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
v' \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt M v' \<in> unit_disc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
moebius_pt M v' \<in> unit_disc

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
have "Re Mv' > 0" "is_real Mv'" "Re Mv' < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Re Mv' &&& is_real Mv' &&& Re Mv' < 1
[PROOF STEP]
using M Mv' of_complex_inj \<open>moebius_pt M v' \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> positive_x_axis
moebius_pt M v' = of_complex Mv'
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y
moebius_pt M v' \<in> unit_disc

goal (1 subgoal):
 1. 0 < Re Mv' &&& is_real Mv' &&& Re Mv' < 1
[PROOF STEP]
unfolding positive_x_axis_def circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> {z \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}. z \<noteq> \<infinity>\<^sub>h \<and> 0 < Re (to_complex z)}
moebius_pt M v' = of_complex Mv'
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y
moebius_pt M v' \<in> unit_disc

goal (1 subgoal):
 1. 0 < Re Mv' &&& is_real Mv' &&& Re Mv' < 1
[PROOF STEP]
using cmod_eq_Re
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> {z \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}. z \<noteq> \<infinity>\<^sub>h \<and> 0 < Re (to_complex z)}
moebius_pt M v' = of_complex Mv'
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y
moebius_pt M v' \<in> unit_disc
is_real ?z \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>

goal (1 subgoal):
 1. 0 < Re Mv' &&& is_real Mv' &&& Re Mv' < 1
[PROOF STEP]
by auto fastforce
[PROOF STATE]
proof (state)
this:
0 < Re Mv'
is_real Mv'
Re Mv' < 1

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
have "poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
[PROOF STEP]
using M(1)
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
[PROOF STEP]
using in_disc
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
u' \<in> unit_disc
v' \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
[PROOF STEP]
by (subst M(2)[symmetric], simp)
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
have "Mv' = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mv' = x
[PROOF STEP]
using \<open>poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'\<close> Mv'
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
moebius_pt M v' = of_complex Mv'

goal (1 subgoal):
 1. Mv' = x
[PROOF STEP]
using \<open>poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
moebius_pt M v' = of_complex Mv'
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'

goal (1 subgoal):
 1. Mv' = x
[PROOF STEP]
using unique_x_axis_poincare_distance_positive[of "poincare_distance u' v'"]
          \<open>poincare_distance u' v' > 0\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
moebius_pt M v' = of_complex Mv'
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
0 \<le> poincare_distance u' v' \<Longrightarrow> \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = poincare_distance u' v'
0 < poincare_distance u' v'

goal (1 subgoal):
 1. Mv' = x
[PROOF STEP]
using \<open>Re Mv' > 0\<close> \<open>Re Mv' < 1\<close> \<open>is_real Mv'\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
moebius_pt M v' = of_complex Mv'
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
0 \<le> poincare_distance u' v' \<Longrightarrow> \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = poincare_distance u' v'
0 < poincare_distance u' v'
0 < Re Mv'
Re Mv' < 1
is_real Mv'

goal (1 subgoal):
 1. Mv' = x
[PROOF STEP]
using \<open>is_real x\<close> \<open>Re x > 0\<close> \<open>Re x < 1\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
moebius_pt M v' = of_complex Mv'
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
0 \<le> poincare_distance u' v' \<Longrightarrow> \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = poincare_distance u' v'
0 < poincare_distance u' v'
0 < Re Mv'
Re Mv' < 1
is_real Mv'
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. Mv' = x
[PROOF STEP]
unfolding positive_x_axis_def
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M v') = poincare_distance u' v'
moebius_pt M v' = of_complex Mv'
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
0 \<le> poincare_distance u' v' \<Longrightarrow> \<exists>!z. is_real z \<and> 0 \<le> Re z \<and> Re z < 1 \<and> poincare_distance 0\<^sub>h (of_complex z) = poincare_distance u' v'
0 < poincare_distance u' v'
0 < Re Mv'
Re Mv' < 1
is_real Mv'
is_real x
0 < Re x
Re x < 1

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

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>0\<^sub>h \<noteq> of_complex x; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
thus "?P' u' v' 0\<^sub>h (of_complex x)"
[PROOF STATE]
proof (prove)
using this:
Mv' = x

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
using M Mv'
[PROOF STATE]
proof (prove)
using this:
Mv' = x
unit_disc_fix M
moebius_pt M u' = 0\<^sub>h
moebius_pt M v' \<in> positive_x_axis
moebius_pt M v' = of_complex Mv'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u' v'. 0\<^sub>h \<noteq> of_complex x \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x)

goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
show "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> unit_disc &&& v \<in> unit_disc &&& u \<noteq> v
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
fix M u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
assume 1: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
hence 2: "?Mu \<noteq> ?Mv" "?Mu \<in> unit_disc" "?Mv \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. moebius_pt M u \<noteq> moebius_pt M v &&& moebius_pt M u \<in> unit_disc &&& moebius_pt M v \<in> unit_disc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
moebius_pt M u \<noteq> moebius_pt M v
moebius_pt M u \<in> unit_disc
moebius_pt M v \<in> unit_disc

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
assume 3: "?P (moebius_pt M u) (moebius_pt M v)"
[PROOF STATE]
proof (state)
this:
\<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)\<rbrakk> \<Longrightarrow> \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
show "?P u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
fix u' v'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
assume 4: "u' \<in> unit_disc" "v' \<in> unit_disc" "poincare_distance u v = poincare_distance u' v'"
[PROOF STATE]
proof (state)
this:
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
hence "poincare_distance ?Mu ?Mv = poincare_distance u v"
[PROOF STATE]
proof (prove)
using this:
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'

goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
obtain M' where 5: "unit_disc_fix M'" "moebius_pt M' u' = ?Mu" "moebius_pt M' v' = ?Mv"
[PROOF STATE]
proof (prove)
using this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>unit_disc_fix M'; moebius_pt M' u' = moebius_pt M u; moebius_pt M' v' = moebius_pt M v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2 3 4
[PROOF STATE]
proof (prove)
using this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
moebius_pt M u \<noteq> moebius_pt M v
moebius_pt M u \<in> unit_disc
moebius_pt M v \<in> unit_disc
\<forall>u' v'. moebius_pt M u \<noteq> moebius_pt M v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<longrightarrow> (\<exists>Ma. unit_disc_fix Ma \<and> moebius_pt Ma u' = moebius_pt M u \<and> moebius_pt Ma v' = moebius_pt M v)
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>unit_disc_fix M'; moebius_pt M' u' = moebius_pt M u; moebius_pt M' v' = moebius_pt M v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_disc_fix M'
moebius_pt M' u' = moebius_pt M u
moebius_pt M' v' = moebius_pt M v

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
let ?M = "(-M) + M'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
have "unit_disc_fix ?M \<and> moebius_pt ?M u' = u \<and> moebius_pt ?M v' = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unit_disc_fix (- M + M') \<and> moebius_pt (- M + M') u' = u \<and> moebius_pt (- M + M') v' = v
[PROOF STEP]
using 5 \<open>unit_disc_fix M\<close>
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M'
moebius_pt M' u' = moebius_pt M u
moebius_pt M' v' = moebius_pt M v
unit_disc_fix M

goal (1 subgoal):
 1. unit_disc_fix (- M + M') \<and> moebius_pt (- M + M') u' = u \<and> moebius_pt (- M + M') v' = v
[PROOF STEP]
using unit_disc_fix_moebius_comp[of "-M" "M'"]
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M'
moebius_pt M' u' = moebius_pt M u
moebius_pt M' v' = moebius_pt M v
unit_disc_fix M
\<lbrakk>unit_disc_fix (- M); unit_disc_fix M'\<rbrakk> \<Longrightarrow> unit_disc_fix (moebius_comp (- M) M')

goal (1 subgoal):
 1. unit_disc_fix (- M + M') \<and> moebius_pt (- M + M') u' = u \<and> moebius_pt (- M + M') v' = v
[PROOF STEP]
using unit_disc_fix_moebius_inv[of M]
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M'
moebius_pt M' u' = moebius_pt M u
moebius_pt M' v' = moebius_pt M v
unit_disc_fix M
\<lbrakk>unit_disc_fix (- M); unit_disc_fix M'\<rbrakk> \<Longrightarrow> unit_disc_fix (moebius_comp (- M) M')
unit_disc_fix M \<Longrightarrow> unit_disc_fix (moebius_inv M)

goal (1 subgoal):
 1. unit_disc_fix (- M + M') \<and> moebius_pt (- M + M') u' = u \<and> moebius_pt (- M + M') v' = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unit_disc_fix (- M + M') \<and> moebius_pt (- M + M') u' = u \<and> moebius_pt (- M + M') v' = v

goal (1 subgoal):
 1. \<And>u' v'. \<lbrakk>u \<noteq> v; u' \<in> unit_disc; v' \<in> unit_disc; poincare_distance u v = poincare_distance u' v'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
thus "\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v"
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix (- M + M') \<and> moebius_pt (- M + M') u' = u \<and> moebius_pt (- M + M') v' = v

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
[PROOF STEP]
obtain M where "unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v"
[PROOF STATE]
proof (prove)
using this:
\<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)

goal (1 subgoal):
 1. (\<And>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>u' v'. u \<noteq> v \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> poincare_distance u v = poincare_distance u' v' \<longrightarrow> (\<exists>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v)
u \<in> unit_disc
v \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
u \<noteq> v

goal (1 subgoal):
 1. (\<And>M. unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
hence "unit_disc_fix (-M) \<and> moebius_pt (-M) u = u' \<and> moebius_pt (-M) v = v'"
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v

goal (1 subgoal):
 1. unit_disc_fix (- M) \<and> moebius_pt (- M) u = u' \<and> moebius_pt (- M) v = v'
[PROOF STEP]
using unit_disc_fix_moebius_inv[of M]
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M \<and> moebius_pt M u' = u \<and> moebius_pt M v' = v
unit_disc_fix M \<Longrightarrow> unit_disc_fix (moebius_inv M)

goal (1 subgoal):
 1. unit_disc_fix (- M) \<and> moebius_pt (- M) u = u' \<and> moebius_pt (- M) v = v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_disc_fix (- M) \<and> moebius_pt (- M) u = u' \<and> moebius_pt (- M) v = v'

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix (- M) \<and> moebius_pt (- M) u = u' \<and> moebius_pt (- M) v = v'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M v = v'

goal:
No subgoals!
[PROOF STEP]
qed