[STATEMENT]
lemma unit_disc_fix_f_congruent_triangles:
  assumes
    in_disc: "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc" and
    in_disc': "u' \<in> unit_disc" "v' \<in> unit_disc" "w' \<in> unit_disc" and
    d: "poincare_distance u v = poincare_distance u' v'"
       "poincare_distance v w = poincare_distance v' w'"
       "poincare_distance u w = poincare_distance u' w'"
  shows
    "\<exists> M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
proof (cases "u = v \<or> u = w \<or> v = w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<or> u = w \<or> v = w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
 2. \<not> (u = v \<or> u = w \<or> v = w) \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = v \<or> u = w \<or> v = w

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

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u = v \<or> u = w \<or> v = w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
using poincare_distance_eq_0_iff[of u' v']
[PROOF STATE]
proof (prove)
using this:
u = v \<or> u = w \<or> v = w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'
\<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_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
using poincare_distance_eq_0_iff[of v' w']
[PROOF STATE]
proof (prove)
using this:
u = v \<or> u = w \<or> v = w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'
\<lbrakk>u' \<in> unit_disc; v' \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance u' v' = 0) = (u' = v')
\<lbrakk>v' \<in> unit_disc; w' \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance v' w' = 0) = (v' = w')

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

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

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

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
using poincare_distance_eq_ex_moebius[of u v u' v']
[PROOF STATE]
proof (prove)
using this:
u = v \<or> u = w \<or> v = w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'
\<lbrakk>u' \<in> unit_disc; v' \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance u' v' = 0) = (u' = v')
\<lbrakk>v' \<in> unit_disc; w' \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance v' w' = 0) = (v' = w')
\<lbrakk>u' \<in> unit_disc; w' \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance u' w' = 0) = (u' = w')
\<lbrakk>v \<in> unit_disc; w \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; poincare_distance v w = poincare_distance v' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M v = v' \<and> moebius_pt M w = w'
\<lbrakk>u \<in> unit_disc; w \<in> unit_disc; u' \<in> unit_disc; w' \<in> unit_disc; poincare_distance u w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u = u' \<and> moebius_pt M w = w'
\<lbrakk>u \<in> unit_disc; v \<in> unit_disc; 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'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
by (metis unit_disc_fix_f_def)
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'

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

goal (1 subgoal):
 1. \<not> (u = v \<or> u = w \<or> v = w) \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
have "\<forall> w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and>
    poincare_distance u v = poincare_distance u' v' \<and>
    poincare_distance v w = poincare_distance v' w' \<and>
    poincare_distance u w = poincare_distance u' w' \<longrightarrow>
    (\<exists> M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')" (is "?P u v")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> 0\<^sub>h \<and> w \<noteq> of_complex x \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<and> poincare_distance (of_complex x) w = poincare_distance v' w' \<and> poincare_distance 0\<^sub>h w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w')
[PROOF STEP]
show "v \<in> unit_disc" "u \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> unit_disc &&& u \<in> unit_disc
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
v \<in> unit_disc
u \<in> unit_disc

goal (3 subgoals):
 1. u \<noteq> v
 2. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
 3. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> 0\<^sub>h \<and> w \<noteq> of_complex x \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<and> poincare_distance (of_complex x) w = poincare_distance v' w' \<and> poincare_distance 0\<^sub>h w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. u \<noteq> v
 2. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
 3. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> 0\<^sub>h \<and> w \<noteq> of_complex x \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<and> poincare_distance (of_complex x) w = poincare_distance v' w' \<and> poincare_distance 0\<^sub>h w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w')
[PROOF STEP]
show "u \<noteq> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> v
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (u = v \<or> u = w \<or> v = w)

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

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> 0\<^sub>h \<and> w \<noteq> of_complex x \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<and> poincare_distance (of_complex x) w = poincare_distance v' w' \<and> poincare_distance 0\<^sub>h w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> 0\<^sub>h \<and> w \<noteq> of_complex x \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<and> poincare_distance (of_complex x) w = poincare_distance v' w' \<and> poincare_distance 0\<^sub>h w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w')
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> 0\<^sub>h \<and> w \<noteq> of_complex x \<and> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v' \<and> poincare_distance (of_complex x) w = poincare_distance v' w' \<and> poincare_distance 0\<^sub>h w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w')
[PROOF STEP]
assume x: "is_real x" "0 < Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 < Re x
Re x < 1

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

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h
[PROOF STEP]
using of_complex_zero_iff[of x]
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1
(of_complex x = 0\<^sub>h) = (x = 0)

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h
[PROOF STEP]
by (auto simp add: complex.expand)
[PROOF STATE]
proof (state)
this:
of_complex x \<noteq> 0\<^sub>h

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

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

