[STATEMENT]
lemma diff_apply_chart:
  "diff k (charts_submanifold (domain \<psi>)) charts_eucl \<psi>" if "\<psi> \<in> atlas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff k (charts_submanifold (domain \<psi>)) charts_eucl (apply_chart \<psi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff k (charts_submanifold (domain \<psi>)) charts_eucl (apply_chart \<psi>)
[PROOF STEP]
interpret submanifold charts k "domain \<psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submanifold charts k (domain \<psi>)
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff k (charts_submanifold (domain \<psi>)) charts_eucl (apply_chart \<psi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff k (charts_submanifold (domain \<psi>)) charts_eucl (apply_chart \<psi>)
[PROOF STEP]
proof (unfold_locales)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sub.carrier \<Longrightarrow> \<exists>c1\<in>sub.atlas. \<exists>c2\<in>manifold_eucl.dest.atlas. x \<in> domain c1 \<and> apply_chart \<psi> ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> apply_chart \<psi> \<circ> inv_chart c1)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sub.carrier \<Longrightarrow> \<exists>c1\<in>sub.atlas. \<exists>c2\<in>manifold_eucl.dest.atlas. x \<in> domain c1 \<and> apply_chart \<psi> ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> apply_chart \<psi> \<circ> inv_chart c1)
[PROOF STEP]
assume x: "x \<in> sub.carrier"
[PROOF STATE]
proof (state)
this:
x \<in> sub.carrier

goal (1 subgoal):
 1. \<And>x. x \<in> sub.carrier \<Longrightarrow> \<exists>c1\<in>sub.atlas. \<exists>c2\<in>manifold_eucl.dest.atlas. x \<in> domain c1 \<and> apply_chart \<psi> ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> apply_chart \<psi> \<circ> inv_chart c1)
[PROOF STEP]
show "\<exists>c1\<in>sub.atlas.
            \<exists>c2\<in>manifold_eucl.dest.atlas.
               x \<in> domain c1 \<and> \<psi> ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (c2 \<circ> \<psi> \<circ> inv_chart c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c1\<in>sub.atlas. \<exists>c2\<in>manifold_eucl.dest.atlas. x \<in> domain c1 \<and> apply_chart \<psi> ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> apply_chart \<psi> \<circ> inv_chart c1)
[PROOF STEP]
apply (rule bexI[where x = "restrict_chart (domain \<psi>) \<psi>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>c2\<in>manifold_eucl.dest.atlas. x \<in> domain (restrict_chart (domain \<psi>) \<psi>) \<and> apply_chart \<psi> ` domain (restrict_chart (domain \<psi>) \<psi>) \<subseteq> domain c2 \<and> k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart c2 \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))
 2. restrict_chart (domain \<psi>) \<psi> \<in> sub.atlas
[PROOF STEP]
apply (rule bexI[where x = "chart_eucl"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x \<in> domain (restrict_chart (domain \<psi>) \<psi>) \<and> apply_chart \<psi> ` domain (restrict_chart (domain \<psi>) \<psi>) \<subseteq> domain chart_eucl \<and> k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart chart_eucl \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))
 2. chart_eucl \<in> manifold_eucl.dest.atlas
 3. restrict_chart (domain \<psi>) \<psi> \<in> sub.atlas
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> domain (restrict_chart (domain \<psi>) \<psi>) \<and> apply_chart \<psi> ` domain (restrict_chart (domain \<psi>) \<psi>) \<subseteq> domain chart_eucl \<and> k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart chart_eucl \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x \<in> domain (restrict_chart (domain \<psi>) \<psi>)
 2. \<And>x xa. xa \<in> domain (restrict_chart (domain \<psi>) \<psi>) \<Longrightarrow> apply_chart \<psi> xa \<in> domain chart_eucl
 3. k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart chart_eucl \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))
[PROOF STEP]
show "x \<in> domain (restrict_chart (domain \<psi>) \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> domain (restrict_chart (domain \<psi>) \<psi>)
[PROOF STEP]
using x \<open>\<psi> \<in> atlas\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> sub.carrier
\<psi> \<in> atlas

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

goal (2 subgoals):
 1. \<And>x xa. xa \<in> domain (restrict_chart (domain \<psi>) \<psi>) \<Longrightarrow> apply_chart \<psi> xa \<in> domain chart_eucl
 2. k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart chart_eucl \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))
