[STATEMENT]
lemma reguler_refinementE:
  fixes \<X>::"'i \<Rightarrow> 'a set"
  assumes cover: "carrier \<subseteq> (\<Union>i\<in>I. \<X> i)" and open_cover: "\<And>i. i \<in> I \<Longrightarrow> open (\<X> i)"
  obtains N::"nat set" and \<psi>::"nat \<Rightarrow> ('a, 'b) chart"
  where "\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas" "(domain o \<psi>) ` N refines \<X> ` I" "regular_cover N \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from precompact_locally_finite_open_coverE
[PROOF STATE]
proof (chain)
picking this:
(\<And>W. \<lbrakk>carrier = \<Union> (range W); \<And>i. open (W i); \<And>i. compact (closure (W i)); \<And>i. closure (W i) \<subseteq> carrier; locally_finite_on carrier UNIV W\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain V::"nat\<Rightarrow>_" where V:
    "carrier = (\<Union>i. V i)"
    "\<And>i. open (V i)"
    "\<And>i. compact (closure (V i))"
    "\<And>i. closure (V i) \<subseteq> carrier"
    "locally_finite_on carrier UNIV V"
[PROOF STATE]
proof (prove)
using this:
(\<And>W. \<lbrakk>carrier = \<Union> (range W); \<And>i. open (W i); \<And>i. compact (closure (W i)); \<And>i. closure (W i) \<subseteq> carrier; locally_finite_on carrier UNIV W\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>V. \<lbrakk>carrier = \<Union> (range V); \<And>i. open (V i); \<And>i. compact (closure (V i)); \<And>i. closure (V i) \<subseteq> carrier; locally_finite_on carrier UNIV V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
carrier = \<Union> (range V)
open (V ?i2)
compact (closure (V ?i2))
closure (V ?i2) \<subseteq> carrier
locally_finite_on carrier UNIV V

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define intersecting where "intersecting v = {i. V i \<inter> v \<noteq> {}}" for v
[PROOF STATE]
proof (state)
this:
intersecting ?v = {i. V i \<inter> ?v \<noteq> {}}

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have intersecting_closure: "intersecting (closure x) = intersecting x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersecting (closure x) = intersecting x
[PROOF STEP]
using open_Int_closure_eq_empty[OF V(2), of _ x]
[PROOF STATE]
proof (prove)
using this:
(V ?i3 \<inter> closure x = {}) = (V ?i3 \<inter> x = {})

goal (1 subgoal):
 1. intersecting (closure x) = intersecting x
[PROOF STEP]
by (auto simp: intersecting_def)
[PROOF STATE]
proof (state)
this:
intersecting (closure ?x2) = intersecting ?x2

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from locally_finite_compactD[OF V(5) V(3) V(4)]
[PROOF STATE]
proof (chain)
picking this:
finite {i \<in> UNIV. V i \<inter> closure (V ?i3) \<noteq> {}}
[PROOF STEP]
have "finite (intersecting (closure (V x)))" for x
[PROOF STATE]
proof (prove)
using this:
finite {i \<in> UNIV. V i \<inter> closure (V ?i3) \<noteq> {}}

goal (1 subgoal):
 1. finite (intersecting (closure (V x)))
[PROOF STEP]
by (simp add: intersecting_def)
[PROOF STATE]
proof (state)
this:
finite (intersecting (closure (V ?x2)))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (intersecting (closure (V ?x2)))
[PROOF STEP]
have finite_intersecting: "finite (intersecting (V x))" for x
[PROOF STATE]
proof (prove)
using this:
finite (intersecting (closure (V ?x2)))

goal (1 subgoal):
 1. finite (intersecting (V x))
[PROOF STEP]
by (simp add: intersecting_closure)
[PROOF STATE]
proof (state)
this:
finite (intersecting (V ?x2))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists>\<psi>::('a, 'b) chart.
    \<psi> \<in> atlas \<and>
    codomain \<psi> = ball 0 3 \<and>
    (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and>
     (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and>
      p \<in> domain \<psi> \<and>
      \<psi> p = 0"
    if "p \<in> carrier" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
from cover that open_cover
[PROOF STATE]
proof (chain)
picking this:
carrier \<subseteq> \<Union> (\<X> ` I)
p \<in> carrier
?i2 \<in> I \<Longrightarrow> open (\<X> ?i2)
[PROOF STEP]
obtain c where c: "p \<in> \<X> c" "open (\<X> c)" "c \<in> I"
[PROOF STATE]
proof (prove)
using this:
carrier \<subseteq> \<Union> (\<X> ` I)
p \<in> carrier
?i2 \<in> I \<Longrightarrow> open (\<X> ?i2)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>p \<in> \<X> c; open (\<X> c); c \<in> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
p \<in> \<X> c
open (\<X> c)
c \<in> I

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
define VS where "VS = {U. p \<in> V U}"
[PROOF STATE]
proof (state)
this:
VS = {U. p \<in> V U}

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have open_VS: "\<And>T. T \<in> VS \<Longrightarrow> open (V T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. T \<in> VS \<Longrightarrow> open (V T)
[PROOF STEP]
by (auto simp: VS_def V)
[PROOF STATE]
proof (state)
this:
?T2 \<in> VS \<Longrightarrow> open (V ?T2)

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
from locally_finite_onD[OF V(5) that]
[PROOF STATE]
proof (chain)
picking this:
finite {i \<in> UNIV. p \<in> V i}
[PROOF STEP]
have "finite VS"
[PROOF STATE]
proof (prove)
using this:
finite {i \<in> UNIV. p \<in> V i}

goal (1 subgoal):
 1. finite VS
[PROOF STEP]
by (simp add: VS_def)
[PROOF STATE]
proof (state)
this:
finite VS

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
from atlasE[OF that]
[PROOF STATE]
proof (chain)
picking this:
(\<And>c. \<lbrakk>c \<in> atlas; p \<in> domain c\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<psi>' where \<psi>': "\<psi>' \<in> atlas" "p \<in> domain \<psi>'"
[PROOF STATE]
proof (prove)
using this:
(\<And>c. \<lbrakk>c \<in> atlas; p \<in> domain c\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<psi>'. \<lbrakk>\<psi>' \<in> atlas; p \<in> domain \<psi>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<psi>' \<in> atlas
p \<in> domain \<psi>'

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
define W where  "W = (\<Inter>i\<in>VS. V i) \<inter> domain \<psi>' \<inter> \<X> c"
[PROOF STATE]
proof (state)
this:
W = \<Inter> (V ` VS) \<inter> domain \<psi>' \<inter> \<X> c

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have "open W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open W
[PROOF STEP]
by (force simp: W_def open_VS intro!: c \<open>finite VS\<close>)
[PROOF STATE]
proof (state)
this:
open W

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have "p \<in> W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> W
[PROOF STEP]
by (auto simp: W_def c \<psi>' VS_def)
[PROOF STATE]
proof (state)
this:
p \<in> W

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have "W \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W \<subseteq> carrier
[PROOF STEP]
using \<psi>'
[PROOF STATE]
proof (prove)
using this:
\<psi>' \<in> atlas
p \<in> domain \<psi>'

goal (1 subgoal):
 1. W \<subseteq> carrier
[PROOF STEP]
by (auto simp: W_def)
[PROOF STATE]
proof (state)
this:
W \<subseteq> carrier

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have "0 < (3::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < 3

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
from open_centered_ball_chartE[OF \<open>p \<in> W\<close> \<open>open W\<close> \<open>W \<subseteq> carrier\<close> \<open>0 < 3\<close>]
[PROOF STATE]
proof (chain)
picking this:
(\<And>c. \<lbrakk>c \<in> atlas; p \<in> domain c; apply_chart c p = ?x0.0; domain c \<subseteq> W; codomain c = ball ?x0.0 3\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<psi> where \<psi>: "\<psi> \<in> atlas" "p \<in> domain \<psi>" "\<psi> p = 0" "domain \<psi> \<subseteq> W" "codomain \<psi> = ball 0 3"
[PROOF STATE]
proof (prove)
using this:
(\<And>c. \<lbrakk>c \<in> atlas; p \<in> domain c; apply_chart c p = ?x0.0; domain c \<subseteq> W; codomain c = ball ?x0.0 3\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>\<psi> \<in> atlas; p \<in> domain \<psi>; apply_chart \<psi> p = (0::'b); domain \<psi> \<subseteq> W; codomain \<psi> = ball (0::'b) 3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<psi> \<in> atlas
p \<in> domain \<psi>
apply_chart \<psi> p = (0::'b)
domain \<psi> \<subseteq> W
codomain \<psi> = ball (0::'b) 3

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<psi> \<in> atlas
p \<in> domain \<psi>
apply_chart \<psi> p = (0::'b)
domain \<psi> \<subseteq> W
codomain \<psi> = ball (0::'b) 3

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have "\<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x
[PROOF STEP]
using c \<psi>
[PROOF STATE]
proof (prove)
using this:
p \<in> \<X> c
open (\<X> c)
c \<in> I
\<psi> \<in> atlas
p \<in> domain \<psi>
apply_chart \<psi> p = (0::'b)
domain \<psi> \<subseteq> W
codomain \<psi> = ball (0::'b) 3

goal (1 subgoal):
 1. \<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x
[PROOF STEP]
by (auto simp: W_def)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
have "p \<in> V j \<Longrightarrow> domain \<psi> \<subseteq> V j" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> V j \<Longrightarrow> domain \<psi> \<subseteq> V j
[PROOF STEP]
using c \<psi>
[PROOF STATE]
proof (prove)
using this:
p \<in> \<X> c
open (\<X> c)
c \<in> I
\<psi> \<in> atlas
p \<in> domain \<psi>
apply_chart \<psi> p = (0::'b)
domain \<psi> \<subseteq> W
codomain \<psi> = ball (0::'b) 3

goal (1 subgoal):
 1. p \<in> V j \<Longrightarrow> domain \<psi> \<subseteq> V j
[PROOF STEP]
by (auto simp: W_def VS_def)
[PROOF STATE]
proof (state)
this:
p \<in> V ?j2 \<Longrightarrow> domain \<psi> \<subseteq> V ?j2

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<psi> \<in> atlas
p \<in> domain \<psi>
apply_chart \<psi> p = (0::'b)
domain \<psi> \<subseteq> W
codomain \<psi> = ball (0::'b) 3
\<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x
p \<in> V ?j2 \<Longrightarrow> domain \<psi> \<subseteq> V ?j2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<psi> \<in> atlas
p \<in> domain \<psi>
apply_chart \<psi> p = (0::'b)
domain \<psi> \<subseteq> W
codomain \<psi> = ball (0::'b) 3
\<exists>x\<in>I. domain \<psi> \<subseteq> \<X> x
p \<in> V ?j2 \<Longrightarrow> domain \<psi> \<subseteq> V ?j2

goal (1 subgoal):
 1. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)
[PROOF STEP]
by (intro exI[where x=\<psi>]) auto
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p \<in> domain \<psi> \<and> apply_chart \<psi> p = (0::'b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?p2 \<in> carrier \<Longrightarrow> \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. ?p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> ?p2 \<in> domain \<psi> \<and> apply_chart \<psi> ?p2 = (0::'b)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?p2 \<in> carrier \<Longrightarrow> \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. ?p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> ?p2 \<in> domain \<psi> \<and> apply_chart \<psi> ?p2 = (0::'b)
[PROOF STEP]
have "\<forall>p2 \<in> carrier.
    \<exists>\<psi>::('a, 'b) chart. \<psi> \<in> atlas \<and> codomain \<psi> = ball 0 3 \<and>
         (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p2 \<in> domain \<psi> \<and>
         apply_chart \<psi> p2 = 0"
[PROOF STATE]
proof (prove)
using this:
?p2 \<in> carrier \<Longrightarrow> \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. ?p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> ?p2 \<in> domain \<psi> \<and> apply_chart \<psi> ?p2 = (0::'b)

goal (1 subgoal):
 1. \<forall>p2\<in>carrier. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p2 \<in> domain \<psi> \<and> apply_chart \<psi> p2 = (0::'b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p2\<in>carrier. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p2 \<in> domain \<psi> \<and> apply_chart \<psi> p2 = (0::'b)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p2\<in>carrier. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p2 \<in> domain \<psi> \<and> apply_chart \<psi> p2 = (0::'b)
[PROOF STEP]
obtain \<psi>::"'a \<Rightarrow> ('a, 'b) chart" where \<psi>:
    "\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball 0 3"
    "\<And>p. p \<in> carrier \<Longrightarrow> (\<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c)"
    "\<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j"
    "\<And>p j. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p)"
    "\<And>p. p \<in> carrier \<Longrightarrow> (\<psi> p) p = 0"
    "\<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas"
[PROOF STATE]
proof (prove)
using this:
\<forall>p2\<in>carrier. \<exists>\<psi>. \<psi> \<in> atlas \<and> codomain \<psi> = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain \<psi> \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain \<psi> \<subseteq> V j) \<and> p2 \<in> domain \<psi> \<and> apply_chart \<psi> p2 = (0::'b)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p j. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding bchoice_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>p2\<in>carrier. f p2 \<in> atlas \<and> codomain (f p2) = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain (f p2) \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain (f p2) \<subseteq> V j) \<and> p2 \<in> domain (f p2) \<and> apply_chart (f p2) p2 = (0::'b)

goal (1 subgoal):
 1. (\<And>\<psi>. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p j. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<forall>p2\<in>carrier. f p2 \<in> atlas \<and> codomain (f p2) = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain (f p2) \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain (f p2) \<subseteq> V j) \<and> p2 \<in> domain (f p2) \<and> apply_chart (f p2) p2 = (0::'b) \<Longrightarrow> \<exists>\<psi>. (\<forall>p. p \<in> carrier \<longrightarrow> codomain (\<psi> p) = ball (0::'b) 3) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> (\<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c)) \<and> (\<forall>p j. p \<in> V j \<longrightarrow> domain (\<psi> p) \<subseteq> V j) \<and> (\<forall>p j. p \<in> carrier \<longrightarrow> p \<in> domain (\<psi> p)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> apply_chart (\<psi> p) p = (0::'b)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> \<psi> p \<in> atlas)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<forall>p2\<in>carrier. f p2 \<in> atlas \<and> codomain (f p2) = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain (f p2) \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain (f p2) \<subseteq> V j) \<and> p2 \<in> domain (f p2) \<and> apply_chart (f p2) p2 = (0::'b) \<Longrightarrow> \<exists>\<psi>. (\<forall>p. p \<in> carrier \<longrightarrow> codomain (\<psi> p) = ball (0::'b) 3) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> (\<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c)) \<and> (\<forall>p j. p \<in> V j \<longrightarrow> domain (\<psi> p) \<subseteq> V j) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> p \<in> domain (\<psi> p)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> apply_chart (\<psi> p) p = (0::'b)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> \<psi> p \<in> atlas)
[PROOF STEP]
subgoal for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p2\<in>carrier. f p2 \<in> atlas \<and> codomain (f p2) = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain (f p2) \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain (f p2) \<subseteq> V j) \<and> p2 \<in> domain (f p2) \<and> apply_chart (f p2) p2 = (0::'b) \<Longrightarrow> \<exists>\<psi>. (\<forall>p. p \<in> carrier \<longrightarrow> codomain (\<psi> p) = ball (0::'b) 3) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> (\<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c)) \<and> (\<forall>p j. p \<in> V j \<longrightarrow> domain (\<psi> p) \<subseteq> V j) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> p \<in> domain (\<psi> p)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> apply_chart (\<psi> p) p = (0::'b)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> \<psi> p \<in> atlas)
[PROOF STEP]
apply (rule exI[where x=f])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p2\<in>carrier. f p2 \<in> atlas \<and> codomain (f p2) = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain (f p2) \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain (f p2) \<subseteq> V j) \<and> p2 \<in> domain (f p2) \<and> apply_chart (f p2) p2 = (0::'b) \<Longrightarrow> (\<forall>p. p \<in> carrier \<longrightarrow> codomain (f p) = ball (0::'b) 3) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> (\<exists>c\<in>I. domain (f p) \<subseteq> \<X> c)) \<and> (\<forall>p j. p \<in> V j \<longrightarrow> domain (f p) \<subseteq> V j) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> p \<in> domain (f p)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> apply_chart (f p) p = (0::'b)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> f p \<in> atlas)
[PROOF STEP]
using V
[PROOF STATE]
proof (prove)
using this:
carrier = \<Union> (range V)
open (V ?i2)
compact (closure (V ?i2))
closure (V ?i2) \<subseteq> carrier
locally_finite_on carrier UNIV V

goal (1 subgoal):
 1. \<forall>p2\<in>carrier. f p2 \<in> atlas \<and> codomain (f p2) = ball (0::'b) 3 \<and> (\<exists>c\<in>I. domain (f p2) \<subseteq> \<X> c) \<and> (\<forall>j. p2 \<in> V j \<longrightarrow> domain (f p2) \<subseteq> V j) \<and> p2 \<in> domain (f p2) \<and> apply_chart (f p2) p2 = (0::'b) \<Longrightarrow> (\<forall>p. p \<in> carrier \<longrightarrow> codomain (f p) = ball (0::'b) 3) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> (\<exists>c\<in>I. domain (f p) \<subseteq> \<X> c)) \<and> (\<forall>p j. p \<in> V j \<longrightarrow> domain (f p) \<subseteq> V j) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> p \<in> domain (f p)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> apply_chart (f p) p = (0::'b)) \<and> (\<forall>p. p \<in> carrier \<longrightarrow> f p \<in> atlas)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?p3 \<in> carrier \<Longrightarrow> codomain (\<psi> ?p3) = ball (0::'b) 3
?p3 \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> ?p3) \<subseteq> \<X> c
?p3 \<in> V ?j3 \<Longrightarrow> domain (\<psi> ?p3) \<subseteq> V ?j3
?p3 \<in> carrier \<Longrightarrow> ?p3 \<in> domain (\<psi> ?p3)
?p3 \<in> carrier \<Longrightarrow> apply_chart (\<psi> ?p3) ?p3 = (0::'b)
?p3 \<in> carrier \<Longrightarrow> \<psi> ?p3 \<in> atlas

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define U where "U p = inv_chart (\<psi> p) ` ball 0 1" for p
[PROOF STATE]
proof (state)
this:
U ?p = inv_chart (\<psi> ?p) ` ball (0::'b) 1

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have U_open: "open (U p)" if "p \<in> carrier" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (U p)
[PROOF STEP]
using that \<psi>
[PROOF STATE]
proof (prove)
using this:
p \<in> carrier
?p3 \<in> carrier \<Longrightarrow> codomain (\<psi> ?p3) = ball (0::'b) 3
?p3 \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> ?p3) \<subseteq> \<X> c
?p3 \<in> V ?j3 \<Longrightarrow> domain (\<psi> ?p3) \<subseteq> V ?j3
?p3 \<in> carrier \<Longrightarrow> ?p3 \<in> domain (\<psi> ?p3)
?p3 \<in> carrier \<Longrightarrow> apply_chart (\<psi> ?p3) ?p3 = (0::'b)
?p3 \<in> carrier \<Longrightarrow> \<psi> ?p3 \<in> atlas

goal (1 subgoal):
 1. open (U p)
[PROOF STEP]
by (auto simp: U_def)
[PROOF STATE]
proof (state)
this:
?p3 \<in> carrier \<Longrightarrow> open (U ?p3)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have U_subset_domain: "x \<in> U p \<Longrightarrow> x \<in> domain (\<psi> p)" if "p \<in> carrier" for x p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> U p \<Longrightarrow> x \<in> domain (\<psi> p)
[PROOF STEP]
using \<psi>(1) that
[PROOF STATE]
proof (prove)
using this:
?p3 \<in> carrier \<Longrightarrow> codomain (\<psi> ?p3) = ball (0::'b) 3
p \<in> carrier

goal (1 subgoal):
 1. x \<in> U p \<Longrightarrow> x \<in> domain (\<psi> p)
[PROOF STEP]
by (auto simp: U_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p3 \<in> carrier; ?x3 \<in> U ?p3\<rbrakk> \<Longrightarrow> ?x3 \<in> domain (\<psi> ?p3)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists>M. M \<subseteq> closure (V l) \<and> finite M \<and> closure (V l) \<subseteq> \<Union>(U ` M)" for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
have clcover: "closure (V l) \<subseteq> \<Union>(U ` closure (V l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` closure (V l))
[PROOF STEP]
using \<psi>
[PROOF STATE]
proof (prove)
using this:
?p3 \<in> carrier \<Longrightarrow> codomain (\<psi> ?p3) = ball (0::'b) 3
?p3 \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> ?p3) \<subseteq> \<X> c
?p3 \<in> V ?j3 \<Longrightarrow> domain (\<psi> ?p3) \<subseteq> V ?j3
?p3 \<in> carrier \<Longrightarrow> ?p3 \<in> domain (\<psi> ?p3)
?p3 \<in> carrier \<Longrightarrow> apply_chart (\<psi> ?p3) ?p3 = (0::'b)
?p3 \<in> carrier \<Longrightarrow> \<psi> ?p3 \<in> atlas

goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` closure (V l))
[PROOF STEP]
apply (auto simp: U_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>closure (V l). x \<in> inv_chart (\<psi> xa) ` ball (0::'b) 1
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> inv_chart (\<psi> (?x31 x)) ` ball (0::'b) 1
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> ?x31 x \<in> closure (V l)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> ?x31 x \<in> closure (V l)
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> inv_chart (\<psi> (?x31 x)) ` ball (0::'b) 1
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> inv_chart (\<psi> x) ` ball (0::'b) 1
[PROOF STEP]
apply (rule image_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x = inv_chart (\<psi> x) (?x34 x)
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> ?x34 x \<in> ball (0::'b) 1
[PROOF STEP]
apply (rule inv_chart_inverse[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> domain (\<psi> x)
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> apply_chart (\<psi> x) x \<in> ball (0::'b) 1
[PROOF STEP]
apply (rule \<psi>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> carrier
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> apply_chart (\<psi> x) x \<in> ball (0::'b) 1
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> carrier
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> norm (apply_chart (\<psi> x) x) < 1
[PROOF STEP]
using V(4)
[PROOF STATE]
proof (prove)
using this:
closure (V ?i2) \<subseteq> carrier

goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> x \<in> carrier
 2. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> norm (apply_chart (\<psi> x) x) < 1
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>p. p \<in> carrier \<Longrightarrow> codomain (\<psi> p) = ball (0::'b) 3; \<And>p. p \<in> carrier \<Longrightarrow> \<exists>c\<in>I. domain (\<psi> p) \<subseteq> \<X> c; \<And>p j. p \<in> V j \<Longrightarrow> domain (\<psi> p) \<subseteq> V j; \<And>p. p \<in> carrier \<Longrightarrow> p \<in> domain (\<psi> p); \<And>p. p \<in> carrier \<Longrightarrow> apply_chart (\<psi> p) p = (0::'b); \<And>p. p \<in> carrier \<Longrightarrow> \<psi> p \<in> atlas; x \<in> closure (V l)\<rbrakk> \<Longrightarrow> norm (apply_chart (\<psi> x) x) < 1
[PROOF STEP]
by (metis V(4) less_irrefl norm_numeral norm_one norm_zero one_less_numeral_iff subsetCE
          zero_less_norm_iff zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
closure (V l) \<subseteq> \<Union> (U ` closure (V l))

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
have "B \<in> U ` closure (V l) \<Longrightarrow> open B" for B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> U ` closure (V l) \<Longrightarrow> open B
[PROOF STEP]
using V(4)
[PROOF STATE]
proof (prove)
using this:
closure (V ?i2) \<subseteq> carrier

goal (1 subgoal):
 1. B \<in> U ` closure (V l) \<Longrightarrow> open B
[PROOF STEP]
by (auto intro!: U_open)
[PROOF STATE]
proof (state)
this:
?B3 \<in> U ` closure (V l) \<Longrightarrow> open ?B3

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
from compactE[OF V(3) clcover this]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>B. B \<in> U ` closure (V l) \<Longrightarrow> B \<in> U ` closure (V l); \<And>\<T>'. \<lbrakk>\<T>' \<subseteq> U ` closure (V l); finite \<T>'; closure (V l) \<subseteq> \<Union> \<T>'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
obtain Um where Um: "Um \<subseteq> U ` closure (V l)" "finite Um" "closure (V l) \<subseteq> \<Union>Um"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>B. B \<in> U ` closure (V l) \<Longrightarrow> B \<in> U ` closure (V l); \<And>\<T>'. \<lbrakk>\<T>' \<subseteq> U ` closure (V l); finite \<T>'; closure (V l) \<subseteq> \<Union> \<T>'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Um. \<lbrakk>Um \<subseteq> U ` closure (V l); finite Um; closure (V l) \<subseteq> \<Union> Um\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Um \<subseteq> U ` closure (V l)
finite Um
closure (V l) \<subseteq> \<Union> Um

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
from Um(1)
[PROOF STATE]
proof (chain)
picking this:
Um \<subseteq> U ` closure (V l)
[PROOF STEP]
have "\<forall>t\<in>Um. \<exists>p\<in>closure (V l). t = U p"
[PROOF STATE]
proof (prove)
using this:
Um \<subseteq> U ` closure (V l)

goal (1 subgoal):
 1. \<forall>t\<in>Um. \<exists>p\<in>closure (V l). t = U p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>Um. \<exists>p\<in>closure (V l). t = U p

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>Um. \<exists>p\<in>closure (V l). t = U p
[PROOF STEP]
obtain p_of where p_of: "\<And>t. t \<in> Um \<Longrightarrow> p_of t \<in> closure (V l)"
      "\<And>t. t \<in> Um \<Longrightarrow> t = U (p_of t)"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>Um. \<exists>p\<in>closure (V l). t = U p

goal (1 subgoal):
 1. (\<And>p_of. \<lbrakk>\<And>t. t \<in> Um \<Longrightarrow> p_of t \<in> closure (V l); \<And>t. t \<in> Um \<Longrightarrow> t = U (p_of t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?t3 \<in> Um \<Longrightarrow> p_of ?t3 \<in> closure (V l)
?t3 \<in> Um \<Longrightarrow> ?t3 = U (p_of ?t3)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
have "p_of ` Um \<subseteq> closure (V l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_of ` Um \<subseteq> closure (V l)
[PROOF STEP]
using p_of
[PROOF STATE]
proof (prove)
using this:
?t3 \<in> Um \<Longrightarrow> p_of ?t3 \<in> closure (V l)
?t3 \<in> Um \<Longrightarrow> ?t3 = U (p_of ?t3)

goal (1 subgoal):
 1. p_of ` Um \<subseteq> closure (V l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p_of ` Um \<subseteq> closure (V l)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p_of ` Um \<subseteq> closure (V l)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
have "finite (p_of ` Um)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (p_of ` Um)
[PROOF STEP]
using \<open>finite Um\<close>
[PROOF STATE]
proof (prove)
using this:
finite Um

goal (1 subgoal):
 1. finite (p_of ` Um)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (p_of ` Um)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (p_of ` Um)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
have "closure (V l) \<subseteq> \<Union>(U ` p_of ` Um)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` p_of ` Um)
[PROOF STEP]
using Um p_of
[PROOF STATE]
proof (prove)
using this:
Um \<subseteq> U ` closure (V l)
finite Um
closure (V l) \<subseteq> \<Union> Um
?t3 \<in> Um \<Longrightarrow> p_of ?t3 \<in> closure (V l)
?t3 \<in> Um \<Longrightarrow> ?t3 = U (p_of ?t3)

goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` p_of ` Um)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closure (V l) \<subseteq> \<Union> (U ` p_of ` Um)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p_of ` Um \<subseteq> closure (V l)
finite (p_of ` Um)
closure (V l) \<subseteq> \<Union> (U ` p_of ` Um)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p_of ` Um \<subseteq> closure (V l)
finite (p_of ` Um)
closure (V l) \<subseteq> \<Union> (U ` p_of ` Um)

goal (1 subgoal):
 1. \<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>M\<subseteq>closure (V l). finite M \<and> closure (V l) \<subseteq> \<Union> (U ` M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>M\<subseteq>closure (V ?l3). finite M \<and> closure (V ?l3) \<subseteq> \<Union> (U ` M)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>M\<subseteq>closure (V ?l3). finite M \<and> closure (V ?l3) \<subseteq> \<Union> (U ` M)
[PROOF STEP]
obtain M' where M': "\<And>l. M' l \<subseteq> closure (V l)" "\<And>l. finite (M' l)" "\<And>l. closure (V l) \<subseteq> \<Union>(U ` M' l)"
[PROOF STATE]
proof (prove)
using this:
\<exists>M\<subseteq>closure (V ?l3). finite M \<and> closure (V ?l3) \<subseteq> \<Union> (U ` M)

goal (1 subgoal):
 1. (\<And>M'. \<lbrakk>\<And>l. M' l \<subseteq> closure (V l); \<And>l. finite (M' l); \<And>l. closure (V l) \<subseteq> \<Union> (U ` M' l)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
M' ?l3 \<subseteq> closure (V ?l3)
finite (M' ?l3)
closure (V ?l3) \<subseteq> \<Union> (U ` M' ?l3)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define M where "M v = M' (LEAST l. V l = v)" for v
[PROOF STATE]
proof (state)
this:
M ?v = M' (LEAST l. V l = ?v)

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have V_Least: "V (LEAST la. V la = V l) = V l" for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V (LEAST la. V la = V l) = V l
[PROOF STEP]
by (rule LeastI_ex) auto
[PROOF STATE]
proof (state)
this:
V (LEAST la. V la = V ?l3) = V ?l3

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have M: "M (V l) \<subseteq> closure (V l)" "finite (M v)" "closure (V l) \<subseteq> \<Union>(U ` M (V l))" for v l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M (V l) \<subseteq> closure (V l) &&& finite (M v) &&& closure (V l) \<subseteq> \<Union> (U ` M (V l))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M (V l) \<subseteq> closure (V l)
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M' (LEAST la. V la = V l) \<subseteq> closure (V l)
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. M' (LEAST la. V la = V l) \<subseteq> ?y
 2. ?y \<subseteq> closure (V l)
[PROOF STEP]
apply (rule M')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V (LEAST la. V la = V l)) \<subseteq> closure (V l)
[PROOF STEP]
by (auto simp: V_Least)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (M v)
 2. closure (V l) \<subseteq> \<Union> (U ` M (V l))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (M v)
[PROOF STEP]
using M'
[PROOF STATE]
proof (prove)
using this:
M' ?l3 \<subseteq> closure (V ?l3)
finite (M' ?l3)
closure (V ?l3) \<subseteq> \<Union> (U ` M' ?l3)

goal (1 subgoal):
 1. finite (M v)
[PROOF STEP]
by (auto simp: M_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` M (V l))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` M (V l))
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V l) \<subseteq> \<Union> (U ` M' (LEAST la. V la = V l))
[PROOF STEP]
apply (subst V_Least[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V (LEAST la. V la = V l)) \<subseteq> \<Union> (U ` M' (LEAST la. V la = V l))
[PROOF STEP]
by (rule M')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
M (V ?l3) \<subseteq> closure (V ?l3)
finite (M ?v3)
closure (V ?l3) \<subseteq> \<Union> (U ` M (V ?l3))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from M(1) V(4)
[PROOF STATE]
proof (chain)
picking this:
M (V ?l3) \<subseteq> closure (V ?l3)
closure (V ?i2) \<subseteq> carrier
[PROOF STEP]
have M_carrier: "x \<in> M (V l) \<Longrightarrow> x \<in> carrier" for x l
[PROOF STATE]
proof (prove)
using this:
M (V ?l3) \<subseteq> closure (V ?l3)
closure (V ?i2) \<subseteq> carrier

goal (1 subgoal):
 1. x \<in> M (V l) \<Longrightarrow> x \<in> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "countable (\<Union>l. M (V l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (\<Union>l. M (V l))
[PROOF STEP]
using M(2)
[PROOF STATE]
proof (prove)
using this:
finite (M ?v3)

goal (1 subgoal):
 1. countable (\<Union>l. M (V l))
[PROOF STEP]
by (auto simp: countable_finite)
[PROOF STATE]
proof (state)
this:
countable (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from countableE_bij[OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>f C. bij_betw f C (\<Union>l. M (V l)) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain m and N::"nat set" where n: "bij_betw m N (\<Union>l. M (V l))"
[PROOF STATE]
proof (prove)
using this:
(\<And>f C. bij_betw f C (\<Union>l. M (V l)) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>m N. bij_betw m N (\<Union>l. M (V l)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
bij_betw m N (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define m' where "m' = the_inv_into N m"
[PROOF STATE]
proof (state)
this:
m' = the_inv_into N m

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have m_inverse[simp]: "\<And>i. i \<in> N \<Longrightarrow> m' (m i) = i"
    and m'_inverse[simp]: "\<And>x l. x \<in> M (V l) \<Longrightarrow> m (m' x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> N \<Longrightarrow> m' (m i) = i) &&& (\<And>x l. x \<in> M (V l) \<Longrightarrow> m (m' x) = x)
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
bij_betw m N (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<And>i. i \<in> N \<Longrightarrow> m' (m i) = i) &&& (\<And>x l. x \<in> M (V l) \<Longrightarrow> m (m' x) = x)
[PROOF STEP]
by (force simp: bij_betw_def m'_def the_inv_into_f_f)+
[PROOF STATE]
proof (state)
this:
?i3 \<in> N \<Longrightarrow> m' (m ?i3) = ?i3
?x3 \<in> M (V ?l3) \<Longrightarrow> m (m' ?x3) = ?x3

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have m_in: "m i \<in> (\<Union>l. M (V l))" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m i \<in> (\<Union>l. M (V l))
[PROOF STEP]
using n that
[PROOF STATE]
proof (prove)
using this:
bij_betw m N (\<Union>l. M (V l))
i \<in> N

goal (1 subgoal):
 1. m i \<in> (\<Union>l. M (V l))
[PROOF STEP]
by (auto dest!: bij_betwE)
[PROOF STATE]
proof (state)
this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have m'_in: "m' x \<in> N" if "x \<in> M (V l)" for x l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' x \<in> N
[PROOF STEP]
using that n
[PROOF STATE]
proof (prove)
using this:
x \<in> M (V l)
bij_betw m N (\<Union>l. M (V l))

goal (1 subgoal):
 1. m' x \<in> N
[PROOF STEP]
by (auto simp: m'_def bij_betw_def intro!: the_inv_into_into)
[PROOF STATE]
proof (state)
this:
?x3 \<in> M (V ?l3) \<Longrightarrow> m' ?x3 \<in> N

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from m_in
[PROOF STATE]
proof (chain)
picking this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))
[PROOF STEP]
have m_in_carrier: "m i \<in> carrier" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. m i \<in> carrier
[PROOF STEP]
using that M_carrier
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))
i \<in> N
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier

goal (1 subgoal):
 1. m i \<in> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> carrier

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> carrier
[PROOF STEP]
have "\<And>i. i \<in> N \<Longrightarrow> \<psi> (m i) \<in> atlas"
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> carrier

goal (1 subgoal):
 1. \<And>i. i \<in> N \<Longrightarrow> \<psi> (m i) \<in> atlas
[PROOF STEP]
by (rule \<psi>(6))
[PROOF STATE]
proof (state)
this:
?i3 \<in> N \<Longrightarrow> \<psi> (m ?i3) \<in> atlas

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i3 \<in> N \<Longrightarrow> \<psi> (m ?i3) \<in> atlas

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(domain o (\<lambda>i. (\<psi> (m i)))) ` N refines \<X> ` I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (domain \<circ> (\<lambda>i. \<psi> (m i))) ` N refines \<X> ` I
[PROOF STEP]
by (auto simp: refines_def dest!: m_in_carrier \<psi>(2))
[PROOF STATE]
proof (state)
this:
(domain \<circ> (\<lambda>i. \<psi> (m i))) ` N refines \<X> ` I

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(domain \<circ> (\<lambda>i. \<psi> (m i))) ` N refines \<X> ` I

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "regular_cover N (\<lambda>i. \<psi> (m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
have "countable N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
countable N

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
countable N

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
have carrier_subset: "carrier \<subseteq> (\<Union>i \<in> N. inv_chart (\<psi> (m i)) ` ball 0 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
unfolding V
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (range V) \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> UNIV; x \<in> V xa\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
fix x i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> UNIV; x \<in> V xa\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
assume "x \<in> V i"
[PROOF STATE]
proof (state)
this:
x \<in> V i

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> UNIV; x \<in> V xa\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
with M
[PROOF STATE]
proof (chain)
picking this:
M (V ?l3) \<subseteq> closure (V ?l3)
finite (M ?v3)
closure (V ?l3) \<subseteq> \<Union> (U ` M (V ?l3))
x \<in> V i
[PROOF STEP]
obtain p where p: "p \<in> M (V i)" "x \<in> U p"
[PROOF STATE]
proof (prove)
using this:
M (V ?l3) \<subseteq> closure (V ?l3)
finite (M ?v3)
closure (V ?l3) \<subseteq> \<Union> (U ` M (V ?l3))
x \<in> V i

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> M (V i); x \<in> U p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> M (V i)
x \<in> U p

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> UNIV; x \<in> V xa\<rbrakk> \<Longrightarrow> x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<in> M (V i)
x \<in> U p
[PROOF STEP]
show "x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball 0 1)"
[PROOF STATE]
proof (prove)
using this:
p \<in> M (V i)
x \<in> U p

goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
by (auto simp: U_def intro!: bexI[where x="m' p"] m'_in)
[PROOF STATE]
proof (state)
this:
x \<in> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
have carrier_eq_W:  "carrier = (\<Union>i\<in>N. domain (\<psi> (m i)))" (is "_ = ?W")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier = (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
 2. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
note carrier_subset
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)

goal (2 subgoals):
 1. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
 2. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)

goal (2 subgoals):
 1. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
 2. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
have "\<dots> \<subseteq> ?W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
using U_subset_domain \<psi>(1) M_carrier m_in
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p3 \<in> carrier; ?x3 \<in> U ?p3\<rbrakk> \<Longrightarrow> ?x3 \<in> domain (\<psi> ?p3)
?p3 \<in> carrier \<Longrightarrow> codomain (\<psi> ?p3) = ball (0::'b) 3
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
by (force simp: V)
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))

goal (2 subgoals):
 1. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
 2. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
show "carrier \<subseteq> ?W"
[PROOF STATE]
proof (prove)
using this:
carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))

goal (1 subgoal):
 1. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))

goal (1 subgoal):
 1. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
show "?W \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
using M_carrier \<psi>(6)
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier
?p3 \<in> carrier \<Longrightarrow> \<psi> ?p3 \<in> atlas

goal (1 subgoal):
 1. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier
[PROOF STEP]
by (auto dest!: m_in)
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> carrier

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
carrier = (\<Union>i\<in>N. domain (\<psi> (m i)))

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
carrier = (\<Union>i\<in>N. domain (\<psi> (m i)))

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
have "locally_finite_on carrier N (\<lambda>i. domain (\<psi> (m i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locally_finite_on carrier N (\<lambda>i. domain (\<psi> (m i)))
[PROOF STEP]
proof (rule locally_finite_on_open_coverI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
 2. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
 3. \<And>i. i \<in> N \<Longrightarrow> open (domain (\<psi> (m i)))
[PROOF STEP]
show "open (domain (\<psi> (m i)))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (domain (\<psi> (m i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (domain (\<psi> (m ?i3)))

goal (2 subgoals):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
 2. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
show "carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
unfolding carrier_eq_W
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>N. domain (\<psi> (m i))) \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> (\<Union>i\<in>N. domain (\<psi> (m i)))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
fix ki
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
assume "ki \<in> N"
[PROOF STATE]
proof (state)
this:
ki \<in> N

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
from m_in[OF this]
[PROOF STATE]
proof (chain)
picking this:
m ki \<in> (\<Union>l. M (V l))
[PROOF STEP]
obtain k where k: "m ki \<in> M (V k)"
[PROOF STATE]
proof (prove)
using this:
m ki \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<And>k. m ki \<in> M (V k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m ki \<in> M (V k)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have pkc: "m ki \<in> closure (V k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m ki \<in> closure (V k)
[PROOF STEP]
using k M(1)
[PROOF STATE]
proof (prove)
using this:
m ki \<in> M (V k)
M (V ?l3) \<subseteq> closure (V ?l3)

goal (1 subgoal):
 1. m ki \<in> closure (V k)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
m ki \<in> closure (V k)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
obtain j where j: "m ki \<in> V j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. m ki \<in> V j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M_carrier[of "m ki" k] V(1) k
[PROOF STATE]
proof (prove)
using this:
m ki \<in> M (V k) \<Longrightarrow> m ki \<in> carrier
carrier = \<Union> (range V)
m ki \<in> M (V k)

goal (1 subgoal):
 1. (\<And>j. m ki \<in> V j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
m ki \<in> V j

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have kj: "V k \<inter> V j \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V k \<inter> V j \<noteq> {}
[PROOF STEP]
using open_Int_closure_eq_empty[OF V(2)]
[PROOF STATE]
proof (prove)
using this:
(V ?i3 \<inter> closure ?T = {}) = (V ?i3 \<inter> ?T = {})

goal (1 subgoal):
 1. V k \<inter> V j \<noteq> {}
[PROOF STEP]
using pkc j
[PROOF STATE]
proof (prove)
using this:
(V ?i3 \<inter> closure ?T = {}) = (V ?i3 \<inter> ?T = {})
m ki \<in> closure (V k)
m ki \<in> V j

goal (1 subgoal):
 1. V k \<inter> V j \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V k \<inter> V j \<noteq> {}

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V k \<inter> V j \<noteq> {}
[PROOF STEP]
have jinterk: "j \<in> intersecting (V k)"
[PROOF STATE]
proof (prove)
using this:
V k \<inter> V j \<noteq> {}

goal (1 subgoal):
 1. j \<in> intersecting (V k)
[PROOF STEP]
by (auto simp: intersecting_def)
[PROOF STATE]
proof (state)
this:
j \<in> intersecting (V k)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have 1: "compact (closure (V k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact (closure (V k))
[PROOF STEP]
by (rule V)
[PROOF STATE]
proof (state)
this:
compact (closure (V k))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have 2: "closure (V k) \<subseteq> \<Union>(range V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V k) \<subseteq> \<Union> (range V)
[PROOF STEP]
unfolding V(1)[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V k) \<subseteq> carrier
[PROOF STEP]
by (rule V)
[PROOF STATE]
proof (state)
this:
closure (V k) \<subseteq> \<Union> (range V)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have 3: "B \<in> range V \<Longrightarrow> open B" for B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> range V \<Longrightarrow> open B
[PROOF STEP]
by (auto simp: V)
[PROOF STATE]
proof (state)
this:
?B3 \<in> range V \<Longrightarrow> open ?B3

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
from compactE[OF 1 2 3]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>B. B \<in> range V \<Longrightarrow> B \<in> range V; \<And>\<T>'. \<lbrakk>\<T>' \<subseteq> range V; finite \<T>'; closure (V k) \<subseteq> \<Union> \<T>'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
obtain Vj where "Vj \<subseteq> range V" "finite Vj" "closure (V k) \<subseteq> \<Union>Vj"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>B. B \<in> range V \<Longrightarrow> B \<in> range V; \<And>\<T>'. \<lbrakk>\<T>' \<subseteq> range V; finite \<T>'; closure (V k) \<subseteq> \<Union> \<T>'\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Vj. \<lbrakk>Vj \<subseteq> range V; finite Vj; closure (V k) \<subseteq> \<Union> Vj\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vj \<subseteq> range V
finite Vj
closure (V k) \<subseteq> \<Union> Vj

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Vj \<subseteq> range V
finite Vj
closure (V k) \<subseteq> \<Union> Vj
[PROOF STEP]
obtain J where "finite J" "closure (V k) \<subseteq> \<Union>(V ` J)"
[PROOF STATE]
proof (prove)
using this:
Vj \<subseteq> range V
finite Vj
closure (V k) \<subseteq> \<Union> Vj

goal (1 subgoal):
 1. (\<And>J. \<lbrakk>finite J; closure (V k) \<subseteq> \<Union> (V ` J)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply atomize_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Vj \<subseteq> range V; finite Vj; closure (V k) \<subseteq> \<Union> Vj\<rbrakk> \<Longrightarrow> \<exists>J. finite J \<and> closure (V k) \<subseteq> \<Union> (V ` J)
[PROOF STEP]
by (metis finite_subset_image)
[PROOF STATE]
proof (state)
this:
finite J
closure (V k) \<subseteq> \<Union> (V ` J)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite J
closure (V k) \<subseteq> \<Union> (V ` J)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
fix ki'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
assume "ki' \<in> N"
[PROOF STATE]
proof (state)
this:
ki' \<in> N

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
assume H: "domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}"
[PROOF STATE]
proof (state)
this:
domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
obtain k' where ki': "m ki' \<in> M (V k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. m ki' \<in> M (V k') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using m_in[OF \<open>ki' \<in> N\<close>]
[PROOF STATE]
proof (prove)
using this:
m ki' \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<And>k'. m ki' \<in> M (V k') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m ki' \<in> M (V k')

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have k': "domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}" "m ki' \<in> M (V k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {} &&& m ki' \<in> M (V k')
[PROOF STEP]
using ki'  H
[PROOF STATE]
proof (prove)
using this:
m ki' \<in> M (V k')
domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}

goal (1 subgoal):
 1. domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {} &&& m ki' \<in> M (V k')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}
m ki' \<in> M (V k')

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have pkc': "m ki' \<in> closure (V k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m ki' \<in> closure (V k')
[PROOF STEP]
using k' M(1)
[PROOF STATE]
proof (prove)
using this:
domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}
m ki' \<in> M (V k')
M (V ?l3) \<subseteq> closure (V ?l3)

goal (1 subgoal):
 1. m ki' \<in> closure (V k')
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
m ki' \<in> closure (V k')

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
obtain j' where j': "m ki' \<in> V j'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j'. m ki' \<in> V j' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using M_carrier V(1) k'
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier
carrier = \<Union> (range V)
domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}
m ki' \<in> M (V k')