goal (1 subgoal):
 1. \<And>w u' v' w'. \<lbrakk>w \<in> unit_disc; u' \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; w \<noteq> 0\<^sub>h; w \<noteq> of_complex x; poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'; poincare_distance (of_complex x) w = poincare_distance v' w'; poincare_distance 0\<^sub>h w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poincare_distance 0\<^sub>h (of_complex x) = 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' = (of_complex x)"
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (of_complex x) = 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' = of_complex x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using poincare_distance_eq_ex_moebius[of u' v' "0\<^sub>h" "of_complex x"] in_disc x
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance u' v'
\<lbrakk>u' \<in> unit_disc; v' \<in> unit_disc; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; poincare_distance u' v' = poincare_distance 0\<^sub>h (of_complex x)\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> moebius_pt M u' = 0\<^sub>h \<and> moebius_pt M v' = of_complex x
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
is_real x
0 < Re x
Re x < 1

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. 0 < poincare_distance 0\<^sub>h w &&& 0 < poincare_distance (of_complex x) w
[PROOF STEP]
by (simp_all add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
0 < poincare_distance 0\<^sub>h w
0 < poincare_distance (of_complex x) w

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

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

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

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

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

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (moebius_pt M' w') = poincare_distance 0\<^sub>h w &&& poincare_distance (of_complex x) (moebius_pt M' w') = poincare_distance (of_complex x) w
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (moebius_pt M' w') = poincare_distance 0\<^sub>h w
poincare_distance (of_complex x) (moebius_pt M' w') = poincare_distance (of_complex x) w

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

goal (1 subgoal):
 1. moebius_pt M' w' \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w) &&& w \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
[PROOF STEP]
using \<open>?w \<in> unit_disc\<close> \<open>w \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M' w') = poincare_distance 0\<^sub>h w
poincare_distance (of_complex x) (moebius_pt M' w') = poincare_distance (of_complex x) w
moebius_pt M' w' \<in> unit_disc
w \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt M' w' \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w) &&& w \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
[PROOF STEP]
unfolding poincare_circle_def
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (moebius_pt M' w') = poincare_distance 0\<^sub>h w
poincare_distance (of_complex x) (moebius_pt M' w') = poincare_distance (of_complex x) w
moebius_pt M' w' \<in> unit_disc
w \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt M' w' \<in> {z' \<in> unit_disc. poincare_distance 0\<^sub>h z' = poincare_distance 0\<^sub>h w} \<inter> {z' \<in> unit_disc. poincare_distance (of_complex x) z' = poincare_distance (of_complex x) w} &&& w \<in> {z' \<in> unit_disc. poincare_distance 0\<^sub>h z' = poincare_distance 0\<^sub>h w} \<inter> {z' \<in> unit_disc. poincare_distance (of_complex x) z' = poincare_distance (of_complex x) w}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
moebius_pt M' w' \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
w \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)

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

goal (1 subgoal):
 1. moebius_pt M' w' = w \<or> moebius_pt M' w' = conjugate w
