[STATEMENT]
lemma unique_midpoint_x_axis:
  assumes x: "is_real x" "-1 < Re x" "Re x < 1" and
          y: "is_real y" "-1 < Re y" "Re y < 1" and
          "x \<noteq> y"
  shows "\<exists>! z. -1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)" (is "\<exists>! z. ?R z (of_complex x) (of_complex y)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
let ?x = "of_complex x" and ?y = "of_complex y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
let ?P = "\<lambda> x y. \<exists>! z. ?R z x y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
have "\<forall> x. -1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> ?y \<longrightarrow> ?P (of_complex x) ?y" (is "?Q (of_complex y)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> of_complex y \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y))
[PROOF STEP]
proof (rule wlog_real_zero)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. of_complex y \<in> unit_disc
 2. is_real (to_complex (of_complex y))
 3. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
 4. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h)
[PROOF STEP]
show "?y \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex y \<in> unit_disc
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
is_real y
- 1 < Re y
Re y < 1

goal (1 subgoal):
 1. of_complex y \<in> unit_disc
[PROOF STEP]
by (simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
of_complex y \<in> unit_disc

goal (3 subgoals):
 1. is_real (to_complex (of_complex y))
 2. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
 3. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_real (to_complex (of_complex y))
 2. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
 3. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h)
[PROOF STEP]
show "is_real (to_complex ?y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (to_complex (of_complex y))
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
is_real y
- 1 < Re y
Re y < 1

goal (1 subgoal):
 1. is_real (to_complex (of_complex y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_real (to_complex (of_complex y))

goal (2 subgoals):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
 2. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
 2. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h)
[PROOF STEP]
show "?Q 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> 0\<^sub>h \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h)
[PROOF STEP]
proof (rule allI, rule impI, (erule conjE)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
assume x: "-1 < Re x" "Re x < 1" "is_real x"
[PROOF STATE]
proof (state)
this:
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
let ?x = "of_complex x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
assume "?x \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (state)
this:
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
hence "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
of_complex x \<noteq> 0\<^sub>h

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
hence "Re x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. Re x \<noteq> 0
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. Re x \<noteq> 0
[PROOF STEP]
using complex_neq_0
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
- 1 < Re x
Re x < 1
is_real x
(?z \<noteq> 0) = (0 < (Re ?z)\<^sup>2 + (Im ?z)\<^sup>2)

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
have *: "\<forall> a. -1 < a \<and> a < 1 \<longrightarrow>
                 (poincare_distance (of_complex (cor a)) ?x = poincare_distance (of_complex (cor a)) 0\<^sub>h \<longleftrightarrow>
                 (Re x) * a * a - 2 * a + Re x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. - 1 < a \<and> a < 1 \<longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
fix a :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
assume "-1 < a \<and> a < 1"
[PROOF STATE]
proof (state)
this:
- 1 < a \<and> a < 1

goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
hence "of_complex (cor a) \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
- 1 < a \<and> a < 1

goal (1 subgoal):
 1. of_complex (cor a) \<in> unit_disc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_complex (cor a) \<in> unit_disc

goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_complex (cor a) \<in> unit_disc

goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "(a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2) \<longleftrightarrow>
              (Re x) * a * a - 2 * a + Re x = 0" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "1 - a\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - a\<^sup>2 \<noteq> 0
[PROOF STEP]
using \<open>-1 < a \<and> a < 1\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < a \<and> a < 1

goal (1 subgoal):
 1. 1 - a\<^sup>2 \<noteq> 0
[PROOF STEP]
by (metis cancel_comm_monoid_add_class.diff_cancel diff_eq_diff_less less_numeral_extra(4) power2_eq_1_iff right_minus_eq)
[PROOF STATE]
proof (state)
this:
1 - a\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
hence "?lhs \<longleftrightarrow> (a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
1 - a\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2)
[PROOF STEP]
by (smt divide_cancel_right divide_divide_eq_left mult.commute)
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "... \<longleftrightarrow> (a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))
[PROOF STEP]
have "1 - (Re x)\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - (Re x)\<^sup>2 \<noteq> 0
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. 1 - (Re x)\<^sup>2 \<noteq> 0
[PROOF STEP]
by (smt power2_eq_1_iff)
[PROOF STATE]
proof (state)
this:
1 - (Re x)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 - (Re x)\<^sup>2 \<noteq> 0

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))
[PROOF STEP]
by (simp add: divide_eq_eq)
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / (1 - (Re x)\<^sup>2) = a\<^sup>2) = ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2))

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "... \<longleftrightarrow> a\<^sup>2 * (Re x)\<^sup>2 - 2*a*Re x + (Re x)\<^sup>2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2)) = (a\<^sup>2 * (Re x)\<^sup>2 - 2 * a * Re x + (Re x)\<^sup>2 = 0)
[PROOF STEP]
by (simp add: power2_diff field_simps)
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2)) = (a\<^sup>2 * (Re x)\<^sup>2 - 2 * a * Re x + (Re x)\<^sup>2 = 0)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 = a\<^sup>2 * (1 - (Re x)\<^sup>2)) = (a\<^sup>2 * (Re x)\<^sup>2 - 2 * a * Re x + (Re x)\<^sup>2 = 0)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "... \<longleftrightarrow> Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a\<^sup>2 * (Re x)\<^sup>2 - 2 * a * Re x + (Re x)\<^sup>2 = 0) = (Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0)
[PROOF STEP]
by (simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(a\<^sup>2 * (Re x)\<^sup>2 - 2 * a * Re x + (Re x)\<^sup>2 = 0) = (Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a\<^sup>2 * (Re x)\<^sup>2 - 2 * a * Re x + (Re x)\<^sup>2 = 0) = (Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "... \<longleftrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
using \<open>Re x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Re x \<noteq> 0

goal (1 subgoal):
 1. (Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
by (simp add: mult.commute mult.left_commute power2_eq_square)
[PROOF STATE]
proof (state)
this:
(Re x * (a\<^sup>2 * Re x - 2 * a + Re x) = 0) = (Re x * a * a - 2 * a + Re x = 0)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)

goal (1 subgoal):
 1. ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)

goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)

goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
have "arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2)) \<longleftrightarrow> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))
[PROOF STEP]
using \<open>-1 < a \<and> a < 1\<close> x mult_left_cancel[of "2::real" "(a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2))" "a\<^sup>2 / (1 - a\<^sup>2)"]
[PROOF STATE]
proof (prove)
using this:
- 1 < a \<and> a < 1
- 1 < Re x
Re x < 1
is_real x
2 \<noteq> 0 \<Longrightarrow> (2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2))) = 2 * (a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))

goal (1 subgoal):
 1. (arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))
[PROOF STEP]
by (subst arcosh_eq_iff, simp_all add: square_le_1)
[PROOF STATE]
proof (state)
this:
(arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))

goal (1 subgoal):
 1. \<And>a. - 1 < a \<and> a < 1 \<Longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
of_complex (cor a) \<in> unit_disc
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
(arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))
[PROOF STEP]
show "poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h \<longleftrightarrow>
              (Re x) * a * a - 2 * a + Re x = 0"
[PROOF STATE]
proof (prove)
using this:
of_complex (cor a) \<in> unit_disc
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
(arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))

goal (1 subgoal):
 1. (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
of_complex (cor a) \<in> unit_disc
((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2)) = (Re x * a * a - 2 * a + Re x = 0)
(arcosh (1 + 2 * ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)))) = arcosh (1 + 2 * a\<^sup>2 / (1 - a\<^sup>2))) = ((a - Re x)\<^sup>2 / ((1 - a\<^sup>2) * (1 - (Re x)\<^sup>2)) = a\<^sup>2 / (1 - a\<^sup>2))
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)
[PROOF STEP]
by (auto simp add: poincare_distance_formula cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
(poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>a. - 1 < a \<and> a < 1 \<longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> 0\<^sub>h\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
show "?P ?x 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
let ?a = "(1 - sqrt(1 - (Re x)\<^sup>2)) / (Re x)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
let ?b = "(1 + sqrt(1 - (Re x)\<^sup>2)) / (Re x)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
have "is_real ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
have "1 - (Re x)\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (Re x)\<^sup>2
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. 0 < 1 - (Re x)\<^sup>2
[PROOF STEP]
by (smt power2_eq_1_iff square_le_1)
[PROOF STATE]
proof (state)
this:
0 < 1 - (Re x)\<^sup>2

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
have "\<bar>?a\<bar> < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
proof (cases "Re x > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
 2. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < Re x

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
 2. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
have "(1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
[PROOF STEP]
using \<open>Re x > 0\<close> x
[PROOF STATE]
proof (prove)
using this:
0 < Re x
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. (1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
 2. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
hence "1 - Re x < sqrt (1 - (Re x)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
(1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. 1 - Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
using real_less_rsqrt
[PROOF STATE]
proof (prove)
using this:
(1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
?x\<^sup>2 < ?y \<Longrightarrow> ?x < sqrt ?y

goal (1 subgoal):
 1. 1 - Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
1 - Re x < sqrt (1 - (Re x)\<^sup>2)

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
 2. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 - Re x < sqrt (1 - (Re x)\<^sup>2)

goal (1 subgoal):
 1. \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
using \<open>1 - (Re x)\<^sup>2 > 0\<close> \<open>Re x > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 - Re x < sqrt (1 - (Re x)\<^sup>2)
0 < 1 - (Re x)\<^sup>2
0 < Re x

goal (1 subgoal):
 1. \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < Re x

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
hence "Re x < 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Re x

goal (1 subgoal):
 1. Re x < 0
[PROOF STEP]
using \<open>Re x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Re x
Re x \<noteq> 0

goal (1 subgoal):
 1. Re x < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re x < 0

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
have "1 + Re x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 + Re x
[PROOF STEP]
using \<open>Re x > -1\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x

goal (1 subgoal):
 1. 0 < 1 + Re x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < 1 + Re x

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
hence "2*Re x + 2*Re x*Re x < 0"
[PROOF STATE]
proof (prove)
using this:
0 < 1 + Re x

goal (1 subgoal):
 1. 2 * Re x + 2 * Re x * Re x < 0
[PROOF STEP]
using \<open>Re x < 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 + Re x
Re x < 0

goal (1 subgoal):
 1. 2 * Re x + 2 * Re x * Re x < 0
[PROOF STEP]
by (metis comm_semiring_class.distrib mult.commute mult_2_right mult_less_0_iff one_add_one zero_less_double_add_iff_zero_less_single_add)
[PROOF STATE]
proof (state)
this:
2 * Re x + 2 * Re x * Re x < 0

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
hence "(1 + Re x)\<^sup>2 < 1 - (Re x)\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
2 * Re x + 2 * Re x * Re x < 0

goal (1 subgoal):
 1. (1 + Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(1 + Re x)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
hence "1 + Re x < sqrt (1 - (Re x)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
(1 + Re x)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. 1 + Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
using \<open>1 - (Re x)\<^sup>2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
(1 + Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
0 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. 1 + Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
using real_less_rsqrt
[PROOF STATE]
proof (prove)
using this:
(1 + Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
0 < 1 - (Re x)\<^sup>2
?x\<^sup>2 < ?y \<Longrightarrow> ?x < sqrt ?y

goal (1 subgoal):
 1. 1 + Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
1 + Re x < sqrt (1 - (Re x)\<^sup>2)

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 + Re x < sqrt (1 - (Re x)\<^sup>2)

goal (1 subgoal):
 1. \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
using \<open>Re x < 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 + Re x < sqrt (1 - (Re x)\<^sup>2)
Re x < 0

goal (1 subgoal):
 1. \<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
hence "-1 < ?a" "?a < 1"
[PROOF STATE]
proof (prove)
using this:
\<bar>(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar> < 1

goal (1 subgoal):
 1. - 1 < (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x &&& (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x < 1
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
- 1 < (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x < 1

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- 1 < (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x < 1

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
have "(Re x) * ?a * ?a - 2 * ?a + Re x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re x * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) - 2 * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) + Re x = 0
[PROOF STEP]
using \<open>Re x \<noteq> 0\<close> \<open>1 - (Re x)\<^sup>2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Re x \<noteq> 0
0 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. Re x * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) - 2 * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) + Re x = 0
[PROOF STEP]
by (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
Re x * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) - 2 * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) + Re x = 0

goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = ?a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))
- 1 < (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x < 1
Re x * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) - 2 * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) + Re x = 0
[PROOF STEP]
show "-1 < Re (cor ?a) \<and> Re (cor ?a) < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) 0\<^sub>h"
[PROOF STATE]
proof (prove)
using this:
is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))
- 1 < (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x < 1
Re x * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) - 2 * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) + Re x = 0

goal (1 subgoal):
 1. - 1 < Re (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) \<and> Re (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) < 1 \<and> is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) \<and> poincare_distance (of_complex (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))) (of_complex x) = poincare_distance (of_complex (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))) 0\<^sub>h
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))
- 1 < (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(1 - sqrt (1 - (Re x)\<^sup>2)) / Re x < 1
Re x * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) - 2 * ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x) + Re x = 0
\<forall>a. - 1 < a \<and> a < 1 \<longrightarrow> (poincare_distance (of_complex (cor a)) (of_complex x) = poincare_distance (of_complex (cor a)) 0\<^sub>h) = (Re x * a * a - 2 * a + Re x = 0)

