[STATEMENT]
lemma poincare_distance_formula:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)" (is "?P u v")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
proof (rule wlog_x_axis)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
assume *: "is_real x" "0 \<le> Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 \<le> Re x
Re x < 1

goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
show "?P  0\<^sub>h (of_complex x)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
have "of_complex x \<in> unit_disc" "of_complex x \<in> circline_set x_axis" "cmod x < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> unit_disc &&& of_complex x \<in> circline_set x_axis &&& cmod x < 1
[PROOF STEP]
using * cmod_eq_Re
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1
is_real ?z \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>

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

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
hence "?lhs = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>"
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
of_complex x \<in> circline_set x_axis
cmod x < 1

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
using poincare_distance_zero_x_axis[of "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
of_complex x \<in> circline_set x_axis
cmod x < 1
\<lbrakk>of_complex x \<in> unit_disc; of_complex x \<in> circline_set x_axis\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = (let x' = to_complex (of_complex x) in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (of_complex x) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (of_complex x) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
have "?rhs = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
let ?x = "1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "0 \<le> 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)
[PROOF STEP]
by (smt \<open>cmod x < 1\<close> divide_nonneg_nonneg norm_ge_zero power_le_one zero_le_power2)
[PROOF STATE]
proof (state)
this:
0 \<le> 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
hence arcosh_real_gt: "1 \<le> ?x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)

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

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "?rhs = arcosh ?x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "... = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * (cmod x) / (1 - (cmod x)\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
have "1 - (cmod x)\<^sup>2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2
[PROOF STEP]
using \<open>cmod x < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod x < 1

goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2
[PROOF STEP]
by (smt norm_not_less_zero one_power2 power2_eq_imp_eq power_mono)
[PROOF STATE]
proof (state)
this:
0 < 1 - (cmod x)\<^sup>2

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

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

goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
have 2: "?x\<^sup>2 - 1 = (4 * (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))\<^sup>2 - 1 = 4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2
[PROOF STEP]
using \<open>1 - (cmod x)\<^sup>2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod x)\<^sup>2

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))\<^sup>2 - 1 = 4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2
[PROOF STEP]
apply (subst 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2))\<^sup>2 - 1 = 4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2
[PROOF STEP]
unfolding power_divide
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> (1 + (cmod x)\<^sup>2)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2 - 1 = 4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2
[PROOF STEP]
by (subst divide_diff_eq_iff, simp, simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
(1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))\<^sup>2 - 1 = 4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2

goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
using \<open>1 - (cmod x)\<^sup>2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod x)\<^sup>2

goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (subst arcosh_real_def[OF arcosh_real_gt])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> ln (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2) + sqrt ((1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))\<^sup>2 - 1)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (subst 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> ln (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2) + sqrt (4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (subst 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + sqrt (4 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (subst real_sqrt_divide)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + sqrt (4 * (cmod x)\<^sup>2) / sqrt ((1 - (cmod x)\<^sup>2)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (subst real_sqrt_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 \<Longrightarrow> ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + sqrt 4 * sqrt ((cmod x)\<^sup>2) / sqrt ((1 - (cmod x)\<^sup>2)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))

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

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
arcosh (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "... = ln (((1 + (cmod x))\<^sup>2) / (1 - (cmod x)\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (subst add_divide_distrib[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln ((1 + (cmod x)\<^sup>2 + 2 * cmod x) / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))
[PROOF STEP]
apply (simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln ((1 + (cmod x)\<^sup>2) / (1 - (cmod x)\<^sup>2) + 2 * cmod x / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "... = ln ((1 + cmod x) / (1 - (cmod x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x) / (1 - cmod x))
[PROOF STEP]
using \<open>cmod x < 1\<close>
[PROOF STATE]
proof (prove)
using this:
cmod x < 1

goal (1 subgoal):
 1. ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x) / (1 - cmod x))
[PROOF STEP]
using square_diff_square_factored[of 1 "cmod x"]
[PROOF STATE]
proof (prove)
using this:
cmod x < 1
1 * 1 - cmod x * cmod x = (1 + cmod x) * (1 - cmod x)

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

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ln ((1 + cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) = ln ((1 + cmod x) / (1 - cmod x))

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "... = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have *: "Re ((1 - x) / (1 + x)) \<le> 1" "Re ((1 - x) / (1 + x)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ((1 - x) / (1 + x)) \<le> 1 &&& 0 < Re ((1 - x) / (1 + x))
[PROOF STEP]
using \<open>is_real x\<close> \<open>Re x \<ge> 0\<close> \<open>Re x < 1\<close>
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1

goal (1 subgoal):
 1. Re ((1 - x) / (1 + x)) \<le> 1 &&& 0 < Re ((1 - x) / (1 + x))
[PROOF STEP]
using complex_is_Real_iff
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1
(?z \<in> \<real>) = is_real ?z

goal (1 subgoal):
 1. Re ((1 - x) / (1 + x)) \<le> 1 &&& 0 < Re ((1 - x) / (1 + x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re ((1 - x) / (1 + x)) \<le> 1
0 < Re ((1 - x) / (1 + x))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
hence "\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = - ln (Re ((1 - x) / (1 + x)))"
[PROOF STATE]
proof (prove)
using this:
Re ((1 - x) / (1 + x)) \<le> 1
0 < Re ((1 - x) / (1 + x))

goal (1 subgoal):
 1. \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = - ln (Re ((1 - x) / (1 + x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = - ln (Re ((1 - x) / (1 + x)))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
hence "\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))"
[PROOF STATE]
proof (prove)
using this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = - ln (Re ((1 - x) / (1 + x)))

goal (1 subgoal):
 1. \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))
[PROOF STEP]
using ln_div[of 1 "Re ((1 - x)/(1 + x))"] * \<open>is_real x\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = - ln (Re ((1 - x) / (1 + x)))
\<lbrakk>0 < 1; 0 < Re ((1 - x) / (1 + x))\<rbrakk> \<Longrightarrow> ln (1 / Re ((1 - x) / (1 + x))) = ln 1 - ln (Re ((1 - x) / (1 + x)))
Re ((1 - x) / (1 + x)) \<le> 1
0 < Re ((1 - x) / (1 + x))
is_real x

goal (1 subgoal):
 1. \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))
[PROOF STEP]
by (simp add: complex_is_Real_iff)
[PROOF STATE]
proof (state)
this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))
[PROOF STEP]
using \<open>Re x \<ge> 0\<close> \<open>is_real x\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re x
is_real x

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))
[PROOF STEP]
using cmod_eq_Re
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re x
is_real x
is_real ?z \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
have "(1 + Re x) / (1 - Re x) = Re ((1 + x) / (1 - x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + Re x) / (1 - Re x) = Re ((1 + x) / (1 - x))
[PROOF STEP]
using \<open>is_real x\<close> \<open>Re x < 1\<close>
[PROOF STATE]
proof (prove)
using this:
is_real x
Re x < 1

goal (1 subgoal):
 1. (1 + Re x) / (1 - Re x) = Re ((1 + x) / (1 - x))
[PROOF STEP]
by (smt Re_divide_real eq_iff_diff_eq_0 minus_complex.simps one_complex.simps plus_complex.simps)
[PROOF STATE]
proof (state)
this:
(1 + Re x) / (1 - Re x) = Re ((1 + x) / (1 - x))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))
ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))
(1 + Re x) / (1 - Re x) = Re ((1 + x) / (1 - x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = ln (Re ((1 + x) / (1 - x)))
ln ((1 + cmod x) / (1 - cmod x)) = ln ((1 + Re x) / (1 - Re x))
(1 + Re x) / (1 - Re x) = Re ((1 + x) / (1 - x))

goal (1 subgoal):
 1. ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ln ((1 + cmod x) / (1 - cmod x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal (1 subgoal):
 1. poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poincare_distance 0\<^sub>h (of_complex x) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poincare_distance 0\<^sub>h (of_complex x) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>
poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x)) = \<bar>ln (Re ((1 - x) / (1 + x)))\<bar>

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))

goal (3 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
fix M u v
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
assume *: "unit_disc_fix M"  "u \<in> unit_disc" "v \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

goal (3 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
assume "?P (moebius_pt M u) (moebius_pt M v)"
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))

goal (3 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))\<rbrakk> \<Longrightarrow> poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
thus "?P u v"
[PROOF STATE]
proof (prove)
using this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance_formula (to_complex (moebius_pt M u)) (to_complex (moebius_pt M v))

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

goal (1 subgoal):
 1. poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
by (simp del: poincare_distance_formula_def)
[PROOF STATE]
proof (state)
this:
poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)

