[STATEMENT]
lemma poincare_distance_formula_zero_sum:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v =
         (let u' = cmod (to_complex u); v' = cmod (to_complex v)
           in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
obtain u' v' where uv: "u' = to_complex u" "v' = to_complex v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u' v'. \<lbrakk>u' = to_complex u; v' = to_complex v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' = to_complex u
v' = to_complex v

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
have uv': "u = of_complex u'" "v = of_complex v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = of_complex u' &&& v = of_complex v'
[PROOF STEP]
using uv assms inf_or_of_complex[of u] inf_or_of_complex[of v]
[PROOF STATE]
proof (prove)
using this:
u' = to_complex u
v' = to_complex v
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. u = of_complex u' &&& v = of_complex v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = of_complex u'
v = of_complex v'

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
let ?u' = "cmod u'" and ?v' = "cmod v'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
have disc: "?u'\<^sup>2 < 1" "?v'\<^sup>2 < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod u')\<^sup>2 < 1 &&& (cmod v')\<^sup>2 < 1
[PROOF STEP]
using unit_disc_cmod_square_lt_1[OF \<open>u \<in> unit_disc\<close>]
[PROOF STATE]
proof (prove)
using this:
(cmod (to_complex u))\<^sup>2 < 1

goal (1 subgoal):
 1. (cmod u')\<^sup>2 < 1 &&& (cmod v')\<^sup>2 < 1
[PROOF STEP]
using unit_disc_cmod_square_lt_1[OF \<open>v \<in> unit_disc\<close>] uv
[PROOF STATE]
proof (prove)
using this:
(cmod (to_complex u))\<^sup>2 < 1
(cmod (to_complex v))\<^sup>2 < 1
u' = to_complex u
v' = to_complex v

goal (1 subgoal):
 1. (cmod u')\<^sup>2 < 1 &&& (cmod v')\<^sup>2 < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
thm arcosh_add
[PROOF STATE]
proof (state)
this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
have "arcosh (1 + 2 * ?u'\<^sup>2 / (1 - ?u'\<^sup>2)) + arcosh (1 + 2 * ?v'\<^sup>2 / (1 - ?v'\<^sup>2)) =
        arcosh (((1 + ?u'\<^sup>2) * (1 + ?v'\<^sup>2) + 4 * ?u' * ?v') / ((1 - ?u'\<^sup>2) * (1 - ?v'\<^sup>2)))" (is "arcosh ?ll + arcosh ?rr = arcosh ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcosh (1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) + arcosh (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
proof (subst arcosh_add)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 1 \<le> 1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)
 2. 1 \<le> 1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)
 3. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
show "?ll \<ge> 1"  "?rr \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) &&& 1 \<le> 1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

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

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
show "arcosh ((1 + 2 * ?u'\<^sup>2 / (1 - ?u'\<^sup>2)) * (1 + 2 * ?v'\<^sup>2 / (1 - ?v'\<^sup>2)) +
                  sqrt (((1 + 2 * ?u'\<^sup>2 / (1 - ?u'\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * ?v'\<^sup>2 / (1 - ?v'\<^sup>2))\<^sup>2 - 1))) =
          arcosh ?r" (is "arcosh ?l = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
have "1 + 2 * ?u'\<^sup>2 / (1 - ?u'\<^sup>2) = (1 + ?u'\<^sup>2) / (1 - ?u'\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. 1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)
[PROOF STEP]
by (subst add_divide_eq_iff, simp_all)
[PROOF STATE]
proof (state)
this:
1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
have "1 + 2 * ?v'\<^sup>2 / (1 - ?v'\<^sup>2) = (1 + ?v'\<^sup>2) / (1 - ?v'\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. 1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)
[PROOF STEP]
by (subst add_divide_eq_iff, simp_all)
[PROOF STATE]
proof (state)
this:
1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
have "sqrt (((1 + 2 * ?u'\<^sup>2 / (1 - ?u'\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * ?v'\<^sup>2 / (1 - ?v'\<^sup>2))\<^sup>2 - 1)) =
               (4  * ?u' * ?v') / ((1 - ?u'\<^sup>2) * (1 - ?v'\<^sup>2))" (is "sqrt ?s = ?t")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