goal (1 subgoal):
 1. - 1 < Re (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) \<and> Re (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) < 1 \<and> is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) \<and> poincare_distance (of_complex (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))) (of_complex x) = poincare_distance (of_complex (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))) 0\<^sub>h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- 1 < Re (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) \<and> Re (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) < 1 \<and> is_real (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)) \<and> poincare_distance (of_complex (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))) (of_complex x) = poincare_distance (of_complex (cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x))) 0\<^sub>h

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
assume **: "- 1 < Re z \<and> Re z < 1 \<and> is_real z \<and>
               poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h"
[PROOF STATE]
proof (state)
this:
- 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
hence "Re x * Re z * Re z - 2 * Re z + Re x = 0"
[PROOF STATE]
proof (prove)
using this:
- 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h

goal (1 subgoal):
 1. Re x * Re z * Re z - 2 * Re z + Re x = 0
[PROOF STEP]
using *[rule_format, of "Re z"] x
[PROOF STATE]
proof (prove)
using this:
- 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
- 1 < Re z \<and> Re z < 1 \<Longrightarrow> (poincare_distance (of_complex (cor (Re z))) (of_complex x) = poincare_distance (of_complex (cor (Re z))) 0\<^sub>h) = (Re x * Re z * Re z - 2 * Re z + Re x = 0)
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. Re x * Re z * Re z - 2 * Re z + Re x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re x * Re z * Re z - 2 * Re z + Re x = 0

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Re x * Re z * Re z - 2 * Re z + Re x = 0

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
have "sqrt (4 - 4 * Re x * Re x) = 2 * sqrt(1 - Re x * Re x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
[PROOF STEP]
have "sqrt (4 - 4 * Re x * Re x) = sqrt(4 * (1 - Re x * Re x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (4 - 4 * Re x * Re x) = sqrt (4 * (1 - Re x * Re x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt (4 - 4 * Re x * Re x) = sqrt (4 * (1 - Re x * Re x))

goal (1 subgoal):
 1. sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sqrt (4 - 4 * Re x * Re x) = sqrt (4 * (1 - Re x * Re x))

goal (1 subgoal):
 1. sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