[PROOF STEP]
show "k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (chart_eucl \<circ> \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart chart_eucl \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))
[PROOF STEP]
apply (auto simp: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (codomain \<psi> \<inter> inv_chart \<psi> -` domain \<psi>) (\<lambda>x. apply_chart \<psi> (inv_chart \<psi> x))
[PROOF STEP]
apply (rule smooth_on_cong[where g="\<lambda>x. x"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. k-smooth_on (codomain \<psi> \<inter> inv_chart \<psi> -` domain \<psi>) (\<lambda>x. x)
 2. open (codomain \<psi> \<inter> inv_chart \<psi> -` domain \<psi>)
 3. \<And>x. x \<in> codomain \<psi> \<inter> inv_chart \<psi> -` domain \<psi> \<Longrightarrow> apply_chart \<psi> (inv_chart \<psi> x) = x
[PROOF STEP]
by (auto intro!: open_continuous_vimage' continuous_on_codomain)
[PROOF STATE]
proof (state)
this:
k-smooth_on (codomain (restrict_chart (domain \<psi>) \<psi>)) (apply_chart chart_eucl \<circ> apply_chart \<psi> \<circ> inv_chart (restrict_chart (domain \<psi>) \<psi>))

goal (1 subgoal):
 1. \<And>x xa. xa \<in> domain (restrict_chart (domain \<psi>) \<psi>) \<Longrightarrow> apply_chart \<psi> xa \<in> domain chart_eucl
[PROOF STEP]
qed simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. chart_eucl \<in> manifold_eucl.dest.atlas
 2. restrict_chart (domain \<psi>) \<psi> \<in> sub.atlas
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chart_eucl \<in> manifold_eucl.dest.atlas
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart (domain \<psi>) \<psi> \<in> sub.atlas
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart (domain \<psi>) \<psi> \<in> sub.atlas
[PROOF STEP]
by (rule submanifold_atlasI) fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>c1\<in>sub.atlas. \<exists>c2\<in>manifold_eucl.dest.atlas. x \<in> domain c1 \<and> apply_chart \<psi> ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> apply_chart \<psi> \<circ> inv_chart c1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
diff k (charts_submanifold (domain \<psi>)) charts_eucl (apply_chart \<psi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_inv_chart:
  "diff k (manifold_eucl.charts_submanifold (codomain c)) charts (inv_chart c)" if "c \<in> atlas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff k (manifold_eucl.dest.charts_submanifold (codomain c)) charts (inv_chart c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff k (manifold_eucl.dest.charts_submanifold (codomain c)) charts (inv_chart c)
[PROOF STEP]
interpret submanifold charts_eucl k "codomain c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submanifold charts_eucl k (codomain c)
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff k (manifold_eucl.dest.charts_submanifold (codomain c)) charts (inv_chart c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff k (manifold_eucl.dest.charts_submanifold (codomain c)) charts (inv_chart c)
[PROOF STEP]
proof (unfold_locales)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sub.carrier \<Longrightarrow> \<exists>c1\<in>sub.atlas. \<exists>c2\<in>atlas. x \<in> domain c1 \<and> inv_chart c ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> inv_chart c \<circ> inv_chart c1)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sub.carrier \<Longrightarrow> \<exists>c1\<in>sub.atlas. \<exists>c2\<in>atlas. x \<in> domain c1 \<and> inv_chart c ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> inv_chart c \<circ> inv_chart c1)
[PROOF STEP]
assume x: "x \<in> sub.carrier"
[PROOF STATE]
proof (state)
this:
x \<in> sub.carrier

goal (1 subgoal):
 1. \<And>x. x \<in> sub.carrier \<Longrightarrow> \<exists>c1\<in>sub.atlas. \<exists>c2\<in>atlas. x \<in> domain c1 \<and> inv_chart c ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> inv_chart c \<circ> inv_chart c1)
[PROOF STEP]
show "\<exists>c1\<in>sub.atlas.
            \<exists>c2\<in>atlas.
               x \<in> domain c1 \<and> inv_chart c ` domain c1 \<subseteq> domain c2 \<and>
               k-smooth_on (codomain c1) (c2 \<circ> inv_chart c \<circ> inv_chart c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c1\<in>sub.atlas. \<exists>c2\<in>atlas. x \<in> domain c1 \<and> inv_chart c ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> inv_chart c \<circ> inv_chart c1)
[PROOF STEP]
apply (rule bexI[where x = "restrict_chart (codomain c) chart_eucl"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>c2\<in>atlas. x \<in> domain (restrict_chart (codomain c) chart_eucl) \<and> inv_chart c ` domain (restrict_chart (codomain c) chart_eucl) \<subseteq> domain c2 \<and> k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c2 \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))
 2. restrict_chart (codomain c) chart_eucl \<in> sub.atlas