goal (1 subgoal):
 1. (\<And>j'. m ki' \<in> V j' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
m ki' \<in> V j'

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have kj': "(V k') \<inter> V j' \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V k' \<inter> V j' \<noteq> {}
[PROOF STEP]
using open_Int_closure_eq_empty[OF V(2)]
[PROOF STATE]
proof (prove)
using this:
(V ?i3 \<inter> closure ?T = {}) = (V ?i3 \<inter> ?T = {})

goal (1 subgoal):
 1. V k' \<inter> V j' \<noteq> {}
[PROOF STEP]
using pkc' j'
[PROOF STATE]
proof (prove)
using this:
(V ?i3 \<inter> closure ?T = {}) = (V ?i3 \<inter> ?T = {})
m ki' \<in> closure (V k')
m ki' \<in> V j'

goal (1 subgoal):
 1. V k' \<inter> V j' \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V k' \<inter> V j' \<noteq> {}

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V k' \<inter> V j' \<noteq> {}
[PROOF STEP]
have j'interk': "k' \<in> intersecting (V j')"
[PROOF STATE]
proof (prove)
using this:
V k' \<inter> V j' \<noteq> {}

goal (1 subgoal):
 1. k' \<in> intersecting (V j')
[PROOF STEP]
by (auto simp: intersecting_def)
[PROOF STATE]
proof (state)
this:
k' \<in> intersecting (V j')

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have j'interj: "j' \<in> intersecting (V j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' \<in> intersecting (V j)
[PROOF STEP]
using k' \<psi>(3)[OF j'] \<psi>(3)[OF j]
[PROOF STATE]
proof (prove)
using this:
domain (\<psi> (m ki')) \<inter> domain (\<psi> (m ki)) \<noteq> {}
m ki' \<in> M (V k')
domain (\<psi> (m ki')) \<subseteq> V j'
domain (\<psi> (m ki)) \<subseteq> V j

goal (1 subgoal):
 1. j' \<in> intersecting (V j)
[PROOF STEP]
by (auto simp: intersecting_def)
[PROOF STATE]
proof (state)
this:
j' \<in> intersecting (V j)

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
have "k' \<in> \<Union>(intersecting ` V ` \<Union>(intersecting ` V ` intersecting (V k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' \<in> \<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k)))
[PROOF STEP]
using jinterk j'interk' j'interj
[PROOF STATE]
proof (prove)
using this:
j \<in> intersecting (V k)
k' \<in> intersecting (V j')
j' \<in> intersecting (V j)

goal (1 subgoal):
 1. k' \<in> \<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' \<in> \<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k)))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k' \<in> \<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k)))
[PROOF STEP]
have "m ki' \<in> \<Union>((\<lambda>x. M (V x)) ` \<Union>(intersecting ` V ` \<Union>(intersecting ` V ` intersecting (V k))))"
[PROOF STATE]
proof (prove)
using this:
k' \<in> \<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k)))

goal (1 subgoal):
 1. m ki' \<in> (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))
[PROOF STEP]
using ki'
[PROOF STATE]
proof (prove)
using this:
k' \<in> \<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k)))
m ki' \<in> M (V k')

goal (1 subgoal):
 1. m ki' \<in> (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m ki' \<in> (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
from m_inverse[symmetric] this
[PROOF STATE]
proof (chain)
picking this:
?t \<in> N \<Longrightarrow> ?t = m' (m ?t)
m ki' \<in> (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))
[PROOF STEP]
have "ki' \<in> m' ` \<Union>((\<lambda>x. M (V x)) ` \<Union>(intersecting ` V ` \<Union>(intersecting ` V ` intersecting (V k))))"
[PROOF STATE]
proof (prove)
using this:
?t \<in> N \<Longrightarrow> ?t = m' (m ?t)
m ki' \<in> (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))

goal (1 subgoal):
 1. ki' \<in> m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))
[PROOF STEP]
by (rule image_eqI) fact
[PROOF STATE]
proof (state)
this:
ki' \<in> m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ki'5 \<in> N; domain (\<psi> (m ?ki'5)) \<inter> domain (\<psi> (m ki)) \<noteq> {}\<rbrakk> \<Longrightarrow> ?ki'5 \<in> m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ki'5 \<in> N; domain (\<psi> (m ?ki'5)) \<inter> domain (\<psi> (m ki)) \<noteq> {}\<rbrakk> \<Longrightarrow> ?ki'5 \<in> m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))

goal (1 subgoal):
 1. \<And>j. j \<in> N \<Longrightarrow> finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m j)) \<noteq> {}}