[PROOF STEP]
by (simp only: real_sqrt_mult, simp)
[PROOF STATE]
proof (state)
this:
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
have "(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
have "(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) =
               (2 * (1 - sqrt (1 - Re x * Re x))) / (2 * Re x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = 2 * (1 - sqrt (1 - Re x * Re x)) / (2 * Re x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = 2 * (1 - sqrt (1 - Re x * Re x)) / (2 * Re x)

goal (1 subgoal):
 1. (2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = 2 * (1 - sqrt (1 - Re x * Re x)) / (2 * Re x)

goal (1 subgoal):
 1. (2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
by (subst (asm) mult_divide_mult_cancel_left) (auto simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
have "(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = ?b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
have "(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) =
               (2 * (1 + sqrt (1 - Re x * Re x))) / (2 * Re x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = 2 * (1 + sqrt (1 - Re x * Re x)) / (2 * Re x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = 2 * (1 + sqrt (1 - Re x * Re x)) / (2 * Re x)

goal (1 subgoal):
 1. (2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = 2 * (1 + sqrt (1 - Re x * Re x)) / (2 * Re x)

goal (1 subgoal):
 1. (2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
by (subst (asm) mult_divide_mult_cancel_left) (auto simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Re x * Re z * Re z - 2 * Re z + Re x = 0
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
have "Re z = ?a \<or> Re z = ?b"
[PROOF STATE]
proof (prove)
using this:
Re x * Re z * Re z - 2 * Re z + Re x = 0
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x \<or> Re z = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
using discriminant_nonneg[of "Re x" "-2" "Re x" "Re z"] discrim_def[of "Re x" "-2" "Re x"]
[PROOF STATE]
proof (prove)
using this:
Re x * Re z * Re z - 2 * Re z + Re x = 0
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
\<lbrakk>Re x \<noteq> 0; 0 \<le> discrim (Re x) (- 2) (Re x)\<rbrakk> \<Longrightarrow> (Re x * (Re z)\<^sup>2 + - 2 * Re z + Re x = 0) = (Re z = (- (- 2) + sqrt (discrim (Re x) (- 2) (Re x))) / (2 * Re x) \<or> Re z = (- (- 2) - sqrt (discrim (Re x) (- 2) (Re x))) / (2 * Re x))
discrim (Re x) (- 2) (Re x) \<equiv> (- 2)\<^sup>2 - 4 * Re x * Re x

goal (1 subgoal):
 1. Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x \<or> Re z = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
using \<open>Re x \<noteq> 0\<close> \<open>-1 < Re x\<close> \<open>Re x < 1\<close> \<open>1 - (Re x)\<^sup>2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Re x * Re z * Re z - 2 * Re z + Re x = 0
sqrt (4 - 4 * Re x * Re x) = 2 * sqrt (1 - Re x * Re x)
(2 - 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
(2 + 2 * sqrt (1 - Re x * Re x)) / (2 * Re x) = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
\<lbrakk>Re x \<noteq> 0; 0 \<le> discrim (Re x) (- 2) (Re x)\<rbrakk> \<Longrightarrow> (Re x * (Re z)\<^sup>2 + - 2 * Re z + Re x = 0) = (Re z = (- (- 2) + sqrt (discrim (Re x) (- 2) (Re x))) / (2 * Re x) \<or> Re z = (- (- 2) - sqrt (discrim (Re x) (- 2) (Re x))) / (2 * Re x))
discrim (Re x) (- 2) (Re x) \<equiv> (- 2)\<^sup>2 - 4 * Re x * Re x
Re x \<noteq> 0
- 1 < Re x
Re x < 1
0 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x \<or> Re z = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
by (auto simp add:power2_eq_square)
[PROOF STATE]
proof (state)
this:
Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x \<or> Re z = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
have "\<bar>?b\<bar> > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
proof (cases "Re x > 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
 2. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < Re x

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
 2. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
have "(Re x - 1)\<^sup>2 < 1 - (Re x)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re x - 1)\<^sup>2 < 1 - (Re x)\<^sup>2
[PROOF STEP]
using \<open>Re x > 0\<close> x
[PROOF STATE]
proof (prove)
using this:
0 < Re x
- 1 < Re x
Re x < 1
is_real x

goal (1 subgoal):
 1. (Re x - 1)\<^sup>2 < 1 - (Re x)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(Re x - 1)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
 2. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
hence "Re x - 1 < sqrt (1 - (Re x)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
(Re x - 1)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. Re x - 1 < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
using real_less_rsqrt
[PROOF STATE]
proof (prove)
using this:
(Re x - 1)\<^sup>2 < 1 - (Re x)\<^sup>2
?x\<^sup>2 < ?y \<Longrightarrow> ?x < sqrt ?y

goal (1 subgoal):
 1. Re x - 1 < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re x - 1 < sqrt (1 - (Re x)\<^sup>2)

goal (2 subgoals):
 1. 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
 2. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Re x - 1 < sqrt (1 - (Re x)\<^sup>2)

goal (1 subgoal):
 1. 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
using \<open>1 - (Re x)\<^sup>2 > 0\<close> \<open>Re x > 0\<close>
[PROOF STATE]
proof (prove)
using this:
Re x - 1 < sqrt (1 - (Re x)\<^sup>2)
0 < 1 - (Re x)\<^sup>2
0 < Re x

goal (1 subgoal):
 1. 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < Re x

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
hence "Re x < 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Re x

goal (1 subgoal):
 1. Re x < 0
[PROOF STEP]
using \<open>Re x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Re x
Re x \<noteq> 0

goal (1 subgoal):
 1. Re x < 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re x < 0

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
have "1 + Re x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 + Re x
[PROOF STEP]
using \<open>Re x > -1\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x

goal (1 subgoal):
 1. 0 < 1 + Re x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < 1 + Re x

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
hence "2*Re x + 2*Re x*Re x < 0"
[PROOF STATE]
proof (prove)
using this:
0 < 1 + Re x

goal (1 subgoal):
 1. 2 * Re x + 2 * Re x * Re x < 0
[PROOF STEP]
using \<open>Re x < 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 + Re x
Re x < 0

goal (1 subgoal):
 1. 2 * Re x + 2 * Re x * Re x < 0
[PROOF STEP]
by (metis comm_semiring_class.distrib mult.commute mult_2_right mult_less_0_iff one_add_one zero_less_double_add_iff_zero_less_single_add)
[PROOF STATE]
proof (state)
this:
2 * Re x + 2 * Re x * Re x < 0

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
hence "1 - (Re x)\<^sup>2 > (- 1 - (Re x))\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
2 * Re x + 2 * Re x * Re x < 0

goal (1 subgoal):
 1. (- 1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
[PROOF STEP]
by (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
(- 1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
hence "sqrt (1 - (Re x)\<^sup>2) > -1 - Re x"
[PROOF STATE]
proof (prove)
using this:
(- 1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2

goal (1 subgoal):
 1. - 1 - Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
using real_less_rsqrt
[PROOF STATE]
proof (prove)
using this:
(- 1 - Re x)\<^sup>2 < 1 - (Re x)\<^sup>2
?x\<^sup>2 < ?y \<Longrightarrow> ?x < sqrt ?y

goal (1 subgoal):
 1. - 1 - Re x < sqrt (1 - (Re x)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- 1 - Re x < sqrt (1 - (Re x)\<^sup>2)

goal (1 subgoal):
 1. \<not> 0 < Re x \<Longrightarrow> 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- 1 - Re x < sqrt (1 - (Re x)\<^sup>2)

goal (1 subgoal):
 1. 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
using \<open>Re x < 0\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 - Re x < sqrt (1 - (Re x)\<^sup>2)
Re x < 0

goal (1 subgoal):
 1. 1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
hence "?b < -1 \<or> ?b > 1"
[PROOF STATE]
proof (prove)
using this:
1 < \<bar>(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x\<bar>

goal (1 subgoal):
 1. (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x < - 1 \<or> 1 < (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x < - 1 \<or> 1 < (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
hence "Re z = ?a"
[PROOF STATE]
proof (prove)
using this:
(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x < - 1 \<or> 1 < (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
using \<open>Re z = ?a \<or> Re z = ?b\<close> **
[PROOF STATE]
proof (prove)
using this:
(1 + sqrt (1 - (Re x)\<^sup>2)) / Re x < - 1 \<or> 1 < (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x \<or> Re z = (1 + sqrt (1 - (Re x)\<^sup>2)) / Re x
- 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h

goal (1 subgoal):
 1. Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h \<Longrightarrow> z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
thus "z = ?a"
[PROOF STATE]
proof (prove)
using this:
Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x

goal (1 subgoal):
 1. z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
using ** complex_of_real_Re
[PROOF STATE]
proof (prove)
using this:
Re z = (1 - sqrt (1 - (Re x)\<^sup>2)) / Re x
- 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) 0\<^sub>h
is_real ?k \<Longrightarrow> cor (Re ?k) = ?k

goal (1 subgoal):
 1. z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
z = cor ((1 - sqrt (1 - (Re x)\<^sup>2)) / Re x)

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

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

goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
fix a u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
let ?M = "moebius_pt (blaschke a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
let ?Mu = "?M u"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
assume "u \<in> unit_disc" "is_real a" "cmod a < 1"
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
is_real a
cmod a < 1

goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
assume *: "?Q ?Mu"
[PROOF STATE]
proof (state)
this:
\<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))

goal (1 subgoal):
 1. \<And>a u. \<lbrakk>u \<in> unit_disc; is_real a; cmod a < 1; \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> moebius_pt (blaschke a) u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u))\<rbrakk> \<Longrightarrow> \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
show "?Q u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)
[PROOF STEP]
proof (rule allI, rule impI, (erule conjE)+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
assume x: "-1 < Re x" "Re x < 1" "is_real x" "of_complex x \<noteq> u"
[PROOF STATE]
proof (state)
this:
- 1 < Re x
Re x < 1
is_real x
of_complex x \<noteq> u

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
let ?Mx = "?M (of_complex x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have "of_complex x \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> unit_disc
[PROOF STEP]
using x cmod_eq_Re
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x
Re x < 1
is_real x
of_complex x \<noteq> u
is_real ?z \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>

goal (1 subgoal):
 1. of_complex x \<in> unit_disc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_complex x \<in> unit_disc

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
hence "?Mx \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<in> unit_disc
[PROOF STEP]
using \<open>is_real a\<close> \<open>cmod a < 1\<close> blaschke_unit_disc_fix[of a]
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
is_real a
cmod a < 1
cmod a < 1 \<Longrightarrow> unit_disc_fix (blaschke a)

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<in> unit_disc
[PROOF STEP]
using unit_disc_fix_discI
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
is_real a
cmod a < 1
cmod a < 1 \<Longrightarrow> unit_disc_fix (blaschke a)
\<lbrakk>unit_disc_fix ?M; ?u \<in> unit_disc\<rbrakk> \<Longrightarrow> moebius_pt ?M ?u \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<in> unit_disc
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex x) \<in> unit_disc

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
hence "?Mx \<noteq> \<infinity>\<^sub>h"
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex x) \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have "of_complex x \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> circline_set x_axis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x
Re x < 1
is_real x
of_complex x \<noteq> u

goal (1 subgoal):
 1. of_complex x \<in> circline_set x_axis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_complex x \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
hence "?Mx \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> circline_set x_axis

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<in> circline_set x_axis
[PROOF STEP]
using blaschke_real_preserve_x_axis[OF \<open>is_real a\<close> \<open>cmod a < 1\<close>, of "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> circline_set x_axis
(moebius_pt (blaschke a) (of_complex x) \<in> circline_set x_axis) = (of_complex x \<in> circline_set x_axis)

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<in> circline_set x_axis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex x) \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
hence "-1 < Re (to_complex ?Mx) \<and> Re (to_complex ?Mx) < 1 \<and> is_real (to_complex ?Mx)"
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex x) \<in> circline_set x_axis

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))
[PROOF STEP]
using \<open>?Mx \<noteq> \<infinity>\<^sub>h\<close> \<open>?Mx \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex x) \<in> circline_set x_axis
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h
moebius_pt (blaschke a) (of_complex x) \<in> unit_disc

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex x) \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h
moebius_pt (blaschke a) (of_complex x) \<in> unit_disc

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have "?Mx \<noteq> ?Mu"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<noteq> moebius_pt (blaschke a) u
[PROOF STEP]
using \<open>of_complex x \<noteq> u\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex x \<noteq> u

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex x) \<noteq> moebius_pt (blaschke a) u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex x) \<noteq> moebius_pt (blaschke a) u

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))
moebius_pt (blaschke a) (of_complex x) \<noteq> moebius_pt (blaschke a) u
[PROOF STEP]
have "?P ?Mx ?Mu"
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))
moebius_pt (blaschke a) (of_complex x) \<noteq> moebius_pt (blaschke a) u

goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)
[PROOF STEP]
using *[rule_format, of "to_complex ?Mx"] \<open>?Mx \<noteq> \<infinity>\<^sub>h\<close>
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x)))
moebius_pt (blaschke a) (of_complex x) \<noteq> moebius_pt (blaschke a) u
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex x))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex x))) \<and> of_complex (to_complex (moebius_pt (blaschke a) (of_complex x))) \<noteq> moebius_pt (blaschke a) u \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex (to_complex (moebius_pt (blaschke a) (of_complex x)))) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)
moebius_pt (blaschke a) (of_complex x) \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)
[PROOF STEP]
obtain Mz where
        "?R Mz ?Mx ?Mu"
[PROOF STATE]
proof (prove)
using this:
\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. (\<And>Mz. - 1 < Re Mz \<and> Re Mz < 1 \<and> is_real Mz \<and> poincare_distance (of_complex Mz) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex Mz) (moebius_pt (blaschke a) u) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- 1 < Re Mz \<and> Re Mz < 1 \<and> is_real Mz \<and> poincare_distance (of_complex Mz) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex Mz) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have "of_complex Mz \<in> unit_disc" "of_complex Mz \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex Mz \<in> unit_disc &&& of_complex Mz \<in> circline_set x_axis
[PROOF STEP]
using \<open>?R Mz ?Mx ?Mu\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re Mz \<and> Re Mz < 1 \<and> is_real Mz \<and> poincare_distance (of_complex Mz) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex Mz) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. of_complex Mz \<in> unit_disc &&& of_complex Mz \<in> circline_set x_axis
[PROOF STEP]
using cmod_eq_Re
[PROOF STATE]
proof (prove)
using this:
- 1 < Re Mz \<and> Re Mz < 1 \<and> is_real Mz \<and> poincare_distance (of_complex Mz) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex Mz) (moebius_pt (blaschke a) u)
is_real ?z \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
let ?Minv = "- (blaschke a)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
let ?z = "moebius_pt ?Minv (of_complex Mz)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have "?z \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
[PROOF STEP]
using \<open>of_complex Mz \<in> unit_disc\<close> \<open>cmod a < 1\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex Mz \<in> unit_disc
cmod a < 1

goal (1 subgoal):
 1. moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have "?z \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis
[PROOF STEP]
using \<open>of_complex Mz \<in> circline_set x_axis\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex Mz \<in> circline_set x_axis

goal (1 subgoal):
 1. moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis
[PROOF STEP]
using blaschke_real_preserve_x_axis \<open>is_real a\<close> \<open>cmod a < 1\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex Mz \<in> circline_set x_axis
\<lbrakk>is_real ?a; cmod ?a < 1\<rbrakk> \<Longrightarrow> (moebius_pt (blaschke ?a) ?z \<in> circline_set x_axis) = (?z \<in> circline_set x_axis)
is_real a
cmod a < 1

goal (1 subgoal):
 1. moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis
[PROOF STEP]
have z1: "-1 < Re (to_complex ?z)" "Re (to_complex ?z) < 1" "is_real (to_complex ?z)"
[PROOF STATE]
proof (prove)
using this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) &&& Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1 &&& is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))
[PROOF STEP]
using inf_or_of_complex[of "?z"]
[PROOF STATE]
proof (prove)
using this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
moebius_pt (- blaschke a) (of_complex Mz) \<in> circline_set x_axis
moebius_pt (- blaschke a) (of_complex Mz) = \<infinity>\<^sub>h \<or> (\<exists>x. moebius_pt (- blaschke a) (of_complex Mz) = of_complex x)

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) &&& Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1 &&& is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
moebius_pt (- blaschke a) (of_complex Mz) \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
moebius_pt (- blaschke a) (of_complex Mz) = \<infinity>\<^sub>h \<or> (\<exists>x. moebius_pt (- blaschke a) (of_complex Mz) = of_complex x)

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) &&& Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1 &&& is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))
Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1
is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
have z2: "poincare_distance ?z (of_complex x) = poincare_distance ?z u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) (of_complex x) = poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) u
[PROOF STEP]
using \<open>?R Mz ?Mx ?Mu\<close> \<open>cmod a < 1\<close> \<open>?z \<in> unit_disc\<close> \<open>of_complex x \<in> unit_disc\<close> \<open>u \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re Mz \<and> Re Mz < 1 \<and> is_real Mz \<and> poincare_distance (of_complex Mz) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex Mz) (moebius_pt (blaschke a) u)
cmod a < 1
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
of_complex x \<in> unit_disc
u \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) (of_complex x) = poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) u
[PROOF STEP]
by (metis blaschke_preserve_distance_formula blaschke_unit_disc_fix moebius_pt_comp_inv_right poincare_distance_formula uminus_moebius_def unit_disc_fix_discI unit_disc_iff_cmod_lt_1)
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) (of_complex x) = poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) u

goal (1 subgoal):
 1. \<And>x. \<lbrakk>- 1 < Re x; Re x < 1; is_real x; of_complex x \<noteq> u\<rbrakk> \<Longrightarrow> \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
show "?P (of_complex x) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. - 1 < Re ?a \<and> Re ?a < 1 \<and> is_real ?a \<and> poincare_distance (of_complex ?a) (of_complex x) = poincare_distance (of_complex ?a) u
 2. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = ?a
[PROOF STEP]
show "?R (to_complex ?z) (of_complex x) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) \<and> Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1 \<and> is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))) (of_complex x) = poincare_distance (of_complex (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))) u
[PROOF STEP]
using z1 z2 \<open>?z \<in> unit_disc\<close> inf_or_of_complex[of ?z]
[PROOF STATE]
proof (prove)
using this:
- 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))
Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1
is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))
poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) (of_complex x) = poincare_distance (moebius_pt (- blaschke a) (of_complex Mz)) u
moebius_pt (- blaschke a) (of_complex Mz) \<in> unit_disc
moebius_pt (- blaschke a) (of_complex Mz) = \<infinity>\<^sub>h \<or> (\<exists>x. moebius_pt (- blaschke a) (of_complex Mz) = of_complex x)

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) \<and> Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1 \<and> is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))) (of_complex x) = poincare_distance (of_complex (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))) u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) \<and> Re (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) < 1 \<and> is_real (to_complex (moebius_pt (- blaschke a) (of_complex Mz))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))) (of_complex x) = poincare_distance (of_complex (to_complex (moebius_pt (- blaschke a) (of_complex Mz)))) u

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
fix z'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
assume "?R z' (of_complex x) u"
[PROOF STATE]
proof (state)
this:
- 1 < Re z' \<and> Re z' < 1 \<and> is_real z' \<and> poincare_distance (of_complex z') (of_complex x) = poincare_distance (of_complex z') u

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
hence "of_complex z' \<in> unit_disc" "of_complex z' \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
- 1 < Re z' \<and> Re z' < 1 \<and> is_real z' \<and> poincare_distance (of_complex z') (of_complex x) = poincare_distance (of_complex z') u

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)
[PROOF STATE]
proof (state)
this:
of_complex z' \<in> unit_disc
of_complex z' \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
let ?Mz' = "?M (of_complex z')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
have "?Mz' \<in> unit_disc" "?Mz' \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex z') \<in> unit_disc &&& moebius_pt (blaschke a) (of_complex z') \<in> circline_set x_axis
[PROOF STEP]
using \<open>of_complex z' \<in> unit_disc\<close> \<open>of_complex z' \<in> circline_set x_axis\<close> \<open>cmod a < 1\<close> \<open>is_real a\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex z' \<in> unit_disc
of_complex z' \<in> circline_set x_axis
cmod a < 1
is_real a

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex z') \<in> unit_disc &&& moebius_pt (blaschke a) (of_complex z') \<in> circline_set x_axis
[PROOF STEP]
using  blaschke_unit_disc_fix unit_disc_fix_discI
[PROOF STATE]
proof (prove)
using this:
of_complex z' \<in> unit_disc
of_complex z' \<in> circline_set x_axis
cmod a < 1
is_real a
cmod ?a < 1 \<Longrightarrow> unit_disc_fix (blaschke ?a)
\<lbrakk>unit_disc_fix ?M; ?u \<in> unit_disc\<rbrakk> \<Longrightarrow> moebius_pt ?M ?u \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex z') \<in> unit_disc &&& moebius_pt (blaschke a) (of_complex z') \<in> circline_set x_axis
[PROOF STEP]
using blaschke_real_preserve_x_axis circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
of_complex z' \<in> unit_disc
of_complex z' \<in> circline_set x_axis
cmod a < 1
is_real a
cmod ?a < 1 \<Longrightarrow> unit_disc_fix (blaschke ?a)
\<lbrakk>unit_disc_fix ?M; ?u \<in> unit_disc\<rbrakk> \<Longrightarrow> moebius_pt ?M ?u \<in> unit_disc
\<lbrakk>is_real ?a; cmod ?a < 1\<rbrakk> \<Longrightarrow> (moebius_pt (blaschke ?a) ?z \<in> circline_set x_axis) = (?z \<in> circline_set x_axis)
circline_set x_axis = of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex z') \<in> unit_disc &&& moebius_pt (blaschke a) (of_complex z') \<in> circline_set x_axis
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex z') \<in> unit_disc
moebius_pt (blaschke a) (of_complex z') \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
hence "-1 < Re (to_complex ?Mz')" "Re (to_complex ?Mz') < 1" "is_real (to_complex ?Mz')"
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex z') \<in> unit_disc
moebius_pt (blaschke a) (of_complex z') \<in> circline_set x_axis

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) &&& Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 &&& is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex z') \<in> unit_disc
moebius_pt (blaschke a) (of_complex z') \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) &&& Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 &&& is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z')))
Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1
is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z')))
Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1
is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
have "poincare_distance ?Mz' ?Mx = poincare_distance ?Mz' ?Mu"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)
[PROOF STEP]
using \<open>?R z' (of_complex x) u\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re z' \<and> Re z' < 1 \<and> is_real z' \<and> poincare_distance (of_complex z') (of_complex x) = poincare_distance (of_complex z') u

goal (1 subgoal):
 1. poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)
[PROOF STEP]
using \<open>cmod a < 1\<close> \<open>of_complex x \<in> unit_disc\<close> \<open>of_complex z' \<in> unit_disc\<close> \<open>u \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re z' \<and> Re z' < 1 \<and> is_real z' \<and> poincare_distance (of_complex z') (of_complex x) = poincare_distance (of_complex z') u
cmod a < 1
of_complex x \<in> unit_disc
of_complex z' \<in> unit_disc
u \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z')))
Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1
is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))
poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)
[PROOF STEP]
have "?R (to_complex ?Mz') ?Mx ?Mu"
[PROOF STATE]
proof (prove)
using this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z')))
Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1
is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))
poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) u)
[PROOF STEP]
using \<open>?Mz' \<in> unit_disc\<close> inf_or_of_complex[of ?Mz']
[PROOF STATE]
proof (prove)
using this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z')))
Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1
is_real (to_complex (moebius_pt (blaschke a) (of_complex z')))
poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (moebius_pt (blaschke a) (of_complex z')) (moebius_pt (blaschke a) u)
moebius_pt (blaschke a) (of_complex z') \<in> unit_disc
moebius_pt (blaschke a) (of_complex z') = \<infinity>\<^sub>h \<or> (\<exists>x. moebius_pt (blaschke a) (of_complex z') = of_complex x)

goal (1 subgoal):
 1. - 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
hence "?Mz' = of_complex Mz"
[PROOF STATE]
proof (prove)
using this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex z') = of_complex Mz
[PROOF STEP]
using \<open>?P ?Mx ?Mu\<close> \<open>?R Mz ?Mx ?Mu\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> Re (to_complex (moebius_pt (blaschke a) (of_complex z'))) < 1 \<and> is_real (to_complex (moebius_pt (blaschke a) (of_complex z'))) \<and> poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex (to_complex (moebius_pt (blaschke a) (of_complex z')))) (moebius_pt (blaschke a) u)
\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex z) (moebius_pt (blaschke a) u)
- 1 < Re Mz \<and> Re Mz < 1 \<and> is_real Mz \<and> poincare_distance (of_complex Mz) (moebius_pt (blaschke a) (of_complex x)) = poincare_distance (of_complex Mz) (moebius_pt (blaschke a) u)

goal (1 subgoal):
 1. moebius_pt (blaschke a) (of_complex z') = of_complex Mz
[PROOF STEP]
by (metis \<open>moebius_pt (blaschke a) (of_complex z') \<in> unit_disc\<close> \<open>of_complex Mz \<in> unit_disc\<close> to_complex_of_complex unit_disc_to_complex_inj)
[PROOF STATE]
proof (state)
this:
moebius_pt (blaschke a) (of_complex z') = of_complex Mz

goal (1 subgoal):
 1. \<And>z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u \<Longrightarrow> z = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
thus "z' = to_complex ?z"
[PROOF STATE]
proof (prove)
using this:
moebius_pt (blaschke a) (of_complex z') = of_complex Mz

goal (1 subgoal):
 1. z' = to_complex (moebius_pt (- blaschke a) (of_complex Mz))
[PROOF STEP]
by (simp add: moebius_pt_invert)
[PROOF STATE]
proof (state)
this:
z' = to_complex (moebius_pt (- blaschke a) (of_complex Mz))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> u \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) u)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> of_complex y \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y))

goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> of_complex y \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y))

goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x. - 1 < Re x \<and> Re x < 1 \<and> is_real x \<and> of_complex x \<noteq> of_complex y \<longrightarrow> (\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y))
is_real x
- 1 < Re x
Re x < 1
is_real y
- 1 < Re y
Re y < 1
x \<noteq> y

goal (1 subgoal):
 1. \<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)
[PROOF STEP]
by (metis to_complex_of_complex)
[PROOF STATE]
proof (state)
this:
\<exists>!z. - 1 < Re z \<and> Re z < 1 \<and> is_real z \<and> poincare_distance (of_complex z) (of_complex x) = poincare_distance (of_complex z) (of_complex y)

goal:
No subgoals!
[PROOF STEP]
qed