have "?s = ?t\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1) = (4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))\<^sup>2
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1) = (4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))\<^sup>2
[PROOF STEP]
apply (subst add_divide_eq_iff, simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cmod u')\<^sup>2 < 1; (cmod v')\<^sup>2 < 1; (cmod u')\<^sup>2 < 1; (cmod v')\<^sup>2 < 1\<rbrakk> \<Longrightarrow> (((1 * (1 - (cmod u')\<^sup>2) + 2 * (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * (((1 * (1 - (cmod v')\<^sup>2) + 2 * (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1) = (4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))\<^sup>2
[PROOF STEP]
apply (subst power_divide)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cmod u')\<^sup>2 < 1; (cmod v')\<^sup>2 < 1; (cmod u')\<^sup>2 < 1; (cmod v')\<^sup>2 < 1\<rbrakk> \<Longrightarrow> ((1 * (1 - (cmod u')\<^sup>2) + 2 * (cmod u')\<^sup>2)\<^sup>2 / (1 - (cmod u')\<^sup>2)\<^sup>2 - 1) * ((1 * (1 - (cmod v')\<^sup>2) + 2 * (cmod v')\<^sup>2)\<^sup>2 / (1 - (cmod v')\<^sup>2)\<^sup>2 - 1) = (4 * cmod u' * cmod v')\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))\<^sup>2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cmod u')\<^sup>2 < 1; (cmod v')\<^sup>2 < 1\<rbrakk> \<Longrightarrow> (((cmod u')\<^sup>2 + 1)\<^sup>2 / (1 - (cmod u')\<^sup>2)\<^sup>2 - 1) * (((cmod v')\<^sup>2 + 1)\<^sup>2 / (1 - (cmod v')\<^sup>2)\<^sup>2 - 1) = (4 * cmod u' * cmod v')\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))\<^sup>2
[PROOF STEP]
apply (subst divide_diff_eq_iff, simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cmod u')\<^sup>2 < 1; (cmod v')\<^sup>2 < 1\<rbrakk> \<Longrightarrow> (((cmod u')\<^sup>2 + 1)\<^sup>2 - 1 * (1 - (cmod u')\<^sup>2)\<^sup>2) / (1 - (cmod u')\<^sup>2)\<^sup>2 * ((((cmod v')\<^sup>2 + 1)\<^sup>2 - 1 * (1 - (cmod v')\<^sup>2)\<^sup>2) / (1 - (cmod v')\<^sup>2)\<^sup>2) = (4 * cmod u' * cmod v')\<^sup>2 / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))\<^sup>2
[PROOF STEP]
apply (simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1) = (4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))\<^sup>2

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

goal (1 subgoal):
 1. sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1) = (4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))\<^sup>2
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

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

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)
1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)
sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
have "?l = ?r"
[PROOF STATE]
proof (prove)
using this:
1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)
1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)
sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = ((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2) = (1 + (cmod u')\<^sup>2) / (1 - (cmod u')\<^sup>2)
1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2) = (1 + (cmod v')\<^sup>2) / (1 - (cmod v')\<^sup>2)
sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = 4 * cmod u' * cmod v' / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
(cmod u')\<^sup>2 < 1
(cmod v')\<^sup>2 < 1

goal (1 subgoal):
 1. (1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = ((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))
[PROOF STEP]
by simp (subst add_divide_distrib, simp)
[PROOF STATE]
proof (state)
this:
(1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = ((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1)) = ((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2))

goal (1 subgoal):
 1. arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arcosh ((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) * (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) + sqrt (((1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2))\<^sup>2 - 1) * ((1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2))\<^sup>2 - 1))) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))

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

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

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
arcosh (1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) + arcosh (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
using uv' assms
[PROOF STATE]
proof (prove)
using this:
arcosh (1 + 2 * (cmod u')\<^sup>2 / (1 - (cmod u')\<^sup>2)) + arcosh (1 + 2 * (cmod v')\<^sup>2 / (1 - (cmod v')\<^sup>2)) = arcosh (((1 + (cmod u')\<^sup>2) * (1 + (cmod v')\<^sup>2) + 4 * cmod u' * cmod v') / ((1 - (cmod u')\<^sup>2) * (1 - (cmod v')\<^sup>2)))
u = of_complex u'
v = of_complex v'
u \<in> unit_disc
v \<in> unit_disc

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

goal (1 subgoal):
 1. poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
poincare_distance u 0\<^sub>h + poincare_distance 0\<^sub>h v = (let u' = cmod (to_complex u); v' = cmod (to_complex v) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poincare_distance_triangle_inequality:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc" and "w \<in> unit_disc"
  shows "poincare_distance u v + poincare_distance v w \<ge> poincare_distance u w" (is "?P' u v w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
[PROOF STEP]
have "\<forall> w. w \<in> unit_disc \<longrightarrow> ?P' u v w"  (is "?P v u")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
[PROOF STEP]
proof (rule wlog_x_axis[where P="?P"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. v \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. v \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[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. v \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
hence "of_complex x \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1

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

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

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> unit_disc
[PROOF STEP]
obtain w' where w: "w = of_complex w'"
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc

goal (1 subgoal):
 1. (\<And>w'. w = of_complex w' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of w]
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
w = \<infinity>\<^sub>h \<or> (\<exists>x. w = of_complex x)

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

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
let ?x = "cmod x" and ?w = "cmod w'" and ?xw = "cmod (x - w')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
have disc: "?x\<^sup>2 < 1" "?w\<^sup>2 < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod x)\<^sup>2 < 1 &&& (cmod w')\<^sup>2 < 1
[PROOF STEP]
using unit_disc_cmod_square_lt_1[OF \<open>of_complex x \<in> unit_disc\<close>]
[PROOF STATE]
proof (prove)
using this:
(cmod (to_complex (of_complex x)))\<^sup>2 < 1

goal (1 subgoal):
 1. (cmod x)\<^sup>2 < 1 &&& (cmod w')\<^sup>2 < 1
[PROOF STEP]
using unit_disc_cmod_square_lt_1[OF \<open>w \<in> unit_disc\<close>] w
[PROOF STATE]
proof (prove)
using this:
(cmod (to_complex (of_complex x)))\<^sup>2 < 1
(cmod (to_complex w))\<^sup>2 < 1
w = of_complex w'

goal (1 subgoal):
 1. (cmod x)\<^sup>2 < 1 &&& (cmod w')\<^sup>2 < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
have "poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w =
           arcosh (((1 + ?x\<^sup>2) * (1 + ?w\<^sup>2) + 4 * ?x * ?w) / ((1 - ?x\<^sup>2) * (1 - ?w\<^sup>2)))" (is "_ = arcosh ?r1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w = arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
[PROOF STEP]
using poincare_distance_formula_zero_sum[OF \<open>of_complex x \<in> unit_disc\<close> \<open>w \<in> unit_disc\<close>] w
[PROOF STATE]
proof (prove)
using this:
poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w = (let u' = cmod (to_complex (of_complex x)); v' = cmod (to_complex w) in arcosh (((1 + u'\<^sup>2) * (1 + v'\<^sup>2) + 4 * u' * v') / ((1 - u'\<^sup>2) * (1 - v'\<^sup>2))))
w = of_complex w'

goal (1 subgoal):
 1. poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w = arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w = arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w = arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
have "poincare_distance (of_complex x) (of_complex w') =
            arcosh (((1 - ?x\<^sup>2) * (1 - ?w\<^sup>2) + 2 * ?xw\<^sup>2) / ((1 - ?x\<^sup>2) * (1 - ?w\<^sup>2)))" (is "_ = arcosh ?r2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (of_complex x) (of_complex w') = arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1

goal (1 subgoal):
 1. poincare_distance (of_complex x) (of_complex w') = arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
[PROOF STEP]
using poincare_distance_formula[OF \<open>of_complex x \<in> unit_disc\<close> \<open>w \<in> unit_disc\<close>] w
[PROOF STATE]
proof (prove)
using this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1
poincare_distance (of_complex x) w = poincare_distance_formula (to_complex (of_complex x)) (to_complex w)
w = of_complex w'

goal (1 subgoal):
 1. poincare_distance (of_complex x) (of_complex w') = arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
[PROOF STEP]
by (subst add_divide_distrib) simp
[PROOF STATE]
proof (state)
this:
poincare_distance (of_complex x) (of_complex w') = arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poincare_distance (of_complex x) (of_complex w') = arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
have *: "(1 - ?x\<^sup>2) * (1 - ?w\<^sup>2) + 2 * ?xw\<^sup>2 \<le> (1 + ?x\<^sup>2) * (1 + ?w\<^sup>2) + 4 * ?x * ?w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2 \<le> (1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2 \<le> (1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w'
[PROOF STEP]
have "(cmod (x - w'))\<^sup>2 \<le> (cmod x + cmod w')\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (x - w'))\<^sup>2 \<le> (cmod x + cmod w')\<^sup>2
[PROOF STEP]
using norm_triangle_ineq4[of x w']
[PROOF STATE]
proof (prove)
using this:
cmod (x - w') \<le> cmod x + cmod w'

goal (1 subgoal):
 1. (cmod (x - w'))\<^sup>2 \<le> (cmod x + cmod w')\<^sup>2
[PROOF STEP]
by (simp add: power_mono)
[PROOF STATE]
proof (state)
this:
(cmod (x - w'))\<^sup>2 \<le> (cmod x + cmod w')\<^sup>2

goal (1 subgoal):
 1. (1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2 \<le> (1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(cmod (x - w'))\<^sup>2 \<le> (cmod x + cmod w')\<^sup>2

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2 \<le> (1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w'

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
have "arcosh ?r1 \<ge> arcosh ?r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))) \<le> arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
[PROOF STEP]
proof (subst arcosh_mono)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 1 \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
 2. 1 \<le> ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
 3. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
show "?r1 \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1

goal (1 subgoal):
 1. 1 \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
by (smt "*" le_divide_eq_1_pos mult_pos_pos zero_le_power2)
[PROOF STATE]
proof (state)
this:
1 \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))

goal (2 subgoals):
 1. 1 \<le> ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
 2. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 \<le> ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
 2. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
show "?r2 \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1

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

goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
show "?r1 \<ge> ?r2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
using disc
[PROOF STATE]
proof (prove)
using this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1

goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(cmod x)\<^sup>2 < 1
(cmod w')\<^sup>2 < 1
(1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2 \<le> (1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w'

goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))
[PROOF STEP]
by (subst divide_right_mono, simp_all)
[PROOF STATE]
proof (state)
this:
((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)) \<le> ((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))

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

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

goal (1 subgoal):
 1. poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w
[PROOF STEP]
using \<open>of_complex x \<in> unit_disc\<close> \<open>w \<in> unit_disc\<close> w
[PROOF STATE]
proof (prove)
using this:
poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w = arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
poincare_distance (of_complex x) (of_complex w') = arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
arcosh (((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2) + 2 * (cmod (x - w'))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2))) \<le> arcosh (((1 + (cmod x)\<^sup>2) * (1 + (cmod w')\<^sup>2) + 4 * cmod x * cmod w') / ((1 - (cmod x)\<^sup>2) * (1 - (cmod w')\<^sup>2)))
of_complex x \<in> unit_disc
w \<in> unit_disc
w = of_complex w'

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (of_complex x) w \<le> poincare_distance (of_complex x) 0\<^sub>h + poincare_distance 0\<^sub>h w

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

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
[PROOF STEP]
fix M u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
[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 (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
[PROOF STEP]
assume **: "?P (moebius_pt M u) (moebius_pt M v)"
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance (moebius_pt M v) w \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) w

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

goal (1 subgoal):
 1. \<And>w. w \<in> unit_disc \<Longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
[PROOF STEP]
thus "?P' v u w"
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance v w \<le> poincare_distance v u + poincare_distance u w
[PROOF STEP]
using * **[rule_format, of "moebius_pt M w"]
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
moebius_pt M w \<in> unit_disc \<Longrightarrow> poincare_distance (moebius_pt M v) (moebius_pt M w) \<le> poincare_distance (moebius_pt M v) (moebius_pt M u) + poincare_distance (moebius_pt M u) (moebius_pt M w)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance v w \<le> poincare_distance v u + poincare_distance u w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance u w \<le> poincare_distance u v + poincare_distance v w

goal (1 subgoal):
 1. poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance u w \<le> poincare_distance u v + poincare_distance v w

goal (1 subgoal):
 1. poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<in> unit_disc \<longrightarrow> poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance u w \<le> poincare_distance u v + poincare_distance v w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_distance u w \<le> poincare_distance u v + poincare_distance v w

goal:
No subgoals!
[PROOF STEP]
qed