[PROOF STEP]
show "finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m ki)) \<noteq> {}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m ki)) \<noteq> {}}
[PROOF STEP]
apply (rule finite_subset[where B="m' ` \<Union>((\<lambda>x. M (V x)) ` \<Union>(intersecting ` V ` \<Union>(intersecting ` V ` intersecting (V k))))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m ki)) \<noteq> {}} \<subseteq> m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x))
 2. finite (m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x)))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> N; domain (\<psi> (m x)) \<inter> domain (\<psi> (m ki)) \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> m' ` (\<Union>x\<in>intersecting (V k). \<Union>x\<in>intersecting (V x). \<Union>x\<in>intersecting (V x). M (V x))
 2. finite (m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x)))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ \<in> N; domain (\<psi> (m x_)) \<inter> domain (\<psi> (m ki)) \<noteq> {}\<rbrakk> \<Longrightarrow> x_ \<in> m' ` (\<Union>x\<in>intersecting (V k). \<Union>x\<in>intersecting (V x). \<Union>x\<in>intersecting (V x). M (V x))
[PROOF STEP]
by (drule *, assumption, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x)))
[PROOF STEP]
using finite_intersecting intersecting_def M
[PROOF STATE]
proof (prove)
using this:
finite (intersecting (V ?x2))
intersecting ?v = {i. V i \<inter> ?v \<noteq> {}}
M (V ?l3) \<subseteq> closure (V ?l3)
finite (M ?v3)
closure (V ?l3) \<subseteq> \<Union> (U ` M (V ?l3))

goal (1 subgoal):
 1. finite (m' ` (\<Union>x\<in>\<Union> (intersecting ` V ` \<Union> (intersecting ` V ` intersecting (V k))). M (V x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {i \<in> N. domain (\<psi> (m i)) \<inter> domain (\<psi> (m ki)) \<noteq> {}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
locally_finite_on carrier N (\<lambda>i. domain (\<psi> (m i)))

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
locally_finite_on carrier N (\<lambda>i. domain (\<psi> (m i)))

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
have "(\<forall>i \<in> N. codomain (\<psi> (m i)) = ball 0 3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>N. codomain (\<psi> (m i)) = ball (0::'b) 3
[PROOF STEP]
using \<psi>(1) M_carrier m_in
[PROOF STATE]
proof (prove)
using this:
?p3 \<in> carrier \<Longrightarrow> codomain (\<psi> ?p3) = ball (0::'b) 3
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. \<forall>i\<in>N. codomain (\<psi> (m i)) = ball (0::'b) 3
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>N. codomain (\<psi> (m i)) = ball (0::'b) 3

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>N. codomain (\<psi> (m i)) = ball (0::'b) 3

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
have "carrier = (\<Union>i \<in> N. inv_chart (\<psi> (m i)) ` ball 0 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier = (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. carrier \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
 2. (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> carrier
[PROOF STEP]
show "(\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball 0 1) \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> carrier
[PROOF STEP]
using \<psi>(6)[OF M_carrier] M_carrier m_in
[PROOF STATE]
proof (prove)
using this:
?p3 \<in> M (V ?l7) \<Longrightarrow> \<psi> ?p3 \<in> atlas
?x3 \<in> M (V ?l3) \<Longrightarrow> ?x3 \<in> carrier
?i3 \<in> N \<Longrightarrow> m ?i3 \<in> (\<Union>l. M (V l))

goal (1 subgoal):
 1. (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> carrier
[PROOF STEP]
by (force simp: \<psi>(1))
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1) \<subseteq> carrier

goal (1 subgoal):
 1. carrier \<subseteq> (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
qed (rule carrier_subset)
[PROOF STATE]
proof (state)
this:
carrier = (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
countable N
carrier = (\<Union>i\<in>N. domain (\<psi> (m i)))
locally_finite_on carrier N (\<lambda>i. domain (\<psi> (m i)))
\<forall>i\<in>N. codomain (\<psi> (m i)) = ball (0::'b) 3
carrier = (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
countable N
carrier = (\<Union>i\<in>N. domain (\<psi> (m i)))
locally_finite_on carrier N (\<lambda>i. domain (\<psi> (m i)))
\<forall>i\<in>N. codomain (\<psi> (m i)) = ball (0::'b) 3
carrier = (\<Union>i\<in>N. inv_chart (\<psi> (m i)) ` ball (0::'b) 1)

goal (1 subgoal):
 1. regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
by (auto simp: regular_cover_def o_def)
[PROOF STATE]
proof (state)
this:
regular_cover N (\<lambda>i. \<psi> (m i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
regular_cover N (\<lambda>i. \<psi> (m i))

goal (1 subgoal):
 1. (\<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines \<X> ` I; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i3 \<in> N \<Longrightarrow> \<psi> (m ?i3) \<in> atlas
(domain \<circ> (\<lambda>i. \<psi> (m i))) ` N refines \<X> ` I
regular_cover N (\<lambda>i. \<psi> (m i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> N \<Longrightarrow> \<psi> (m ?i3) \<in> atlas
(domain \<circ> (\<lambda>i. \<psi> (m i))) ` N refines \<X> ` I
regular_cover N (\<lambda>i. \<psi> (m i))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed