[STATEMENT]
lemma poincare_collinear3_between:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc" and "w \<in> unit_disc"
  assumes "poincare_collinear {u, v, w}"
  shows "poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w" (is "?P' u v w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
proof (cases "u=v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 2. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 2. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u = v
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
poincare_collinear {u, v, w}

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

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> v

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

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
hence "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
using complex.expand[of x 0]
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1
Re x = Re 0 \<and> Im x = Im 0 \<Longrightarrow> x = 0

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

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
hence *: "poincare_line 0\<^sub>h (of_complex x) = x_axis"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
using x poincare_line_0_real_is_x_axis[of "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
is_real x
0 < Re x
Re x < 1
\<lbrakk>of_complex x \<in> circline_set x_axis; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
is_real x
0 < Re x
Re x < 1
\<lbrakk>of_complex x \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
have "of_complex x \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> unit_disc
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

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

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
have "of_complex x \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h
[PROOF STEP]
using \<open>x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

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

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 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 \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
w \<in> unit_disc

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume "poincare_collinear {0\<^sub>h, of_complex x, w}"
[PROOF STATE]
proof (state)
this:
poincare_collinear {0\<^sub>h, of_complex x, w}

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "w \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
poincare_collinear {0\<^sub>h, of_complex x, w}

goal (1 subgoal):
 1. w \<in> circline_set x_axis
[PROOF STEP]
using * unique_poincare_line[of "0\<^sub>h" "of_complex x"] \<open>of_complex x \<in> unit_disc\<close> \<open>x \<noteq> 0\<close> \<open>of_complex x \<noteq> 0\<^sub>h\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_collinear {0\<^sub>h, of_complex x, w}
poincare_line 0\<^sub>h (of_complex x) = x_axis
\<lbrakk>0\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; 0\<^sub>h \<in> circline_set ?l; of_complex x \<in> circline_set ?l; is_poincare_line ?l\<rbrakk> \<Longrightarrow> ?l = poincare_line 0\<^sub>h (of_complex x)
of_complex x \<in> unit_disc
x \<noteq> 0
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. w \<in> circline_set x_axis
[PROOF STEP]
unfolding poincare_collinear_def
[PROOF STATE]
proof (prove)
using this:
\<exists>p. is_poincare_line p \<and> {0\<^sub>h, of_complex x, w} \<subseteq> circline_set p
poincare_line 0\<^sub>h (of_complex x) = x_axis
\<lbrakk>0\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; 0\<^sub>h \<in> circline_set ?l; of_complex x \<in> circline_set ?l; is_poincare_line ?l\<rbrakk> \<Longrightarrow> ?l = poincare_line 0\<^sub>h (of_complex x)
of_complex x \<in> unit_disc
x \<noteq> 0
of_complex x \<noteq> 0\<^sub>h

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

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> circline_set x_axis
[PROOF STEP]
obtain w' where w': "w = of_complex w'" "is_real w'"
[PROOF STATE]
proof (prove)
using this:
w \<in> circline_set x_axis

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>w = of_complex w'; is_real w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>w \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> circline_set x_axis
w \<in> unit_disc

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

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>w = of_complex w'; is_real w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
w \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
w \<in> unit_disc
w = \<infinity>\<^sub>h \<or> (\<exists>x. w = of_complex x)

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

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "-1 < Re w'" "Re w' < 1"
[PROOF STATE]
proof (prove)
using this:
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. - 1 < Re w' &&& Re w' < 1
[PROOF STEP]
using \<open>w \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
w = of_complex w'
is_real w'
w \<in> unit_disc

goal (1 subgoal):
 1. - 1 < Re w' &&& Re w' < 1
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
- 1 < Re w'
Re w' < 1

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume 1: "\<not> poincare_between (of_complex x) 0\<^sub>h w"
[PROOF STATE]
proof (state)
this:
\<not> poincare_between (of_complex x) 0\<^sub>h w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "w \<noteq> 0\<^sub>h" "w' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w

goal (1 subgoal):
 1. w \<noteq> 0\<^sub>h &&& w' \<noteq> 0
[PROOF STEP]
using w'
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. w \<noteq> 0\<^sub>h &&& w' \<noteq> 0
[PROOF STEP]
unfolding poincare_between_def
[PROOF STATE]
proof (prove)
using this:
\<not> (of_complex x = 0\<^sub>h \<or> 0\<^sub>h = w \<or> (let cr = cross_ratio (of_complex x) 0\<^sub>h w (inversion 0\<^sub>h) in is_real (to_complex cr) \<and> Re (to_complex cr) < 0))
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. w \<noteq> 0\<^sub>h &&& w' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<noteq> 0\<^sub>h
w' \<noteq> 0

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "Re w' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0\<^sub>h
w' \<noteq> 0

goal (1 subgoal):
 1. Re w' \<noteq> 0
[PROOF STEP]
using w' complex.expand[of w' 0]
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0\<^sub>h
w' \<noteq> 0
w = of_complex w'
is_real w'
Re w' = Re 0 \<and> Im w' = Im 0 \<Longrightarrow> w' = 0

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

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
have "Re w' \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re w'
[PROOF STEP]
using 1 poincare_between_x_axis_u0v[of x w'] \<open>Re x > 0\<close> \<open>is_real x\<close> \<open>x \<noteq> 0\<close> \<open>w' \<noteq> 0\<close> w'
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w
\<lbrakk>is_real x; x \<noteq> 0; w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between (of_complex x) 0\<^sub>h (of_complex w') = (is_real w' \<and> Re x * Re w' < 0)
0 < Re x
is_real x
x \<noteq> 0
w' \<noteq> 0
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. 0 \<le> Re w'
[PROOF STEP]
using mult_pos_neg
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w
\<lbrakk>is_real x; x \<noteq> 0; w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between (of_complex x) 0\<^sub>h (of_complex w') = (is_real w' \<and> Re x * Re w' < 0)
0 < Re x
is_real x
x \<noteq> 0
w' \<noteq> 0
w = of_complex w'
is_real w'
\<lbrakk>(0::?'a) < ?a; ?b < (0::?'a)\<rbrakk> \<Longrightarrow> ?a * ?b < (0::?'a)

goal (1 subgoal):
 1. 0 \<le> Re w'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<le> Re w'

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> Re w'

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume "\<not> poincare_between 0\<^sub>h (of_complex x) w"
[PROOF STATE]
proof (state)
this:
\<not> poincare_between 0\<^sub>h (of_complex x) w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "Re w' < Re x"
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between 0\<^sub>h (of_complex x) w

goal (1 subgoal):
 1. Re w' < Re x
[PROOF STEP]
using poincare_between_x_axis_0uv[of "Re x" "Re w'"]
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between 0\<^sub>h (of_complex x) w
\<lbrakk>- 1 < Re x; Re x < 1; Re x \<noteq> 0; - 1 < Re w'; Re w' < 1; Re w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re x))) (of_complex (cor (Re w'))) = (Re x < 0 \<and> Re w' < 0 \<and> Re w' \<le> Re x \<or> 0 < Re x \<and> 0 < Re w' \<and> Re x \<le> Re w')

goal (1 subgoal):
 1. Re w' < Re x
[PROOF STEP]
using w' x \<open>-1 < Re w'\<close> \<open>Re w' < 1\<close> \<open>Re w' \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between 0\<^sub>h (of_complex x) w
\<lbrakk>- 1 < Re x; Re x < 1; Re x \<noteq> 0; - 1 < Re w'; Re w' < 1; Re w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re x))) (of_complex (cor (Re w'))) = (Re x < 0 \<and> Re w' < 0 \<and> Re w' \<le> Re x \<or> 0 < Re x \<and> 0 < Re w' \<and> Re x \<le> Re w')
w = of_complex w'
is_real w'
is_real x
0 < Re x
Re x < 1
- 1 < Re w'
Re w' < 1
Re w' \<noteq> 0

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

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> Re w'
Re w' < Re x
[PROOF STEP]
show "poincare_between 0\<^sub>h w (of_complex x)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re w'
Re w' < Re x

goal (1 subgoal):
 1. poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
using poincare_between_x_axis_0uv[of "Re w'" "Re x"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re w'
Re w' < Re x
\<lbrakk>- 1 < Re w'; Re w' < 1; Re w' \<noteq> 0; - 1 < Re x; Re x < 1; Re x \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re w'))) (of_complex (cor (Re x))) = (Re w' < 0 \<and> Re x < 0 \<and> Re x \<le> Re w' \<or> 0 < Re w' \<and> 0 < Re x \<and> Re w' \<le> Re x)

goal (1 subgoal):
 1. poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
using w' x \<open>-1 < Re w'\<close> \<open>Re w' < 1\<close> \<open>Re w' \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re w'
Re w' < Re x
\<lbrakk>- 1 < Re w'; Re w' < 1; Re w' \<noteq> 0; - 1 < Re x; Re x < 1; Re x \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re w'))) (of_complex (cor (Re x))) = (Re w' < 0 \<and> Re x < 0 \<and> Re x \<le> Re w' \<or> 0 < Re w' \<and> 0 < Re x \<and> Re w' \<le> Re x)
w = of_complex w'
is_real w'
is_real x
0 < Re x
Re x < 1
- 1 < Re w'
Re w' < 1
Re w' \<noteq> 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w

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

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v 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; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v 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; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
assume 1: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
assume 2: "?P ?Mu ?Mv"
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (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; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
show "?P u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {u, v, w}; \<not> poincare_between u v w; \<not> poincare_between v u w\<rbrakk> \<Longrightarrow> poincare_between u w v
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {u, v, w}; \<not> poincare_between u v w; \<not> poincare_between v u w\<rbrakk> \<Longrightarrow> poincare_between u w v
[PROOF STEP]
assume "w \<in> unit_disc" "poincare_collinear {u, v, w}" "\<not> poincare_between u v w" "\<not> poincare_between v u w"
[PROOF STATE]
proof (state)
this:
w \<in> unit_disc
poincare_collinear {u, v, w}
\<not> poincare_between u v w
\<not> poincare_between v u w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {u, v, w}; \<not> poincare_between u v w; \<not> poincare_between v u w\<rbrakk> \<Longrightarrow> poincare_between u w v
[PROOF STEP]
thus "poincare_between u w v"
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
poincare_collinear {u, v, w}
\<not> poincare_between u v w
\<not> poincare_between v u w

goal (1 subgoal):
 1. poincare_between u w v
[PROOF STEP]
using 1 2[rule_format, of "moebius_pt M w"]
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
poincare_collinear {u, v, w}
\<not> poincare_between u v w
\<not> poincare_between v u w
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
moebius_pt M w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, moebius_pt M w} \<Longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) \<or> poincare_between (moebius_pt M u) (moebius_pt M w) (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) (moebius_pt M w)

goal (1 subgoal):
 1. poincare_between u w v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_between u w v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
poincare_collinear {u, v, w}

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

goal:
No subgoals!
[PROOF STEP]
qed