[PROOF STEP]
apply (rule bexI[where x = c])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x \<in> domain (restrict_chart (codomain c) chart_eucl) \<and> inv_chart c ` domain (restrict_chart (codomain c) chart_eucl) \<subseteq> domain c \<and> k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))
 2. c \<in> atlas
 3. restrict_chart (codomain c) chart_eucl \<in> sub.atlas
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> domain (restrict_chart (codomain c) chart_eucl) \<and> inv_chart c ` domain (restrict_chart (codomain c) chart_eucl) \<subseteq> domain c \<and> k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x \<in> domain (restrict_chart (codomain c) chart_eucl)
 2. \<And>x xa. xa \<in> domain (restrict_chart (codomain c) chart_eucl) \<Longrightarrow> inv_chart c xa \<in> domain c
 3. k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))
[PROOF STEP]
show "x \<in> domain (restrict_chart (codomain c) chart_eucl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> domain (restrict_chart (codomain c) chart_eucl)
[PROOF STEP]
using x \<open>c \<in> atlas\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> sub.carrier
c \<in> atlas

goal (1 subgoal):
 1. x \<in> domain (restrict_chart (codomain c) chart_eucl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> domain (restrict_chart (codomain c) chart_eucl)

goal (2 subgoals):
 1. \<And>x xa. xa \<in> domain (restrict_chart (codomain c) chart_eucl) \<Longrightarrow> inv_chart c xa \<in> domain c
 2. k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))
[PROOF STEP]
show "k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))
[PROOF STEP]
apply (auto simp: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (codomain c) (\<lambda>x. apply_chart c (inv_chart c x))
[PROOF STEP]
apply (rule smooth_on_cong[where g="\<lambda>x. x"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. k-smooth_on (codomain c) (\<lambda>x. x)
 2. open (codomain c)
 3. \<And>x. x \<in> codomain c \<Longrightarrow> apply_chart c (inv_chart c x) = x
[PROOF STEP]
by (auto intro!: open_continuous_vimage' continuous_on_codomain)
[PROOF STATE]
proof (state)
this:
k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (apply_chart c \<circ> inv_chart c \<circ> inv_chart (restrict_chart (codomain c) chart_eucl))

goal (1 subgoal):
 1. \<And>x xa. xa \<in> domain (restrict_chart (codomain c) chart_eucl) \<Longrightarrow> inv_chart c xa \<in> domain c
[PROOF STEP]
qed simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c \<in> atlas
 2. restrict_chart (codomain c) chart_eucl \<in> sub.atlas
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> atlas
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
c \<in> atlas

goal (1 subgoal):
 1. c \<in> atlas
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart (codomain c) chart_eucl \<in> sub.atlas
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_chart (codomain c) chart_eucl \<in> sub.atlas
[PROOF STEP]
by (rule submanifold_atlasI) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>c1\<in>sub.atlas. \<exists>c2\<in>atlas. x \<in> domain c1 \<and> inv_chart c ` domain c1 \<subseteq> domain c2 \<and> k-smooth_on (codomain c1) (apply_chart c2 \<circ> inv_chart c \<circ> inv_chart c1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
diff k (manifold_eucl.dest.charts_submanifold (codomain c)) charts (inv_chart c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chart_inj_on [simp]:
  fixes c :: "('a, 'b) chart"
  assumes "x \<in> domain c" "y \<in> domain c"
  shows "c x = c y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (apply_chart c x = apply_chart c y) = (x = y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (apply_chart c x = apply_chart c y) = (x = y)
[PROOF STEP]
have "inj_on c (domain c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (apply_chart c) (domain c)
[PROOF STEP]
by (rule inj_on_apply_chart)
[PROOF STATE]
proof (state)
this:
inj_on (apply_chart c) (domain c)

goal (1 subgoal):
 1. (apply_chart c x = apply_chart c y) = (x = y)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> domain c
y \<in> domain c
inj_on (apply_chart c) (domain c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> domain c
y \<in> domain c
inj_on (apply_chart c) (domain c)

goal (1 subgoal):
 1. (apply_chart c x = apply_chart c y) = (x = y)
[PROOF STEP]
by (auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
(apply_chart c x = apply_chart c y) = (x = y)

goal:
No subgoals!
[PROOF STEP]
qed