[PROOF STEP]
using intersect_poincare_circles_x_axis[of 0 x "poincare_distance 0\<^sub>h w" "poincare_distance (of_complex x) w" ?w w] x
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
w \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
\<lbrakk>is_real 0; is_real x; 0 < poincare_distance 0\<^sub>h w; 0 < poincare_distance (of_complex x) w; - 1 < Re 0; Re 0 < 1; - 1 < Re x; Re x < 1; 0 \<noteq> x; moebius_pt M' w' \<in> poincare_circle (of_complex 0) (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w); w \<in> poincare_circle (of_complex 0) (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w); moebius_pt M' w' \<noteq> w\<rbrakk> \<Longrightarrow> moebius_pt M' w' = conjugate w
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. moebius_pt M' w' = w \<or> moebius_pt M' w' = conjugate w
[PROOF STEP]
using \<open>of_complex x \<noteq> 0\<^sub>h\<close> dist_gt_0
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
w \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
\<lbrakk>is_real 0; is_real x; 0 < poincare_distance 0\<^sub>h w; 0 < poincare_distance (of_complex x) w; - 1 < Re 0; Re 0 < 1; - 1 < Re x; Re x < 1; 0 \<noteq> x; moebius_pt M' w' \<in> poincare_circle (of_complex 0) (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w); w \<in> poincare_circle (of_complex 0) (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w); moebius_pt M' w' \<noteq> w\<rbrakk> \<Longrightarrow> moebius_pt M' w' = conjugate w
is_real x
0 < Re x
Re x < 1
of_complex x \<noteq> 0\<^sub>h
0 < poincare_distance 0\<^sub>h w
0 < poincare_distance (of_complex x) w

goal (1 subgoal):
 1. moebius_pt M' w' = w \<or> moebius_pt M' w' = conjugate w
[PROOF STEP]
using poincare_distance_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
w \<in> poincare_circle 0\<^sub>h (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w)
\<lbrakk>is_real 0; is_real x; 0 < poincare_distance 0\<^sub>h w; 0 < poincare_distance (of_complex x) w; - 1 < Re 0; Re 0 < 1; - 1 < Re x; Re x < 1; 0 \<noteq> x; moebius_pt M' w' \<in> poincare_circle (of_complex 0) (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w); w \<in> poincare_circle (of_complex 0) (poincare_distance 0\<^sub>h w) \<inter> poincare_circle (of_complex x) (poincare_distance (of_complex x) w); moebius_pt M' w' \<noteq> w\<rbrakk> \<Longrightarrow> moebius_pt M' w' = conjugate w
is_real x
0 < Re x
Re x < 1
of_complex x \<noteq> 0\<^sub>h
0 < poincare_distance 0\<^sub>h w
0 < poincare_distance (of_complex x) w
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> (poincare_distance ?u ?v = 0) = (?u = ?v)

goal (1 subgoal):
 1. moebius_pt M' w' = w \<or> moebius_pt M' w' = conjugate w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
moebius_pt M' w' = w \<or> moebius_pt M' w' = conjugate w

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

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. moebius_pt M' w' = w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
 2. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
assume "moebius_pt M' w' = w"
[PROOF STATE]
proof (state)
this:
moebius_pt M' w' = w

goal (2 subgoals):
 1. moebius_pt M' w' = w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
 2. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' = w

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

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
using moebius_pt_invert[of M' u' "0\<^sub>h"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' = w
unit_disc_fix M'
moebius_pt M' u' = 0\<^sub>h
moebius_pt M' v' = of_complex x
moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
using moebius_pt_invert[of M' v' "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' = w
unit_disc_fix M'
moebius_pt M' u' = 0\<^sub>h
moebius_pt M' v' = of_complex x
moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'
moebius_pt M' v' = of_complex x \<Longrightarrow> moebius_pt (moebius_inv M') (of_complex x) = v'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
using moebius_pt_invert[of M' w' "w"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' = w
unit_disc_fix M'
moebius_pt M' u' = 0\<^sub>h
moebius_pt M' v' = of_complex x
moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'
moebius_pt M' v' = of_complex x \<Longrightarrow> moebius_pt (moebius_inv M') (of_complex x) = v'
moebius_pt M' w' = w \<Longrightarrow> moebius_pt (moebius_inv M') w = w'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
apply (rule_tac x="moebius_pt (-M')" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>moebius_pt M' w' = w; unit_disc_fix M'; moebius_pt M' u' = 0\<^sub>h; moebius_pt M' v' = of_complex x; moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'; moebius_pt M' v' = of_complex x \<Longrightarrow> moebius_pt (moebius_inv M') (of_complex x) = v'; moebius_pt M' w' = w \<Longrightarrow> moebius_pt (moebius_inv M') w = w'\<rbrakk> \<Longrightarrow> unit_disc_fix_f (moebius_pt (- M')) \<and> moebius_pt (- M') 0\<^sub>h = u' \<and> moebius_pt (- M') (of_complex x) = v' \<and> moebius_pt (- M') w = w'
[PROOF STEP]
apply (simp add: unit_disc_fix_f_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>moebius_pt M' w' = w; unit_disc_fix M'; moebius_pt M' u' = 0\<^sub>h; moebius_pt M' v' = of_complex x; moebius_pt (moebius_inv M') 0\<^sub>h = u'; moebius_pt (moebius_inv M') (of_complex x) = v'; moebius_pt (moebius_inv M') w = w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix M \<and> (moebius_pt (moebius_inv M') = moebius_pt M \<or> moebius_pt (moebius_inv M') = moebius_pt M \<circ> conjugate)
[PROOF STEP]
apply (rule_tac x="-M'" in exI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
let ?M = "moebius_pt (-M') \<circ> conjugate"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
assume "moebius_pt M' w' = conjugate w"
[PROOF STATE]
proof (state)
this:
moebius_pt M' w' = conjugate w

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
hence "?M w = w'"
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' = conjugate w

goal (1 subgoal):
 1. (moebius_pt (- M') \<circ> conjugate) w = w'
[PROOF STEP]
using moebius_pt_invert[of  M' w' "conjugate w"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' w' = conjugate w
moebius_pt M' w' = conjugate w \<Longrightarrow> moebius_pt (moebius_inv M') (conjugate w) = w'

goal (1 subgoal):
 1. (moebius_pt (- M') \<circ> conjugate) w = w'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(moebius_pt (- M') \<circ> conjugate) w = w'

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(moebius_pt (- M') \<circ> conjugate) w = w'

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
have "?M 0\<^sub>h = u'" "?M (of_complex x) = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u' &&& (moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'
[PROOF STEP]
using moebius_pt_invert[of M' u' "0\<^sub>h"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'

goal (1 subgoal):
 1. (moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u' &&& (moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'
[PROOF STEP]
using moebius_pt_invert[of M' v' "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'
moebius_pt M' v' = of_complex x \<Longrightarrow> moebius_pt (moebius_inv M') (of_complex x) = v'

goal (1 subgoal):
 1. (moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u' &&& (moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'
[PROOF STEP]
using M' \<open>is_real x\<close> eq_cnj_iff_real[of x]
[PROOF STATE]
proof (prove)
using this:
moebius_pt M' u' = 0\<^sub>h \<Longrightarrow> moebius_pt (moebius_inv M') 0\<^sub>h = u'
moebius_pt M' v' = of_complex x \<Longrightarrow> moebius_pt (moebius_inv M') (of_complex x) = v'
unit_disc_fix M'
moebius_pt M' u' = 0\<^sub>h
moebius_pt M' v' = of_complex x
is_real x
(cnj x = x) = is_real x

goal (1 subgoal):
 1. (moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u' &&& (moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
(moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u'
(moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u'
(moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
have "unit_disc_fix_f ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unit_disc_fix_f (moebius_pt (- M') \<circ> conjugate)
[PROOF STEP]
using \<open>unit_disc_fix M'\<close>
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M'

goal (1 subgoal):
 1. unit_disc_fix_f (moebius_pt (- M') \<circ> conjugate)
[PROOF STEP]
unfolding unit_disc_fix_f_def
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M'

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix M \<and> (moebius_pt (- M') \<circ> conjugate = moebius_pt M \<or> moebius_pt (- M') \<circ> conjugate = moebius_pt M \<circ> conjugate)
[PROOF STEP]
by (rule_tac x="-M'" in exI, simp)
[PROOF STATE]
proof (state)
this:
unit_disc_fix_f (moebius_pt (- M') \<circ> conjugate)

goal (1 subgoal):
 1. moebius_pt M' w' = conjugate w \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(moebius_pt (- M') \<circ> conjugate) w = w'
(moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u'
(moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'
unit_disc_fix_f (moebius_pt (- M') \<circ> conjugate)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(moebius_pt (- M') \<circ> conjugate) w = w'
(moebius_pt (- M') \<circ> conjugate) 0\<^sub>h = u'
(moebius_pt (- M') \<circ> conjugate) (of_complex x) = v'
unit_disc_fix_f (moebius_pt (- M') \<circ> conjugate)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix_f M \<and> M 0\<^sub>h = u' \<and> M (of_complex x) = v' \<and> M w = w'

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

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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[PROOF STEP]
assume 1: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[PROOF STEP]
assume 2: "?P ?Mu ?Mv"
[PROOF STATE]
proof (state)
this:
\<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')

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>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> moebius_pt M u \<and> w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u' v' \<and> poincare_distance (moebius_pt M v) w = poincare_distance v' w' \<and> poincare_distance (moebius_pt M u) w = poincare_distance u' w' \<longrightarrow> (\<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = u' \<and> Ma (moebius_pt M v) = v' \<and> Ma w = w')\<rbrakk> \<Longrightarrow> \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[PROOF STEP]
show "?P u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w u' v' w'. \<lbrakk>w \<in> unit_disc; u' \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; w \<noteq> u; w \<noteq> v; poincare_distance u v = poincare_distance u' v'; poincare_distance v w = poincare_distance v' w'; poincare_distance u w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
fix w u' v' w'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w u' v' w'. \<lbrakk>w \<in> unit_disc; u' \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; w \<noteq> u; w \<noteq> v; poincare_distance u v = poincare_distance u' v'; poincare_distance v w = poincare_distance v' w'; poincare_distance u w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
let ?Mw = "moebius_pt M w" and ?Mu' = "moebius_pt M u'" and ?Mv' = "moebius_pt M v'" and ?Mw' = "moebius_pt M w'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w u' v' w'. \<lbrakk>w \<in> unit_disc; u' \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; w \<noteq> u; w \<noteq> v; poincare_distance u v = poincare_distance u' v'; poincare_distance v w = poincare_distance v' w'; poincare_distance u w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
assume "w \<in> unit_disc" "u' \<in> unit_disc" "v' \<in> unit_disc" "w' \<in> unit_disc" "w \<noteq> u" "w \<noteq> v"
             "poincare_distance u v = poincare_distance u' v'"
             "poincare_distance v w = poincare_distance v' w'"
             "poincare_distance u w = poincare_distance u' w'"
[PROOF STATE]
proof (state)
this:
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
w \<noteq> u
w \<noteq> v
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'

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

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>unit_disc_fix_f M'; M' (moebius_pt M u) = moebius_pt M u'; M' (moebius_pt M v) = moebius_pt M v'; M' (moebius_pt M w) = moebius_pt M w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1 2[rule_format, of ?Mw ?Mu' ?Mv' ?Mw']
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
w \<noteq> u
w \<noteq> v
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
moebius_pt M w \<in> unit_disc \<and> moebius_pt M u' \<in> unit_disc \<and> moebius_pt M v' \<in> unit_disc \<and> moebius_pt M w' \<in> unit_disc \<and> moebius_pt M w \<noteq> moebius_pt M u \<and> moebius_pt M w \<noteq> moebius_pt M v \<and> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance (moebius_pt M u') (moebius_pt M v') \<and> poincare_distance (moebius_pt M v) (moebius_pt M w) = poincare_distance (moebius_pt M v') (moebius_pt M w') \<and> poincare_distance (moebius_pt M u) (moebius_pt M w) = poincare_distance (moebius_pt M u') (moebius_pt M w') \<Longrightarrow> \<exists>Ma. unit_disc_fix_f Ma \<and> Ma (moebius_pt M u) = moebius_pt M u' \<and> Ma (moebius_pt M v) = moebius_pt M v' \<and> Ma (moebius_pt M w) = moebius_pt M w'

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

goal (1 subgoal):
 1. \<And>w u' v' w'. \<lbrakk>w \<in> unit_disc; u' \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; w \<noteq> u; w \<noteq> v; poincare_distance u v = poincare_distance u' v'; poincare_distance v w = poincare_distance v' w'; poincare_distance u w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
let ?M = "moebius_pt (-M) \<circ> M' \<circ> moebius_pt M"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w u' v' w'. \<lbrakk>w \<in> unit_disc; u' \<in> unit_disc; v' \<in> unit_disc; w' \<in> unit_disc; w \<noteq> u; w \<noteq> v; poincare_distance u v = poincare_distance u' v'; poincare_distance v w = poincare_distance v' w'; poincare_distance u w = poincare_distance u' w'\<rbrakk> \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
show "\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
proof (rule_tac x="?M" in exI, safe)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. unit_disc_fix_f (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M)
 2. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) u = u'
 3. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) v = v'
 4. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) w = w'
[PROOF STEP]
show "unit_disc_fix_f ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unit_disc_fix_f (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M)
[PROOF STEP]
using M'(1) \<open>unit_disc_fix M\<close>
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix_f M'
unit_disc_fix M

goal (1 subgoal):
 1. unit_disc_fix_f (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M)
[PROOF STEP]
by (subst unit_disc_fix_f_comp, subst unit_disc_fix_f_comp, simp_all)
[PROOF STATE]
proof (state)
this:
unit_disc_fix_f (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M)

goal (3 subgoals):
 1. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) u = u'
 2. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) v = v'
 3. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) w = w'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) u = u'
 2. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) v = v'
 3. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) w = w'
[PROOF STEP]
show "?M u = u'" "?M v = v'" "?M w = w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) u = u' &&& (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) v = v' &&& (moebius_pt (- M) \<circ> M' \<circ> moebius_pt M) w = w'
[PROOF STEP]
using M'
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix_f M'
M' (moebius_pt M u) = moebius_pt M u'
M' (moebius_pt M v) = moebius_pt M v'
M' (moebius_pt M w) = moebius_pt M w'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'

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

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

goal (1 subgoal):
 1. \<not> (u = v \<or> u = w \<or> v = w) \<Longrightarrow> \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')

goal (1 subgoal):
 1. \<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w'
[PROOF STEP]
using assms False
[PROOF STATE]
proof (prove)
using this:
\<forall>w u' v' w'. w \<in> unit_disc \<and> u' \<in> unit_disc \<and> v' \<in> unit_disc \<and> w' \<in> unit_disc \<and> w \<noteq> u \<and> w \<noteq> v \<and> poincare_distance u v = poincare_distance u' v' \<and> poincare_distance v w = poincare_distance v' w' \<and> poincare_distance u w = poincare_distance u' w' \<longrightarrow> (\<exists>M. unit_disc_fix_f M \<and> M u = u' \<and> M v = v' \<and> M w = w')
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
u' \<in> unit_disc
v' \<in> unit_disc
w' \<in> unit_disc
poincare_distance u v = poincare_distance u' v'
poincare_distance v w = poincare_distance v' w'
poincare_distance u w = poincare_distance u' w'
\<not> (u = v \<or> u = w \<or> v = w)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_bset_bempty[simp]: "map_bset f bempty = bempty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_bset f bempty = bempty
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma map_bset_eq_bempty[simp]:
  "map_bset f x = bempty \<longleftrightarrow> x = bempty"
  "bempty = map_bset f x \<longleftrightarrow> x = bempty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_bset f x = bempty) = (x = bempty) &&& (bempty = map_bset f x) = (x = bempty)
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma map_bset_bsingleton[simp]: "map_bset f (bsingleton x) = bsingleton (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_bset f (bsingleton x) = bsingleton (f x)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma map_bset_bdoubleton[simp]: "map_bset f (bdoubleton x y) = bdoubleton (f x) (f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_bset f (bdoubleton x y) = bdoubleton (f x) (f y)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma bdoubleton_same[simp]: "bdoubleton x x = bsingleton x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdoubleton x x = bsingleton x
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma bempty_neq_bsingleton[simp]:
  "bempty \<noteq> bsingleton x"
  "bsingleton x \<noteq> bempty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bempty \<noteq> bsingleton x &&& bsingleton x \<noteq> bempty
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma bempty_neq_bdoubleton[simp]:
  "bempty \<noteq> bdoubleton x y"
  "bdoubleton x y \<noteq> bempty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bempty \<noteq> bdoubleton x y &&& bdoubleton x y \<noteq> bempty
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma bsinleton_eq_bdoubleton[simp]:
  "bsingleton x = bdoubleton y z \<longleftrightarrow> (x = y \<and> y = z)"
  "bdoubleton y z = bsingleton x \<longleftrightarrow> (x = y \<and> y = z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bsingleton x = bdoubleton y z) = (x = y \<and> y = z) &&& (bdoubleton y z = bsingleton x) = (x = y \<and> y = z)
[PROOF STEP]
by (transfer, auto)+


[STATEMENT]
lemma bsinleton_inj[simp]:
  "bsingleton x = bsingleton y \<longleftrightarrow> (x = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bsingleton x = bsingleton y) = (x = y)
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma bdoubleton_eq_iff[simp]:
  "bdoubleton x y = bdoubleton z w \<longleftrightarrow> (x = z \<and> y = w \<or> x = w \<and> y = z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bdoubleton x y = bdoubleton z w) = (x = z \<and> y = w \<or> x = w \<and> y = z)
[PROOF STEP]
by transfer (simp add: doubleton_eq_iff)


[STATEMENT]
lemma bset_cases:
  "\<lbrakk>X = bempty \<Longrightarrow> P; \<And>x. X = bsingleton x \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = bdoubleton x y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X = bempty \<Longrightarrow> P; \<And>x. X = bsingleton x \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = bdoubleton x y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
proof (transfer fixing: P)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
fix Z :: "'a set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
assume "|Z| \<le>o ctwo"
[PROOF STATE]
proof (state)
this:
|Z| \<le>o ctwo

goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
|Z| \<le>o ctwo

goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
|Z| \<le>o ctwo
[PROOF STEP]
have "finite Z"
[PROOF STATE]
proof (prove)
using this:
|Z| \<le>o ctwo

goal (1 subgoal):
 1. finite Z
[PROOF STEP]
by (metis card_of_ordLeq_infinite ctwo_def finite_code)
[PROOF STATE]
proof (state)
this:
finite Z

goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
|Z| \<le>o ctwo
finite Z
[PROOF STEP]
have "card Z \<le> 2"
[PROOF STATE]
proof (prove)
using this:
|Z| \<le>o ctwo
finite Z

goal (1 subgoal):
 1. card Z \<le> 2
[PROOF STEP]
unfolding ctwo_def
[PROOF STATE]
proof (prove)
using this:
|Z| \<le>o |UNIV|
finite Z

goal (1 subgoal):
 1. card Z \<le> 2
[PROOF STEP]
by (subst (asm) finite_card_of_iff_card2) auto
[PROOF STATE]
proof (state)
this:
card Z \<le> 2

goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card Z \<le> 2

goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
assume "Z = {} \<Longrightarrow> P" "\<And>x. Z = {x} \<Longrightarrow> P" "\<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (state)
this:
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. \<And>X. \<lbrakk>|X| \<le>o ctwo; X = {} \<Longrightarrow> P; \<And>x. X = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; X = {x, y}\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card Z \<le> 2
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
show P
[PROOF STATE]
proof (prove)
using this:
card Z \<le> 2
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
using \<open>finite Z\<close>
[PROOF STATE]
proof (prove)
using this:
card Z \<le> 2
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P
finite Z

goal (1 subgoal):
 1. P
[PROOF STEP]
proof (induct "card Z")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>0 = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P
 2. \<And>x. \<lbrakk>\<lbrakk>x = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P; Suc x = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<lbrakk>m = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P
Suc m = card Z
card Z \<le> 2
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P
finite Z

goal (2 subgoals):
 1. \<lbrakk>0 = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P
 2. \<And>x. \<lbrakk>\<lbrakk>x = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P; Suc x = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
from Suc(2)[symmetric] Suc(2-7)
[PROOF STATE]
proof (chain)
picking this:
card Z = Suc m
Suc m = card Z
card Z \<le> 2
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P
finite Z
[PROOF STEP]
show P
[PROOF STATE]
proof (prove)
using this:
card Z = Suc m
Suc m = card Z
card Z \<le> 2
Z = {} \<Longrightarrow> P
Z = {?x} \<Longrightarrow> P
\<lbrakk>?x \<noteq> ?y; Z = {?x, ?y}\<rbrakk> \<Longrightarrow> P
finite Z

goal (1 subgoal):
 1. P
[PROOF STEP]
by (cases m) (auto simp: card_Suc_eq)
[PROOF STATE]
proof (state)
this:
P

goal (1 subgoal):
 1. \<lbrakk>0 = card Z; card Z \<le> 2; Z = {} \<Longrightarrow> P; \<And>x. Z = {x} \<Longrightarrow> P; \<And>x y. \<lbrakk>x \<noteq> y; Z = {x, y}\<rbrakk> \<Longrightarrow> P; finite Z\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
P

goal:
No subgoals!
[PROOF STEP]
qed