goal (2 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
[PROOF STEP]
show "u \<in> unit_disc" "v \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> unit_disc &&& v \<in> unit_disc
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
v \<in> unit_disc

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poincare_distance_sym:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance u v = poincare_distance v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u v = poincare_distance v u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance u v = poincare_distance v u
[PROOF STEP]
using poincare_distance_formula[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)

goal (1 subgoal):
 1. poincare_distance u v = poincare_distance v u
[PROOF STEP]
using poincare_distance_formula[OF assms(2) assms(1)]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
poincare_distance v u = poincare_distance_formula (to_complex v) (to_complex u)

goal (1 subgoal):
 1. poincare_distance u v = poincare_distance v u
[PROOF STEP]
by (simp add: mult.commute norm_minus_commute)


[STATEMENT]
lemma poincare_distance_formula'_ge_1:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)
[PROOF STEP]
using unit_disc_cmod_square_lt_1[OF assms(1)] unit_disc_cmod_square_lt_1[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
(cmod (to_complex u))\<^sup>2 < 1
(cmod (to_complex v))\<^sup>2 < 1

goal (1 subgoal):
 1. 1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)
[PROOF STEP]
by auto


[STATEMENT]
lemma poincare_distance_ge0:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance u v \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> poincare_distance u v
[PROOF STEP]
using poincare_distance_formula'_ge_1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> 1 \<le> poincare_distance_formula' (to_complex ?u) (to_complex ?v)

goal (1 subgoal):
 1. 0 \<le> poincare_distance u v
[PROOF STEP]
unfolding poincare_distance_formula[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> 1 \<le> poincare_distance_formula' (to_complex ?u) (to_complex ?v)

goal (1 subgoal):
 1. 0 \<le> poincare_distance_formula (to_complex u) (to_complex v)
[PROOF STEP]
unfolding poincare_distance_formula_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> 1 \<le> poincare_distance_formula' (to_complex ?u) (to_complex ?v)

goal (1 subgoal):
 1. 0 \<le> arcosh (poincare_distance_formula' (to_complex u) (to_complex v))
[PROOF STEP]
unfolding poincare_distance_formula'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc\<rbrakk> \<Longrightarrow> 1 \<le> 1 + 2 * ((cmod (to_complex ?u - to_complex ?v))\<^sup>2 / ((1 - (cmod (to_complex ?u))\<^sup>2) * (1 - (cmod (to_complex ?v))\<^sup>2)))

goal (1 subgoal):
 1. 0 \<le> arcosh (1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2))))
[PROOF STEP]
by (rule arcosh_ge_0, simp_all add: assms)


[STATEMENT]
lemma cosh_dist:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "cosh_dist u v = poincare_distance_formula' (to_complex u) (to_complex v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist u v = poincare_distance_formula' (to_complex u) (to_complex v)
[PROOF STEP]
using poincare_distance_formula[OF assms] poincare_distance_formula'_ge_1[OF assms]
[PROOF STATE]
proof (prove)
using this:
poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)

goal (1 subgoal):
 1. cosh_dist u v = poincare_distance_formula' (to_complex u) (to_complex v)
[PROOF STEP]
by simp


[STATEMENT]
lemma poincare_distance_eq_0_iff:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance u v = 0 \<longleftrightarrow> u = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poincare_distance u v = 0) = (u = v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. (poincare_distance u v = 0) = (u = v)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; poincare_distance u v = 0\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
using poincare_distance_formula'_ge_1[OF assms]
[PROOF STATE]
proof (prove)
using this:
1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)

goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; poincare_distance u v = 0\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
using unit_disc_cmod_square_lt_1[OF assms(1)] unit_disc_cmod_square_lt_1[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)
(cmod (to_complex u))\<^sup>2 < 1
(cmod (to_complex v))\<^sup>2 < 1

goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; poincare_distance u v = 0\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
unfolding poincare_distance_formula[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)
(cmod (to_complex u))\<^sup>2 < 1
(cmod (to_complex v))\<^sup>2 < 1

goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; poincare_distance_formula (to_complex u) (to_complex v) = 0\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
unfolding poincare_distance_formula_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> poincare_distance_formula' (to_complex u) (to_complex v)
(cmod (to_complex u))\<^sup>2 < 1
(cmod (to_complex v))\<^sup>2 < 1

goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; arcosh (poincare_distance_formula' (to_complex u) (to_complex v)) = 0\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
unfolding poincare_distance_formula'_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2)))
(cmod (to_complex u))\<^sup>2 < 1
(cmod (to_complex v))\<^sup>2 < 1

goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; arcosh (1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2)))) = 0\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
apply (subst (asm) arcosh_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2))); (cmod (to_complex u))\<^sup>2 < 1; (cmod (to_complex v))\<^sup>2 < 1; u \<in> unit_disc; v \<in> unit_disc\<rbrakk> \<Longrightarrow> 1 \<le> 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2)))
 2. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2))) = 1; 1 \<le> 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2))); (cmod (to_complex u))\<^sup>2 < 1; (cmod (to_complex v))\<^sup>2 < 1\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2))) = 1; 1 \<le> 1 + 2 * ((cmod (to_complex u - to_complex v))\<^sup>2 / ((1 - (cmod (to_complex u))\<^sup>2) * (1 - (cmod (to_complex v))\<^sup>2))); (cmod (to_complex u))\<^sup>2 < 1; (cmod (to_complex v))\<^sup>2 < 1\<rbrakk> \<Longrightarrow> u = v
[PROOF STEP]
apply (simp add: unit_disc_to_complex_inj)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma conjugate_preserve_poincare_distance [simp]:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance (conjugate u) (conjugate v) = poincare_distance u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
obtain u' v' where *: "u = of_complex u'" "v = of_complex v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u' v'. \<lbrakk>u = of_complex u'; v = of_complex v'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms inf_or_of_complex[of u] inf_or_of_complex[of v]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
u = \<infinity>\<^sub>h \<or> (\<exists>x. u = of_complex x)
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)

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

goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
have **: "conjugate u \<in> unit_disc" "conjugate v \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate u \<in> unit_disc &&& conjugate v \<in> unit_disc
[PROOF STEP]
using * assms
[PROOF STATE]
proof (prove)
using this:
u = of_complex u'
v = of_complex v'
u \<in> unit_disc
v \<in> unit_disc

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

goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
u = of_complex u'
v = of_complex v'

goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
using poincare_distance_formula[OF assms]
[PROOF STATE]
proof (prove)
using this:
u = of_complex u'
v = of_complex v'
poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)

goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
using poincare_distance_formula[OF **]
[PROOF STATE]
proof (prove)
using this:
u = of_complex u'
v = of_complex v'
poincare_distance u v = poincare_distance_formula (to_complex u) (to_complex v)
poincare_distance (conjugate u) (conjugate v) = poincare_distance_formula (to_complex (conjugate u)) (to_complex (conjugate v))

goal (1 subgoal):
 1. poincare_distance (conjugate u) (conjugate v) = poincare_distance u v
[PROOF STEP]
by (metis complex_cnj_diff complex_mod_cnj conjugate_of_complex poincare_distance_def poincare_distance_formula'_def poincare_distance_formula_def to_complex_of_complex)
[PROOF STATE]
proof (state)
this:
poincare_distance (conjugate u) (conjugate v) = poincare_distance u v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_x_axis_poincare_distance_negative':
  fixes d :: real
  assumes "d \<ge> 0"
  shows "let z = (1 - exp d) / (1 + exp d)
          in is_real z \<and> Re z \<le> 0 \<and> Re z > -1 \<and>
              of_complex z \<in> unit_disc \<and> of_complex z \<in> circline_set x_axis \<and>
              poincare_distance 0\<^sub>h (of_complex z) = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
have "exp d \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> exp d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> d

goal (1 subgoal):
 1. 1 \<le> exp d
[PROOF STEP]
using one_le_exp_iff[of d, symmetric]
[PROOF STATE]
proof (prove)
using this:
0 \<le> d
(0 \<le> d) = (1 \<le> exp d)

goal (1 subgoal):
 1. 1 \<le> exp d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
1 \<le> exp d

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
hence "1 + exp d \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> exp d

goal (1 subgoal):
 1. 1 + exp d \<noteq> 0
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
1 + exp d \<noteq> 0

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
let ?z = "(1 - exp d) / (1 + exp d)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
have "?z \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - exp d) / (1 + exp d) \<le> 0
[PROOF STEP]
using \<open>exp d \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> exp d

goal (1 subgoal):
 1. (1 - exp d) / (1 + exp d) \<le> 0
[PROOF STEP]
by (simp add: divide_nonpos_nonneg)
[PROOF STATE]
proof (state)
this:
(1 - exp d) / (1 + exp d) \<le> 0

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(1 - exp d) / (1 + exp d) \<le> 0

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
have "?z > -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 < (1 - exp d) / (1 + exp d)
[PROOF STEP]
using exp_gt_zero[of d]
[PROOF STATE]
proof (prove)
using this:
0 < exp d

goal (1 subgoal):
 1. - 1 < (1 - exp d) / (1 + exp d)
[PROOF STEP]
by (smt divide_less_eq_1_neg nonzero_minus_divide_right)
[PROOF STATE]
proof (state)
this:
- 1 < (1 - exp d) / (1 + exp d)

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- 1 < (1 - exp d) / (1 + exp d)

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
hence "abs ?z < 1"
[PROOF STATE]
proof (prove)
using this:
- 1 < (1 - exp d) / (1 + exp d)

goal (1 subgoal):
 1. \<bar>(1 - exp d) / (1 + exp d)\<bar> < 1
[PROOF STEP]
using \<open>?z \<le> 0\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < (1 - exp d) / (1 + exp d)
(1 - exp d) / (1 + exp d) \<le> 0

goal (1 subgoal):
 1. \<bar>(1 - exp d) / (1 + exp d)\<bar> < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>(1 - exp d) / (1 + exp d)\<bar> < 1

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
hence "cmod ?z < 1"
[PROOF STATE]
proof (prove)
using this:
\<bar>(1 - exp d) / (1 + exp d)\<bar> < 1

goal (1 subgoal):
 1. cmod (cor ((1 - exp d) / (1 + exp d))) < 1
[PROOF STEP]
by (metis norm_of_real)
[PROOF STATE]
proof (state)
this:
cmod (cor ((1 - exp d) / (1 + exp d))) < 1

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
hence "of_complex ?z \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
cmod (cor ((1 - exp d) / (1 + exp d))) < 1

goal (1 subgoal):
 1. of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
have "of_complex ?z \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
have "(1 - ?z) / (1 + ?z) = exp d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
have "1 + ?z = 2 / (1 + exp d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)
[PROOF STEP]
using \<open>1 + exp d \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 + exp d \<noteq> 0

goal (1 subgoal):
 1. 1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)
[PROOF STEP]
by (subst add_divide_eq_iff, auto)
[PROOF STATE]
proof (state)
this:
1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)

goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)

goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
have "1 - ?z = 2 * exp d / (1 + exp d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - (1 - exp d) / (1 + exp d) = 2 * exp d / (1 + exp d)
[PROOF STEP]
using \<open>1 + exp d \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 + exp d \<noteq> 0

goal (1 subgoal):
 1. 1 - (1 - exp d) / (1 + exp d) = 2 * exp d / (1 + exp d)
[PROOF STEP]
by (subst diff_divide_eq_iff, auto)
[PROOF STATE]
proof (state)
this:
1 - (1 - exp d) / (1 + exp d) = 2 * exp d / (1 + exp d)

goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)
1 - (1 - exp d) / (1 + exp d) = 2 * exp d / (1 + exp d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)
1 - (1 - exp d) / (1 + exp d) = 2 * exp d / (1 + exp d)

goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
using \<open>1 + exp d \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 + (1 - exp d) / (1 + exp d) = 2 / (1 + exp d)
1 - (1 - exp d) / (1 + exp d) = 2 * exp d / (1 + exp d)
1 + exp d \<noteq> 0

goal (1 subgoal):
 1. (1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(1 - exp d) / (1 + exp d) \<le> 0
- 1 < (1 - exp d) / (1 + exp d)
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis
(1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(1 - exp d) / (1 + exp d) \<le> 0
- 1 < (1 - exp d) / (1 + exp d)
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis
(1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
using poincare_distance_zero_x_axis[of "of_complex ?z"]
[PROOF STATE]
proof (prove)
using this:
(1 - exp d) / (1 + exp d) \<le> 0
- 1 < (1 - exp d) / (1 + exp d)
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis
(1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
\<lbrakk>of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc; of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = (let x' = to_complex (of_complex (cor ((1 - exp d) / (1 + exp d)))) in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
using \<open>d \<ge> 0\<close> \<open>exp d \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
(1 - exp d) / (1 + exp d) \<le> 0
- 1 < (1 - exp d) / (1 + exp d)
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc
of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis
(1 - (1 - exp d) / (1 + exp d)) / (1 + (1 - exp d) / (1 + exp d)) = exp d
\<lbrakk>of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc; of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = (let x' = to_complex (of_complex (cor ((1 - exp d) / (1 + exp d)))) in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)
0 \<le> d
1 \<le> exp d

goal (1 subgoal):
 1. let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d
[PROOF STEP]
by simp (simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_x_axis_poincare_distance_negative:
  assumes "d \<ge> 0"
  shows "\<exists> z. is_real z \<and> Re z \<le> 0 \<and> Re z > -1 \<and>
              of_complex z \<in> unit_disc \<and> of_complex z \<in> circline_set x_axis \<and>
              poincare_distance 0\<^sub>h (of_complex z) = d" (is "\<exists> z. ?P z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> of_complex z \<in> unit_disc \<and> of_complex z \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
using ex_x_axis_poincare_distance_negative'[OF assms]
[PROOF STATE]
proof (prove)
using this:
let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d

goal (1 subgoal):
 1. \<exists>z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> of_complex z \<in> unit_disc \<and> of_complex z \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc \<and> of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d

goal (1 subgoal):
 1. \<exists>z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> of_complex z \<in> unit_disc \<and> of_complex z \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
by blast


[STATEMENT]
lemma unique_x_axis_poincare_distance_negative:
  assumes "d \<ge> 0"
  shows "\<exists>! z. is_real z \<and> Re z \<le> 0 \<and> Re z > -1 \<and>
              poincare_distance 0\<^sub>h (of_complex z) = d" (is "\<exists>! z. ?P z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
let ?z = "(1 - exp d) / (1 + exp d)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
have "?P ?z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d
[PROOF STEP]
using ex_x_axis_poincare_distance_negative'[OF assms]
[PROOF STATE]
proof (prove)
using this:
let x = (1 - exp d) / (1 + exp d) in is_real (cor x) \<and> Re (cor x) \<le> 0 \<and> - 1 < Re (cor x) \<and> of_complex (cor x) \<in> unit_disc \<and> of_complex (cor x) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor x)) = d

goal (1 subgoal):
 1. is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> unit_disc \<and> of_complex (cor ((1 - exp d) / (1 + exp d))) \<in> circline_set x_axis \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d

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

goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d

goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
have "\<forall> z'. ?P z' \<longrightarrow> z' = ?z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
let ?g = "\<lambda> x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
let ?A = "{x. is_real x \<and> Re x > -1 \<and> Re x \<le> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
have "inj_on (poincare_distance 0\<^sub>h \<circ> of_complex) ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (poincare_distance 0\<^sub>h \<circ> of_complex) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
[PROOF STEP]
proof (rule comp_inj_on)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on of_complex {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
 2. inj_on (poincare_distance 0\<^sub>h) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
show "inj_on of_complex ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on of_complex {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
[PROOF STEP]
using of_complex_inj
[PROOF STATE]
proof (prove)
using this:
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. inj_on of_complex {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
of_complex ?x = of_complex ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<forall>x\<in>{x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. \<forall>y\<in>{x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. of_complex x = of_complex y \<longrightarrow> x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on of_complex {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. inj_on (poincare_distance 0\<^sub>h) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on (poincare_distance 0\<^sub>h) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
show "inj_on (poincare_distance 0\<^sub>h) (of_complex ` ?A)" (is "inj_on ?f (of_complex ` ?A)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (poincare_distance 0\<^sub>h) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
proof (subst inj_on_cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} \<Longrightarrow> poincare_distance 0\<^sub>h a = ?g a
 2. inj_on ?g (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
have *: "of_complex ` ?A =
                 {z. z \<in> unit_disc \<and> z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}" (is "_ = ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} = {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}
[PROOF STEP]
by (auto simp add: cmod_eq_Re circline_set_x_axis)
[PROOF STATE]
proof (state)
this:
of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} = {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}

goal (2 subgoals):
 1. \<And>a. a \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} \<Longrightarrow> poincare_distance 0\<^sub>h a = ?g a
 2. inj_on ?g (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. a \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} \<Longrightarrow> poincare_distance 0\<^sub>h a = ?g a
 2. inj_on ?g (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
assume "x \<in> of_complex ` ?A"
[PROOF STATE]
proof (state)
this:
x \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (2 subgoals):
 1. \<And>a. a \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} \<Longrightarrow> poincare_distance 0\<^sub>h a = ?g a
 2. inj_on ?g (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
hence "x \<in> ?B"
[PROOF STATE]
proof (prove)
using this:
x \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. x \<in> {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
x \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} = {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}

goal (1 subgoal):
 1. x \<in> {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}

goal (2 subgoals):
 1. \<And>a. a \<in> of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} \<Longrightarrow> poincare_distance 0\<^sub>h a = ?g a
 2. inj_on ?g (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
thus "poincare_distance 0\<^sub>h x = (?g \<circ> to_complex) x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) x
[PROOF STEP]
using poincare_distance_zero_x_axis
[PROOF STATE]
proof (prove)
using this:
x \<in> {z \<in> unit_disc. z \<in> circline_set x_axis \<and> Re (to_complex z) \<le> 0}
\<lbrakk>?x \<in> unit_disc; ?x \<in> circline_set x_axis\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h ?x = (let x' = to_complex ?x in \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>)

goal (1 subgoal):
 1. poincare_distance 0\<^sub>h x = ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) x
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
poincare_distance 0\<^sub>h x = ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) x

goal (1 subgoal):
 1. inj_on ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
have *: "to_complex ` of_complex ` ?A = ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} = {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
[PROOF STEP]
by (auto simp add: image_iff)
[PROOF STATE]
proof (state)
this:
to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} = {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. inj_on ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
show "inj_on (?g \<circ> to_complex) (of_complex ` ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
proof (rule comp_inj_on)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on to_complex (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
 2. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
show "inj_on to_complex (of_complex ` ?A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on to_complex (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. \<forall>y\<in>of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. to_complex x = to_complex y \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on to_complex (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})

goal (1 subgoal):
 1. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
have "inj_on ?g ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. \<forall>y\<in>{x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar> \<longrightarrow> x = y
[PROOF STEP]
proof(safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume hh: "is_real x" "is_real y" "- 1 < Re x" "Re x \<le> 0"
              "- 1 < Re y" "Re y \<le> 0" "\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>"
[PROOF STATE]
proof (state)
this:
is_real x
is_real y
- 1 < Re x
Re x \<le> 0
- 1 < Re y
Re y \<le> 0
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "is_real ((1 - x)/(1 + x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real ((1 - x) / (1 + x))
[PROOF STEP]
using \<open>is_real x\<close> div_reals[of "1-x" "1+x"]
[PROOF STATE]
proof (prove)
using this:
is_real x
\<lbrakk>is_real (1 - x); is_real (1 + x)\<rbrakk> \<Longrightarrow> is_real ((1 - x) / (1 + x))

goal (1 subgoal):
 1. is_real ((1 - x) / (1 + x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real ((1 - x) / (1 + x))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "is_real ((1 - y)/(1 + y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real ((1 - y) / (1 + y))
[PROOF STEP]
using \<open>is_real y\<close> div_reals[of "1-y" "1+y"]
[PROOF STATE]
proof (prove)
using this:
is_real y
\<lbrakk>is_real (1 - y); is_real (1 + y)\<rbrakk> \<Longrightarrow> is_real ((1 - y) / (1 + y))

goal (1 subgoal):
 1. is_real ((1 - y) / (1 + y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real ((1 - y) / (1 + y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "Re (1 + x) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Re (1 + x)
[PROOF STEP]
using \<open>- 1 < Re x\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re x

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "1 + x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < Re (1 + x)

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "Re (1 - x) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re (1 - x)
[PROOF STEP]
using \<open>Re x \<le> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Re x \<le> 0

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "Re ((1 - x)/(1 + x)) > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re (1 - x)

goal (1 subgoal):
 1. 0 < Re ((1 - x) / (1 + x))
[PROOF STEP]
using Re_divide_real \<open>0 < Re (1 + x)\<close> complex_eq_if_Re_eq hh(1) hh(4)
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re (1 - x)
\<lbrakk>is_real ?b; ?b \<noteq> 0\<rbrakk> \<Longrightarrow> Re (?a / ?b) = Re ?a / Re ?b
0 < Re (1 + x)
\<lbrakk>is_real ?z1.0; is_real ?z2.0\<rbrakk> \<Longrightarrow> (?z1.0 = ?z2.0) = (Re ?z1.0 = Re ?z2.0)
is_real x
Re x \<le> 0

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "Re(1 - x) \<ge> Re ( 1 + x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (1 + x) \<le> Re (1 - x)
[PROOF STEP]
using hh
[PROOF STATE]
proof (prove)
using this:
is_real x
is_real y
- 1 < Re x
Re x \<le> 0
- 1 < Re y
Re y \<le> 0
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "Re ((1 - x)/(1 + x)) \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
Re (1 + x) \<le> Re (1 - x)

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

goal (1 subgoal):
 1. 1 \<le> Re ((1 - x) / (1 + x))
[PROOF STEP]
by (smt Re_divide_real arg_0_iff hh(1) le_divide_eq_1_pos one_complex.simps(2) plus_complex.simps(2))
[PROOF STATE]
proof (state)
this:
1 \<le> Re ((1 - x) / (1 + x))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "Re (1 + y) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Re (1 + y)
[PROOF STEP]
using \<open>- 1 < Re y\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 < Re y

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "1 + y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < Re (1 + y)

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "Re (1 - y) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re (1 - y)
[PROOF STEP]
using \<open>Re y \<le> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Re y \<le> 0

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "Re ((1 - y)/(1 + y)) > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re (1 - y)

goal (1 subgoal):
 1. 0 < Re ((1 - y) / (1 + y))
[PROOF STEP]
using Re_divide_real \<open>0 < Re (1 + y)\<close> complex_eq_if_Re_eq hh
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re (1 - y)
\<lbrakk>is_real ?b; ?b \<noteq> 0\<rbrakk> \<Longrightarrow> Re (?a / ?b) = Re ?a / Re ?b
0 < Re (1 + y)
\<lbrakk>is_real ?z1.0; is_real ?z2.0\<rbrakk> \<Longrightarrow> (?z1.0 = ?z2.0) = (Re ?z1.0 = Re ?z2.0)
is_real x
is_real y
- 1 < Re x
Re x \<le> 0
- 1 < Re y
Re y \<le> 0
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>

goal (1 subgoal):
 1. 0 < Re ((1 - y) / (1 + y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < Re ((1 - y) / (1 + y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "Re(1 - y) \<ge> Re ( 1 + y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (1 + y) \<le> Re (1 - y)
[PROOF STEP]
using hh
[PROOF STATE]
proof (prove)
using this:
is_real x
is_real y
- 1 < Re x
Re x \<le> 0
- 1 < Re y
Re y \<le> 0
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>

goal (1 subgoal):
 1. Re (1 + y) \<le> Re (1 - y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re (1 + y) \<le> Re (1 - y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "Re ((1 - y)/(1 + y)) \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
Re (1 + y) \<le> Re (1 - y)

goal (1 subgoal):
 1. 1 \<le> Re ((1 - y) / (1 + y))
[PROOF STEP]
using \<open>Re (1 + y) > 0\<close> \<open>is_real ((1 - y)/(1 + y))\<close>
[PROOF STATE]
proof (prove)
using this:
Re (1 + y) \<le> Re (1 - y)
0 < Re (1 + y)
is_real ((1 - y) / (1 + y))

goal (1 subgoal):
 1. 1 \<le> Re ((1 - y) / (1 + y))
[PROOF STEP]
by (smt Re_divide_real arg_0_iff hh le_divide_eq_1_pos one_complex.simps(2) plus_complex.simps(2))
[PROOF STATE]
proof (state)
this:
1 \<le> Re ((1 - y) / (1 + y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "ln (Re ((1 - x) / (1 + x))) = ln (Re ((1 - y) / (1 + y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (Re ((1 - x) / (1 + x))) = ln (Re ((1 - y) / (1 + y)))
[PROOF STEP]
using \<open>Re ((1 - y)/(1 + y)) \<ge> 1\<close> \<open>Re ((1 - x)/(1 + x)) \<ge> 1\<close> hh
[PROOF STATE]
proof (prove)
using this:
1 \<le> Re ((1 - y) / (1 + y))
1 \<le> Re ((1 - x) / (1 + x))
is_real x
is_real y
- 1 < Re x
Re x \<le> 0
- 1 < Re y
Re y \<le> 0
\<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>

goal (1 subgoal):
 1. ln (Re ((1 - x) / (1 + x))) = ln (Re ((1 - y) / (1 + y)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ln (Re ((1 - x) / (1 + x))) = ln (Re ((1 - y) / (1 + y)))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))"
[PROOF STATE]
proof (prove)
using this:
ln (Re ((1 - x) / (1 + x))) = ln (Re ((1 - y) / (1 + y)))

goal (1 subgoal):
 1. Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))
[PROOF STEP]
using \<open>Re ((1 - y)/(1 + y)) > 0\<close> \<open>Re ((1 - x)/(1 + x)) > 0\<close>
[PROOF STATE]
proof (prove)
using this:
ln (Re ((1 - x) / (1 + x))) = ln (Re ((1 - y) / (1 + y)))
0 < Re ((1 - y) / (1 + y))
0 < Re ((1 - x) / (1 + x))

goal (1 subgoal):
 1. Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "(1 - x) / (1 + x) = (1 - y) / (1 + y)"
[PROOF STATE]
proof (prove)
using this:
Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))

goal (1 subgoal):
 1. (1 - x) / (1 + x) = (1 - y) / (1 + y)
[PROOF STEP]
using \<open>is_real ((1 - y)/(1 + y))\<close> \<open>is_real ((1 - x)/(1 + x))\<close>
[PROOF STATE]
proof (prove)
using this:
Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))
is_real ((1 - y) / (1 + y))
is_real ((1 - x) / (1 + x))

goal (1 subgoal):
 1. (1 - x) / (1 + x) = (1 - y) / (1 + y)
[PROOF STEP]
using complex_eq_if_Re_eq
[PROOF STATE]
proof (prove)
using this:
Re ((1 - x) / (1 + x)) = Re ((1 - y) / (1 + y))
is_real ((1 - y) / (1 + y))
is_real ((1 - x) / (1 + x))
\<lbrakk>is_real ?z1.0; is_real ?z2.0\<rbrakk> \<Longrightarrow> (?z1.0 = ?z2.0) = (Re ?z1.0 = Re ?z2.0)

goal (1 subgoal):
 1. (1 - x) / (1 + x) = (1 - y) / (1 + y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(1 - x) / (1 + x) = (1 - y) / (1 + y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "(1 - x) * (1 + y) = (1 - y) * (1 + x)"
[PROOF STATE]
proof (prove)
using this:
(1 - x) / (1 + x) = (1 - y) / (1 + y)

goal (1 subgoal):
 1. (1 - x) * (1 + y) = (1 - y) * (1 + x)
[PROOF STEP]
using \<open>1 + y \<noteq> 0\<close> \<open>1 + x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
(1 - x) / (1 + x) = (1 - y) / (1 + y)
1 + y \<noteq> 0
1 + x \<noteq> 0

goal (1 subgoal):
 1. (1 - x) * (1 + y) = (1 - y) * (1 + x)
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
(1 - x) * (1 + y) = (1 - y) * (1 + x)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_real x; is_real y; - 1 < Re x; Re x \<le> 0; - 1 < Re y; Re y \<le> 0; \<bar>ln (Re ((1 - x) / (1 + x)))\<bar> = \<bar>ln (Re ((1 - y) / (1 + y)))\<bar>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
(1 - x) * (1 + y) = (1 - y) * (1 + x)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (simp add:field_simps)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
thus "inj_on ?g (to_complex ` of_complex ` ?A)"
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0} = {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) (to_complex ` of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on ((\<lambda>x'. \<bar>ln (Re ((1 - x') / (1 + x')))\<bar>) \<circ> to_complex) (of_complex ` {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0})

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

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

goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (poincare_distance 0\<^sub>h \<circ> of_complex) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}

goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
using \<open>?P ?z\<close>
[PROOF STATE]
proof (prove)
using this:
inj_on (poincare_distance 0\<^sub>h \<circ> of_complex) {x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d

goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. \<forall>y\<in>{x. is_real x \<and> - 1 < Re x \<and> Re x \<le> 0}. (poincare_distance 0\<^sub>h \<circ> of_complex) x = (poincare_distance 0\<^sub>h \<circ> of_complex) y \<longrightarrow> x = y
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d

goal (1 subgoal):
 1. \<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))

goal (1 subgoal):
 1. \<exists>!z. is_real z \<and> Re z \<le> 0 \<and> - 1 < Re z \<and> poincare_distance 0\<^sub>h (of_complex z) = d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d
\<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_real (cor ((1 - exp d) / (1 + exp d))) \<and> Re (cor ((1 - exp d) / (1 + exp d))) \<le> 0 \<and> - 1 < Re (cor ((1 - exp d) / (1 + exp d))) \<and> poincare_distance 0\<^sub>h (of_complex (cor ((1 - exp d) / (1 + exp d)))) = d
\<forall>z'. is_real z' \<and> Re z' \<le> 0 \<and> - 1 < Re z' \<and> poincare_distance 0\<^sub>h (of_complex z') = d \<longrightarrow> z' = cor ((1 - exp d) / (1 + exp d))

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed