[STATEMENT]
theorem partitions_of_unityE:
  fixes A::"'i set" and X::"'i \<Rightarrow> 'a set"
  assumes "carrier \<subseteq> (\<Union>i\<in>A. X i)"
  assumes "\<And>i. i \<in> A \<Longrightarrow> open (X i)"
  obtains \<phi>::"'i \<Rightarrow> 'a \<Rightarrow> real"
  where "\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i)"
    and "\<And>i x. i \<in> A \<Longrightarrow> x \<in> carrier \<Longrightarrow> 0 \<le> \<phi> i x"
    and "\<And>i x. i \<in> A \<Longrightarrow> x \<in> carrier \<Longrightarrow> \<phi> i x \<le> 1"
    and "\<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i\<in>{i\<in>A. \<phi> i x \<noteq> 0}. \<phi> i x) = 1"
    and "\<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i"
    and "locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from reguler_refinementE[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>i. i \<in> A \<Longrightarrow> i \<in> A; \<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines X ` A; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
obtain N and \<psi>::"nat \<Rightarrow> ('a, 'b) chart" where \<psi>:
    "\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas"
    "(domain o \<psi>) ` N refines X ` A"
    "regular_cover N \<psi>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. i \<in> A \<Longrightarrow> i \<in> A; \<And>N \<psi>. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> \<psi> i \<in> atlas; (domain \<circ> \<psi>) ` N refines X ` A; regular_cover N \<psi>\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define U where "U i = inv_chart (\<psi> i) ` ball 0 1" for i::nat
[PROOF STATE]
proof (state)
this:
U ?i = inv_chart (\<psi> ?i) ` ball (0::'b) 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define V where "V i = inv_chart (\<psi> i) ` ball 0 2" for i::nat
[PROOF STATE]
proof (state)
this:
V ?i = inv_chart (\<psi> ?i) ` ball (0::'b) 2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define W where "W i = inv_chart (\<psi> i) ` ball 0 3" for i::nat
[PROOF STATE]
proof (state)
this:
W ?i = inv_chart (\<psi> ?i) ` ball (0::'b) 3

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>regular_cover N \<psi>\<close>
[PROOF STATE]
proof (chain)
picking this:
regular_cover N \<psi>
[PROOF STEP]
have regular_cover:
    "countable N"
    "(\<Union>i\<in>N. U i) = (\<Union>i\<in>N. domain (\<psi> i))"
    "locally_finite_on carrier N (domain \<circ> \<psi>)"
    "\<And>i. i \<in> N \<Longrightarrow> codomain (\<psi> i) = ball 0 3"
    "carrier = (\<Union>i\<in>N. U i)"
[PROOF STATE]
proof (prove)
using this:
regular_cover N \<psi>

goal (1 subgoal):
 1. (countable N &&& \<Union> (U ` N) = (\<Union>i\<in>N. domain (\<psi> i))) &&& locally_finite_on carrier N (domain \<circ> \<psi>) &&& (\<And>i. i \<in> N \<Longrightarrow> codomain (\<psi> i) = ball (0::'b) 3) &&& carrier = \<Union> (U ` N)
[PROOF STEP]
by (auto simp: regular_cover_def U_def)
[PROOF STATE]
proof (state)
this:
countable N
\<Union> (U ` N) = (\<Union>i\<in>N. domain (\<psi> i))
locally_finite_on carrier N (domain \<circ> \<psi>)
?i2 \<in> N \<Longrightarrow> codomain (\<psi> ?i2) = ball (0::'b) 3
carrier = \<Union> (U ` N)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have open_W: "open (W i)" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (W i)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<in> N

goal (1 subgoal):
 1. open (W i)
[PROOF STEP]
by (auto simp: W_def regular_cover)
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> open (W ?i2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have W_eq: "domain (\<psi> i) = W i" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (\<psi> i) = W i
[PROOF STEP]
using W_def regular_cover(4) that
[PROOF STATE]
proof (prove)
using this:
W ?i = inv_chart (\<psi> ?i) ` ball (0::'b) 3
?i2 \<in> N \<Longrightarrow> codomain (\<psi> ?i2) = ball (0::'b) 3
i \<in> N

goal (1 subgoal):
 1. domain (\<psi> i) = W i
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> domain (\<psi> ?i2) = W ?i2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have carrier_W: "carrier = (\<Union>i\<in>N. W i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier = \<Union> (W ` N)
[PROOF STEP]
by (auto simp: regular_cover W_eq)
[PROOF STATE]
proof (state)
this:
carrier = \<Union> (W ` N)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have V_subset_W: "closure (V i) \<subseteq> W i" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
have "closure (V i) \<subseteq> closure (inv_chart (\<psi> i) ` cball 0 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (V i) \<subseteq> closure (inv_chart (\<psi> i) ` cball (0::'b) 2)
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (inv_chart (\<psi> i) ` ball (0::'b) 2) \<subseteq> closure (inv_chart (\<psi> i) ` cball (0::'b) 2)
[PROOF STEP]
by (rule closure_mono) auto
[PROOF STATE]
proof (state)
this:
closure (V i) \<subseteq> closure (inv_chart (\<psi> i) ` cball (0::'b) 2)

goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
closure (V i) \<subseteq> closure (inv_chart (\<psi> i) ` cball (0::'b) 2)

goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
have "\<dots> = inv_chart (\<psi> i) ` cball 0 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (inv_chart (\<psi> i) ` cball (0::'b) 2) = inv_chart (\<psi> i) ` cball (0::'b) 2
[PROOF STEP]
apply (rule closure_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (inv_chart (\<psi> i) ` cball (0::'b) 2)
[PROOF STEP]
apply (rule compact_imp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact (inv_chart (\<psi> i) ` cball (0::'b) 2)
[PROOF STEP]
apply (rule compact_continuous_image)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on (cball (0::'b) 2) (inv_chart (\<psi> i))
 2. compact (cball (0::'b) 2)
[PROOF STEP]
by (auto intro!: continuous_intros simp: regular_cover that)
[PROOF STATE]
proof (state)
this:
closure (inv_chart (\<psi> i) ` cball (0::'b) 2) = inv_chart (\<psi> i) ` cball (0::'b) 2

goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
closure (inv_chart (\<psi> i) ` cball (0::'b) 2) = inv_chart (\<psi> i) ` cball (0::'b) 2

goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
have "\<dots> \<subseteq> W i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_chart (\<psi> i) ` cball (0::'b) 2 \<subseteq> W i
[PROOF STEP]
by (auto simp: W_def)
[PROOF STATE]
proof (state)
this:
inv_chart (\<psi> i) ` cball (0::'b) 2 \<subseteq> W i

goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
closure (V i) \<subseteq> W i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
closure (V i) \<subseteq> W i

goal (1 subgoal):
 1. closure (V i) \<subseteq> W i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
closure (V i) \<subseteq> W i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> closure (V ?i2) \<subseteq> W ?i2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have carrier_V: "carrier = (\<Union>i\<in>N. V i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier = \<Union> (V ` N)
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. carrier \<subseteq> \<Union> (V ` N)
 2. \<Union> (V ` N) \<subseteq> carrier
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier \<subseteq> \<Union> (V ` N)
[PROOF STEP]
unfolding regular_cover(5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (U ` N) \<subseteq> \<Union> (V ` N)
[PROOF STEP]
by (auto simp: U_def V_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (V ` N) \<subseteq> carrier
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (V ` N) \<subseteq> carrier
[PROOF STEP]
unfolding carrier_W
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (V ` N) \<subseteq> \<Union> (W ` N)
[PROOF STEP]
using V_subset_W
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> closure (V ?i2) \<subseteq> W ?i2

goal (1 subgoal):
 1. \<Union> (V ` N) \<subseteq> \<Union> (W ` N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
carrier = \<Union> (V ` N)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define f where "f i x = (if x \<in> W i then H (\<psi> i x) else 0)" for i x
[PROOF STATE]
proof (state)
this:
f ?i ?x = (if ?x \<in> W ?i then H (apply_chart (\<psi> ?i) ?x) else 0)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have f_simps: "x \<in> W i \<Longrightarrow> f i x = H (\<psi> i x)"
    "x \<notin> W i \<Longrightarrow> f i x = 0"
    for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> W i \<Longrightarrow> f i x = H (apply_chart (\<psi> i) x)) &&& (x \<notin> W i \<Longrightarrow> f i x = 0)
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
?x2 \<in> W ?i2 \<Longrightarrow> f ?i2 ?x2 = H (apply_chart (\<psi> ?i2) ?x2)
?x2 \<notin> W ?i2 \<Longrightarrow> f ?i2 ?x2 = 0

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have f_eq_one: "f j y = 1" if "j \<in> N" "y \<in> U j" for j y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f j y = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f j y = 1
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
j \<in> N
y \<in> U j
[PROOF STEP]
have "y \<in> W j"
[PROOF STATE]
proof (prove)
using this:
j \<in> N
y \<in> U j

goal (1 subgoal):
 1. y \<in> W j
[PROOF STEP]
by (auto simp: U_def W_def)
[PROOF STATE]
proof (state)
this:
y \<in> W j

goal (1 subgoal):
 1. f j y = 1
[PROOF STEP]
from \<open>y \<in> U j\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> U j
[PROOF STEP]
have "norm (\<psi> j y) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
y \<in> U j

goal (1 subgoal):
 1. norm (apply_chart (\<psi> j) y) \<le> 1
[PROOF STEP]
by (auto simp: U_def W_eq[symmetric] \<open>j \<in> N\<close> regular_cover(4))
[PROOF STATE]
proof (state)
this:
norm (apply_chart (\<psi> j) y) \<le> 1

goal (1 subgoal):
 1. f j y = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (apply_chart (\<psi> j) y) \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (apply_chart (\<psi> j) y) \<le> 1

goal (1 subgoal):
 1. f j y = 1
[PROOF STEP]
by (auto simp: f_def \<open>y \<in> W j\<close> intro!: H_eq_one)
[PROOF STATE]
proof (state)
this:
f j y = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j2 \<in> N; ?y2 \<in> U ?j2\<rbrakk> \<Longrightarrow> f ?j2 ?y2 = 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have f_diff: "diff_fun k charts (f i)" if i: "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts (f i)
[PROOF STEP]
proof (rule manifold_eucl.diff_open_Un, unfold diff_fun_def[symmetric])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) (f i)
 2. diff_fun k (charts_submanifold ?V) (f i)
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
note W_eq = W_eq[OF that]
[PROOF STATE]
proof (state)
this:
domain (\<psi> i) = W i

goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) (f i)
 2. diff_fun k (charts_submanifold ?V) (f i)
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
have "W i \<subseteq> carrier"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W i \<subseteq> carrier
[PROOF STEP]
unfolding W_eq[symmetric] regular_cover
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (\<psi> i) \<subseteq> (\<Union>i\<in>N. domain (\<psi> i))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i \<in> N

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

goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) (f i)
 2. diff_fun k (charts_submanifold ?V) (f i)
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
interpret W: submanifold _ _ "W i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submanifold charts k (W i)
[PROOF STEP]
by unfold_locales (auto simp: open_W i)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) (f i)
 2. diff_fun k (charts_submanifold ?V) (f i)
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
have "diff_fun k (charts_submanifold (W i)) (H \<circ> (\<psi> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (W i)) (H \<circ> apply_chart (\<psi> i))
[PROOF STEP]
apply (rule diff_fun_compose[where ?M2.0 = charts_eucl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. diff k (charts_submanifold (W i)) charts_eucl (apply_chart (\<psi> i))
 2. diff_fun k charts_eucl H
[PROOF STEP]
apply (rule diff_apply_chart[of "\<psi> i", unfolded W_eq])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<psi> i \<in> atlas
 2. diff_fun k charts_eucl H
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> i \<in> atlas
[PROOF STEP]
using \<psi> \<open>i \<in> N\<close>
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> \<psi> ?i2 \<in> atlas
(domain \<circ> \<psi>) ` N refines X ` A
regular_cover N \<psi>
i \<in> N

goal (1 subgoal):
 1. \<psi> i \<in> atlas
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts_eucl H
[PROOF STEP]
apply (rule diff_fun_charts_euclI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on UNIV H
[PROOF STEP]
by (rule H_smooth_on)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (W i)) (H \<circ> apply_chart (\<psi> i))

goal (5 subgoals):
 1. diff_fun k (charts_submanifold ?U) (f i)
 2. diff_fun k (charts_submanifold ?V) (f i)
 3. open ?U
 4. open ?V
 5. carrier \<subseteq> ?U \<union> ?V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold (W i)) (H \<circ> apply_chart (\<psi> i))
[PROOF STEP]
show "diff_fun k (charts_submanifold (W i)) (f i)"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold (W i)) (H \<circ> apply_chart (\<psi> i))

goal (1 subgoal):
 1. diff_fun k (charts_submanifold (W i)) (f i)
[PROOF STEP]
by (rule diff_fun.diff_fun_cong) (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (W i)) (f i)

goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) (f i)
 2. open (W i)
 3. open ?V
 4. carrier \<subseteq> W i \<union> ?V
[PROOF STEP]
interpret V': submanifold _ _ "carrier - closure (V i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submanifold charts k (carrier - closure (V i))
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) (f i)
 2. open (W i)
 3. open ?V
 4. carrier \<subseteq> W i \<union> ?V
[PROOF STEP]
have "diff_fun k (charts_submanifold (carrier - closure (V i))) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (carrier - closure (V i))) 0
[PROOF STEP]
by (rule V'.sub.diff_fun_zero)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (carrier - closure (V i))) 0

goal (4 subgoals):
 1. diff_fun k (charts_submanifold ?V) (f i)
 2. open (W i)
 3. open ?V
 4. carrier \<subseteq> W i \<union> ?V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold (carrier - closure (V i))) 0
[PROOF STEP]
show "diff_fun k (charts_submanifold (carrier - closure (V i))) (f i)"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold (carrier - closure (V i))) 0

goal (1 subgoal):
 1. diff_fun k (charts_submanifold (carrier - closure (V i))) (f i)
[PROOF STEP]
apply (rule diff_fun.diff_fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> V'.sub.carrier \<Longrightarrow> 0 x = f i x
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> V'.sub.carrier \<Longrightarrow> 0 x = (if x \<in> W i then H (apply_chart (\<psi> i) x) else 0)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> closure (V i); x \<in> carrier; x \<in> W i\<rbrakk> \<Longrightarrow> H (apply_chart (\<psi> i) x) = 0
[PROOF STEP]
apply (rule H_eq_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> closure (V i); x \<in> carrier; x \<in> W i\<rbrakk> \<Longrightarrow> apply_chart (\<psi> i) x \<notin> ball (0::'b) 2
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<notin> closure (inv_chart (\<psi> i) ` ball (0::'b) 2); x \<in> carrier; x \<in> W i\<rbrakk> \<Longrightarrow> apply_chart (\<psi> i) x \<notin> ball (0::'b) 2
[PROOF STEP]
by (metis W_eq image_eqI in_closureI inv_chart_inverse)
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (carrier - closure (V i))) (f i)

goal (3 subgoals):
 1. open (W i)
 2. open (carrier - closure (V i))
 3. carrier \<subseteq> W i \<union> (carrier - closure (V i))
[PROOF STEP]
show "open (W i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (W i)
[PROOF STEP]
by (auto simp: W_def regular_cover i)
[PROOF STATE]
proof (state)
this:
open (W i)

goal (2 subgoals):
 1. open (carrier - closure (V i))
 2. carrier \<subseteq> W i \<union> (carrier - closure (V i))
[PROOF STEP]
show "open (carrier - closure (V i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (carrier - closure (V i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (carrier - closure (V i))

goal (1 subgoal):
 1. carrier \<subseteq> W i \<union> (carrier - closure (V i))
[PROOF STEP]
show "carrier \<subseteq> W i \<union> (carrier - closure (V i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier \<subseteq> W i \<union> (carrier - closure (V i))
[PROOF STEP]
using V_subset_W[OF i]
[PROOF STATE]
proof (prove)
using this:
closure (V i) \<subseteq> W i

goal (1 subgoal):
 1. carrier \<subseteq> W i \<union> (carrier - closure (V i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
carrier \<subseteq> W i \<union> (carrier - closure (V i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> diff_fun k charts (f ?i2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define g where "g \<psi> x = f \<psi> x / (\<Sum>i\<in>{j\<in>N. x \<in> W j}. f i x)" for \<psi> x
[PROOF STATE]
proof (state)
this:
g ?\<psi> ?x = f ?\<psi> ?x / (\<Sum>i\<in>{j \<in> N. ?x \<in> W j}. f i ?x)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<forall>p\<in>carrier. \<exists>I. p \<in> I \<and> open I \<and>finite {i \<in> N. W i \<inter> I \<noteq> {}}"
    (is "\<forall>p\<in>carrier. ?P p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>carrier. \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
proof (rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
assume "p \<in> carrier"
[PROOF STATE]
proof (state)
this:
p \<in> carrier

goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
from locally_finite_onE[OF regular_cover(3) this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>Na. \<lbrakk>p \<in> Na; open Na; finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> Na \<noteq> {}}\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain I where "p \<in> I" "open I" "finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}}"
[PROOF STATE]
proof (prove)
using this:
(\<And>Na. \<lbrakk>p \<in> Na; open Na; finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> Na \<noteq> {}}\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>p \<in> I; open I; finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p \<in> I
open I
finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}}

goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<in> I
open I
finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}}

goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
have "{i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}} = {i \<in> N. W i \<inter> I \<noteq> {}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}} = {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
by (auto simp: W_eq)
[PROOF STATE]
proof (state)
this:
{i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}} = {i \<in> N. W i \<inter> I \<noteq> {}}

goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<in> I
open I
finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}}
{i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}} = {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
show "?P p"
[PROOF STATE]
proof (prove)
using this:
p \<in> I
open I
finite {i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}}
{i \<in> N. (domain \<circ> \<psi>) i \<inter> I \<noteq> {}} = {i \<in> N. W i \<inter> I \<noteq> {}}

goal (1 subgoal):
 1. \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>carrier. \<exists>I. p \<in> I \<and> open I \<and> finite {i \<in> N. W i \<inter> I \<noteq> {}}

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from bchoice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x\<in>carrier. x \<in> f x \<and> open (f x) \<and> finite {i \<in> N. W i \<inter> f x \<noteq> {}}
[PROOF STEP]
obtain I where I:
    "\<And>x. x \<in> carrier \<Longrightarrow> x \<in> I x"
    "\<And>x. x \<in> carrier \<Longrightarrow> open (I x)"
    "\<And>x. x \<in> carrier \<Longrightarrow> finite {i \<in> N. W i \<inter> I x \<noteq> {}}"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x\<in>carrier. x \<in> f x \<and> open (f x) \<and> finite {i \<in> N. W i \<inter> f x \<noteq> {}}

goal (1 subgoal):
 1. (\<And>I. \<lbrakk>\<And>x. x \<in> carrier \<Longrightarrow> x \<in> I x; \<And>x. x \<in> carrier \<Longrightarrow> open (I x); \<And>x. x \<in> carrier \<Longrightarrow> finite {i \<in> N. W i \<inter> I x \<noteq> {}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> ?x2 \<in> I ?x2
?x2 \<in> carrier \<Longrightarrow> open (I ?x2)
?x2 \<in> carrier \<Longrightarrow> finite {i \<in> N. W i \<inter> I ?x2 \<noteq> {}}

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have subset_W: "{j \<in> N. y \<in> W j} \<subseteq> {j \<in> N. W j \<inter> I x \<noteq> {}}" if "y \<in> I x" "x \<in> carrier" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {j \<in> N. y \<in> W j} \<subseteq> {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
by (auto simp: that W_eq)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y2 \<in> I ?x2; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> {j \<in> N. ?y2 \<in> W j} \<subseteq> {j \<in> N. W j \<inter> I ?x2 \<noteq> {}}

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have finite_W: "finite {j \<in> N. y \<in> W j}" if "y \<in> carrier" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {j \<in> N. y \<in> W j}
[PROOF STEP]
apply (rule finite_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {j \<in> N. y \<in> W j} \<subseteq> ?B
 2. finite ?B
[PROOF STEP]
apply (rule subset_W[OF _ that])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y \<in> I y
 2. finite {j \<in> N. W j \<inter> I y \<noteq> {}}
[PROOF STEP]
apply (rule I[OF that])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {j \<in> N. W j \<inter> I y \<noteq> {}}
[PROOF STEP]
apply (rule I[unfolded o_def, OF that])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?y2 \<in> carrier \<Longrightarrow> finite {j \<in> N. ?y2 \<in> W j}

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have g: "diff_fun k charts (g i)" if i: "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts (g i)
[PROOF STEP]
proof (rule manifold_eucl.diff_localI, unfold diff_fun_def[symmetric])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (g i)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (g i)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
assume x: "x \<in> carrier"
[PROOF STATE]
proof (state)
this:
x \<in> carrier

goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (g i)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
show "open (I x)" "x \<in> I x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (I x) &&& x \<in> I x
[PROOF STEP]
using I x
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> carrier \<Longrightarrow> ?x2 \<in> I ?x2
?x2 \<in> carrier \<Longrightarrow> open (I ?x2)
?x2 \<in> carrier \<Longrightarrow> finite {i \<in> N. W i \<inter> I ?x2 \<noteq> {}}
x \<in> carrier

goal (1 subgoal):
 1. open (I x) &&& x \<in> I x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (I x)
x \<in> I x

goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open (I x)
x \<in> I x
[PROOF STEP]
interpret submanifold _ _ "I x"
[PROOF STATE]
proof (prove)
using this:
open (I x)
x \<in> I x

goal (1 subgoal):
 1. submanifold charts k (I x)
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
interpret df: diff_fun k charts "f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts (f i)
[PROOF STEP]
by (rule f_diff) fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
have "diff_fun k (charts_submanifold (I x)) (\<lambda>y. f i y / (\<Sum>j\<in>{j\<in>N. W j \<inter> I x \<noteq> {}}. f j y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (\<lambda>y. f i y / (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y))
[PROOF STEP]
apply (rule sub.diff_fun_divide)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. diff_fun k (charts_submanifold (I x)) (f i)
 2. diff_fun k (charts_submanifold (I x)) (\<lambda>xa. \<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa)
 3. \<And>y. y \<in> sub.carrier \<Longrightarrow> (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y) \<noteq> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (f i)
[PROOF STEP]
apply (rule df.diff_submanifold[folded diff_fun_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (I x)
[PROOF STEP]
by (rule I) fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. diff_fun k (charts_submanifold (I x)) (\<lambda>xa. \<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa)
 2. \<And>y. y \<in> sub.carrier \<Longrightarrow> (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y) \<noteq> 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (\<lambda>xa. \<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa)
[PROOF STEP]
proof (rule sub.diff_fun_sum, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<in> N; W j \<inter> I x \<noteq> {}\<rbrakk> \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (f j)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<in> N; W j \<inter> I x \<noteq> {}\<rbrakk> \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (f j)
[PROOF STEP]
assume "j \<in> N" "W j \<inter> I x \<noteq> {}"
[PROOF STATE]
proof (state)
this:
j \<in> N
W j \<inter> I x \<noteq> {}

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<in> N; W j \<inter> I x \<noteq> {}\<rbrakk> \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (f j)
[PROOF STEP]
interpret df': diff_fun k charts "f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts (f j)
[PROOF STEP]
by (rule f_diff) fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<in> N; W j \<inter> I x \<noteq> {}\<rbrakk> \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (f j)
[PROOF STEP]
show "diff_fun k (charts_submanifold (I x)) (f j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (f j)
[PROOF STEP]
apply (rule df'.diff_fun_submanifold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (I x)
[PROOF STEP]
by (rule I) fact
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (I x)) (f j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> sub.carrier \<Longrightarrow> (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y) \<noteq> 0
[PROOF STEP]
subgoal for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> sub.carrier \<Longrightarrow> (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y) \<noteq> 0
[PROOF STEP]
apply (subst sum_nonneg_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. y \<in> sub.carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
 2. \<And>xa. \<lbrakk>y \<in> sub.carrier; xa \<in> {j \<in> N. W j \<inter> I x \<noteq> {}}\<rbrakk> \<Longrightarrow> 0 \<le> f xa y
 3. y \<in> sub.carrier \<Longrightarrow> \<not> (\<forall>x\<in>{j \<in> N. W j \<inter> I x \<noteq> {}}. f x y = 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> sub.carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
using I(3)[OF x]
[PROOF STATE]
proof (prove)
using this:
finite {i \<in> N. W i \<inter> I x \<noteq> {}}

goal (1 subgoal):
 1. y \<in> sub.carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>y \<in> sub.carrier; xa \<in> {j \<in> N. W j \<inter> I x \<noteq> {}}\<rbrakk> \<Longrightarrow> 0 \<le> f xa y
 2. y \<in> sub.carrier \<Longrightarrow> \<not> (\<forall>x\<in>{j \<in> N. W j \<inter> I x \<noteq> {}}. f x y = 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> sub.carrier; xa_ \<in> {j \<in> N. W j \<inter> I x \<noteq> {}}\<rbrakk> \<Longrightarrow> 0 \<le> f xa_ y
[PROOF STEP]
using H_range
[PROOF STATE]
proof (prove)
using this:
0 \<le> H ?x
H ?x \<le> 1

goal (1 subgoal):
 1. \<lbrakk>y \<in> sub.carrier; xa_ \<in> {j \<in> N. W j \<inter> I x \<noteq> {}}\<rbrakk> \<Longrightarrow> 0 \<le> f xa_ y
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> sub.carrier \<Longrightarrow> \<not> (\<forall>x\<in>{j \<in> N. W j \<inter> I x \<noteq> {}}. f x y = 0)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> sub.carrier \<Longrightarrow> \<not> (\<forall>x\<in>{j \<in> N. W j \<inter> I x \<noteq> {}}. f x y = 0)
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
assume y: "y \<in> I x" "y \<in> carrier"
[PROOF STATE]
proof (state)
this:
y \<in> I x
y \<in> carrier

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> I x
y \<in> carrier
[PROOF STEP]
obtain j where "j \<in> N" "y \<in> U j"
[PROOF STATE]
proof (prove)
using this:
y \<in> I x
y \<in> carrier

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> N; y \<in> U j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding regular_cover(5)
[PROOF STATE]
proof (prove)
using this:
y \<in> I x
y \<in> \<Union> (U ` N)

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> N; y \<in> U j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<in> N
y \<in> U j

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<in> N
y \<in> U j
[PROOF STEP]
have "y \<in> W j"
[PROOF STATE]
proof (prove)
using this:
j \<in> N
y \<in> U j

goal (1 subgoal):
 1. y \<in> W j
[PROOF STEP]
by (auto simp: U_def W_def)
[PROOF STATE]
proof (state)
this:
y \<in> W j

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> W j

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
have "W j \<inter> I x \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W j \<inter> I x \<noteq> {}
[PROOF STEP]
using W_eq \<open>j \<in> N\<close> \<open>open (I x)\<close> \<open>y \<in> W j\<close> \<open>y \<in> carrier\<close> \<open>y \<in> I x\<close>
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> domain (\<psi> ?i2) = W ?i2
j \<in> N
open (I x)
y \<in> W j
y \<in> carrier
y \<in> I x

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

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
W j \<inter> I x \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
note f_eq_one[OF \<open>j \<in> N\<close> \<open>y \<in> U j\<close>]
[PROOF STATE]
proof (state)
this:
f j y = 1

goal (1 subgoal):
 1. \<lbrakk>y \<in> I x; y \<in> carrier\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> W j
W j \<inter> I x \<noteq> {}
f j y = 1
[PROOF STEP]
show "\<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
y \<in> W j
W j \<inter> I x \<noteq> {}
f j y = 1

goal (1 subgoal):
 1. \<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0
[PROOF STEP]
by (intro exI[where x=j]) (auto simp: \<open>j \<in> N\<close>)
[PROOF STATE]
proof (state)
this:
\<exists>xa. xa \<in> N \<and> W xa \<inter> I x \<noteq> {} \<and> f xa y \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (I x)) (\<lambda>y. f i y / (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y))

goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold (I x)) (\<lambda>y. f i y / (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y))
[PROOF STEP]
show "diff_fun k (charts_submanifold (I x)) (g i)"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold (I x)) (\<lambda>y. f i y / (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j y))

goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
apply (rule diff_fun.diff_fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> f i xa / (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa) = g i xa
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> f i xa / (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa) = f i xa / (\<Sum>i\<in>{j \<in> N. xa \<in> W j}. f i xa)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> f i xa = 0 \<or> (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa) = (\<Sum>i\<in>{j \<in> N. xa \<in> W j}. f i xa)
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> (\<Sum>j | j \<in> N \<and> W j \<inter> I x \<noteq> {}. f j xa) = (\<Sum>i\<in>{j \<in> N. xa \<in> W j}. f i xa)
[PROOF STEP]
apply (rule sum.mono_neutral_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
 2. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> {j \<in> N. xa \<in> W j} \<subseteq> {j \<in> N. W j \<inter> I x \<noteq> {}}
 3. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> \<forall>i\<in>{j \<in> N. W j \<inter> I x \<noteq> {}} - {j \<in> N. xa \<in> W j}. f i xa = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> I x \<and> xa_ \<in> carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
using I[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
x \<in> I x
open (I x)
finite {i \<in> N. W i \<inter> I x \<noteq> {}}

goal (1 subgoal):
 1. xa_ \<in> I x \<and> xa_ \<in> carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
unfolding o_def
[PROOF STATE]
proof (prove)
using this:
x \<in> I x
open (I x)
finite {i \<in> N. W i \<inter> I x \<noteq> {}}

goal (1 subgoal):
 1. xa_ \<in> I x \<and> xa_ \<in> carrier \<Longrightarrow> finite {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> {j \<in> N. xa \<in> W j} \<subseteq> {j \<in> N. W j \<inter> I x \<noteq> {}}
 2. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> \<forall>i\<in>{j \<in> N. W j \<inter> I x \<noteq> {}} - {j \<in> N. xa \<in> W j}. f i xa = 0
[PROOF STEP]
subgoal for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> I x \<and> y \<in> carrier \<Longrightarrow> {j \<in> N. y \<in> W j} \<subseteq> {j \<in> N. W j \<inter> I x \<noteq> {}}
[PROOF STEP]
apply (rule subset_W)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y \<in> I x \<and> y \<in> carrier \<Longrightarrow> y \<in> I x
 2. y \<in> I x \<and> y \<in> carrier \<Longrightarrow> x \<in> carrier
[PROOF STEP]
using carrier_submanifold I \<open>x \<in> carrier\<close>
[PROOF STATE]
proof (prove)
using this:
sub.carrier = I x \<inter> carrier
?x2 \<in> carrier \<Longrightarrow> ?x2 \<in> I ?x2
?x2 \<in> carrier \<Longrightarrow> open (I ?x2)
?x2 \<in> carrier \<Longrightarrow> finite {i \<in> N. W i \<inter> I ?x2 \<noteq> {}}
x \<in> carrier

goal (2 subgoals):
 1. y \<in> I x \<and> y \<in> carrier \<Longrightarrow> y \<in> I x
 2. y \<in> I x \<and> y \<in> carrier \<Longrightarrow> x \<in> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> I x \<and> xa \<in> carrier \<Longrightarrow> \<forall>i\<in>{j \<in> N. W j \<inter> I x \<noteq> {}} - {j \<in> N. xa \<in> W j}. f i xa = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> I x \<and> xa_ \<in> carrier \<Longrightarrow> \<forall>i\<in>{j \<in> N. W j \<inter> I x \<noteq> {}} - {j \<in> N. xa_ \<in> W j}. f i xa_ = 0
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (I x)) (g i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> diff_fun k charts (g ?i2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have f_nonneg: "0 \<le> f i x" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> f i x
[PROOF STEP]
by (auto simp: f_def H_range intro!: sum_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> f ?i2 ?x2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have U_sub_W: "x \<in> U i \<Longrightarrow> x \<in> W i" for x i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> U i \<Longrightarrow> x \<in> W i
[PROOF STEP]
by (auto simp: U_def W_def)
[PROOF STATE]
proof (state)
this:
?x2 \<in> U ?i2 \<Longrightarrow> ?x2 \<in> W ?i2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have sumf_pos: "(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) > 0" if "x \<in> carrier" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
(* and this sum is smooth, use to simplify earlier reasoning! *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier

goal (1 subgoal):
 1. 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
apply (auto simp: regular_cover(5))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa \<in> N; x \<in> U xa\<rbrakk> \<Longrightarrow> 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
apply (rule sum_pos2[where i=i])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> finite {j \<in> N. x \<in> W j}
 2. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> i \<in> {j \<in> N. x \<in> W j}
 3. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> 0 < f i x
 4. \<And>ia. \<lbrakk>i \<in> N; x \<in> U i; ia \<in> {j \<in> N. x \<in> W j}\<rbrakk> \<Longrightarrow> 0 \<le> f ia x
[PROOF STEP]
using finite_W[OF that]
[PROOF STATE]
proof (prove)
using this:
finite {j \<in> N. x \<in> W j}

goal (4 subgoals):
 1. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> finite {j \<in> N. x \<in> W j}
 2. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> i \<in> {j \<in> N. x \<in> W j}
 3. \<lbrakk>i \<in> N; x \<in> U i\<rbrakk> \<Longrightarrow> 0 < f i x
 4. \<And>ia. \<lbrakk>i \<in> N; x \<in> U i; ia \<in> {j \<in> N. x \<in> W j}\<rbrakk> \<Longrightarrow> 0 \<le> f ia x
[PROOF STEP]
by (auto simp: f_nonneg f_eq_one U_sub_W )
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> 0 < (\<Sum>i\<in>{j \<in> N. ?x2 \<in> W j}. f i ?x2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have sumf_nonneg: "(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<ge> 0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
by (auto simp: f_nonneg intro!: sum_nonneg)
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i\<in>{j \<in> N. ?x2 \<in> W j}. f i ?x2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have g_nonneg: "0 \<le> g i x" if "i \<in> N" "x \<in> carrier" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> g i x
[PROOF STEP]
by (auto simp: g_def intro!: divide_nonneg_nonneg sumf_nonneg f_nonneg)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 \<in> N; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> g ?i2 ?x2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have g_le_one: "g i x \<le> 1" if "i \<in> N" "x \<in> carrier" for i x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g i x \<le> 1
[PROOF STEP]
apply (auto simp add: g_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<le> 1
[PROOF STEP]
(*sumf is positive*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<le> 1
[PROOF STEP]
apply (cases "(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) = 0 \<Longrightarrow> f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<le> 1
 2. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<le> 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) = 0 \<Longrightarrow> f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<le> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<le> 1
[PROOF STEP]
apply (subst divide_le_eq_1_pos)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
 2. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
using sumf_nonneg[of x]
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)

goal (1 subgoal):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> 0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0 \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
apply (cases "x \<in> W i")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
 2. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<notin> W i\<rbrakk> \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
apply (rule member_le_sum)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> i \<in> {j \<in> N. x \<in> W j}
 2. \<And>xa. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i; xa \<in> {j \<in> N. x \<in> W j} - {i}\<rbrakk> \<Longrightarrow> 0 \<le> f xa x
 3. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> finite {j \<in> N. x \<in> W j}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> i \<in> {j \<in> N. x \<in> W j}
[PROOF STEP]
using \<open>i \<in> N\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> N

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> i \<in> {j \<in> N. x \<in> W j}
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i; xa \<in> {j \<in> N. x \<in> W j} - {i}\<rbrakk> \<Longrightarrow> 0 \<le> f xa x
 2. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> finite {j \<in> N. x \<in> W j}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i; xa_ \<in> {j \<in> N. x \<in> W j} - {i}\<rbrakk> \<Longrightarrow> 0 \<le> f xa_ x
[PROOF STEP]
by (rule f_nonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> finite {j \<in> N. x \<in> W j}
[PROOF STEP]
using sum.infinite
[PROOF STATE]
proof (prove)
using this:
infinite ?A \<Longrightarrow> sum ?g ?A = (0::?'a)

goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<in> W i\<rbrakk> \<Longrightarrow> finite {j \<in> N. x \<in> W j}
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<notin> W i\<rbrakk> \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) \<noteq> 0; x \<notin> W i\<rbrakk> \<Longrightarrow> f i x \<le> (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)
[PROOF STEP]
by (simp add: f_simps sum_nonneg H_range)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 \<in> N; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> g ?i2 ?x2 \<le> 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have sum_g: "(\<Sum>i | i \<in> N \<and> x \<in> W i. g i x) = 1" if "x \<in> carrier" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x) = 1
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> x \<in> W i. f i x / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)) = 1
[PROOF STEP]
apply (subst sum_divide_distrib[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> x \<in> W i. f i x) / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) = 1
[PROOF STEP]
using sumf_pos[OF that]
[PROOF STATE]
proof (prove)
using this:
0 < (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x)

goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> x \<in> W i. f i x) / (\<Sum>i\<in>{j \<in> N. x \<in> W j}. f i x) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> N \<and> ?x2 \<in> W i. g i ?x2) = 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists>a. \<forall>i\<in>N. W i \<subseteq> X (a i) \<and> a i \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. \<forall>i\<in>N. W i \<subseteq> X (a i) \<and> a i \<in> A
[PROOF STEP]
using \<psi>(2)
[PROOF STATE]
proof (prove)
using this:
(domain \<circ> \<psi>) ` N refines X ` A

goal (1 subgoal):
 1. \<exists>a. \<forall>i\<in>N. W i \<subseteq> X (a i) \<and> a i \<in> A
[PROOF STEP]
by (intro bchoice) (auto simp: refines_def W_eq)
[PROOF STATE]
proof (state)
this:
\<exists>a. \<forall>i\<in>N. W i \<subseteq> X (a i) \<and> a i \<in> A

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. \<forall>i\<in>N. W i \<subseteq> X (a i) \<and> a i \<in> A
[PROOF STEP]
obtain a where a: "\<And>i. i \<in> N \<Longrightarrow> W i \<subseteq> X (a i)" "\<And>i. i \<in> N \<Longrightarrow> a i \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. \<forall>i\<in>N. W i \<subseteq> X (a i) \<and> a i \<in> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>\<And>i. i \<in> N \<Longrightarrow> W i \<subseteq> X (a i); \<And>i. i \<in> N \<Longrightarrow> a i \<in> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> W ?i2 \<subseteq> X (a ?i2)
?i2 \<in> N \<Longrightarrow> a ?i2 \<in> A

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define \<phi> where "\<phi> \<alpha> x = (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x)" for \<alpha> x
[PROOF STATE]
proof (state)
this:
\<phi> ?\<alpha> ?x = (\<Sum>i | i \<in> N \<and> a i = ?\<alpha> \<and> ?x \<in> W i. g i ?x)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "diff_fun k charts (\<phi> \<alpha>)" if "\<alpha> \<in> A" for \<alpha>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts (\<phi> \<alpha>)
[PROOF STEP]
proof (rule manifold_eucl.diff_localI, unfold diff_fun_def[symmetric])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (\<phi> \<alpha>)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
(* extract the lemma here?! *)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (\<phi> \<alpha>)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (\<phi> \<alpha>)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
assume x: "x \<in> carrier"
[PROOF STATE]
proof (state)
this:
x \<in> carrier

goal (3 subgoals):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (?U x)) (\<phi> \<alpha>)
 2. \<And>x. x \<in> carrier \<Longrightarrow> open (?U x)
 3. \<And>x. x \<in> carrier \<Longrightarrow> x \<in> ?U x
[PROOF STEP]
show "open (I x)" "x \<in> I x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (I x) &&& x \<in> I x
[PROOF STEP]
using I x
[PROOF STATE]
proof (prove)
using this:
?x2 \<in> carrier \<Longrightarrow> ?x2 \<in> I ?x2
?x2 \<in> carrier \<Longrightarrow> open (I ?x2)
?x2 \<in> carrier \<Longrightarrow> finite {i \<in> N. W i \<inter> I ?x2 \<noteq> {}}
x \<in> carrier

goal (1 subgoal):
 1. open (I x) &&& x \<in> I x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
open (I x)
x \<in> I x

goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (\<phi> \<alpha>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
open (I x)
x \<in> I x
[PROOF STEP]
interpret submanifold _ _ "I x"
[PROOF STATE]
proof (prove)
using this:
open (I x)
x \<in> I x

goal (1 subgoal):
 1. submanifold charts k (I x)
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (\<phi> \<alpha>)
[PROOF STEP]
have "diff_fun k (charts_submanifold (I x)) (\<lambda>y. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (\<lambda>y. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i y)
[PROOF STEP]
apply (rule sub.diff_fun_sum, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> N; W i \<inter> I x \<noteq> {}; \<alpha> = a i\<rbrakk> \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
subgoal premises prems for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
interpret dg: diff_fun k charts "g i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k charts (g i)
[PROOF STEP]
by (rule g) fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (g i)
[PROOF STEP]
apply (rule dg.diff_fun_submanifold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (I x)
[PROOF STEP]
by (rule I) fact
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (I x)) (g i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (I x)) (\<lambda>y. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i y)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier \<Longrightarrow> diff_fun k (charts_submanifold (I x)) (\<phi> \<alpha>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
diff_fun k (charts_submanifold (I x)) (\<lambda>y. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i y)
[PROOF STEP]
show "diff_fun k (charts_submanifold (I x)) (\<phi> \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
diff_fun k (charts_submanifold (I x)) (\<lambda>y. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i y)

goal (1 subgoal):
 1. diff_fun k (charts_submanifold (I x)) (\<phi> \<alpha>)
[PROOF STEP]
apply (rule diff_fun.diff_fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i xa) = \<phi> \<alpha> xa
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}. g i xa) = (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> xa \<in> W i. g i xa)
[PROOF STEP]
apply (rule sum.mono_neutral_right)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> finite {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
 2. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> {i \<in> N. a i = \<alpha> \<and> xa \<in> W i} \<subseteq> {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
 3. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> \<forall>i\<in>{i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}} - {i \<in> N. a i = \<alpha> \<and> xa \<in> W i}. g i xa = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> sub.carrier \<Longrightarrow> finite {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
[PROOF STEP]
using _ I(3)[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite {i \<in> N. W i \<inter> I x \<noteq> {}}

goal (1 subgoal):
 1. xa_ \<in> sub.carrier \<Longrightarrow> finite {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
[PROOF STEP]
by (rule finite_subset) (auto simp:)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> {i \<in> N. a i = \<alpha> \<and> xa \<in> W i} \<subseteq> {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
 2. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> \<forall>i\<in>{i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}} - {i \<in> N. a i = \<alpha> \<and> xa \<in> W i}. g i xa = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> sub.carrier \<Longrightarrow> {i \<in> N. a i = \<alpha> \<and> xa_ \<in> W i} \<subseteq> {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
[PROOF STEP]
using \<open>open (I x)\<close> carrier_submanifold
[PROOF STATE]
proof (prove)
using this:
open (I x)
sub.carrier = I x \<inter> carrier

goal (1 subgoal):
 1. xa_ \<in> sub.carrier \<Longrightarrow> {i \<in> N. a i = \<alpha> \<and> xa_ \<in> W i} \<subseteq> {i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> sub.carrier \<Longrightarrow> \<forall>i\<in>{i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}} - {i \<in> N. a i = \<alpha> \<and> xa \<in> W i}. g i xa = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> sub.carrier \<Longrightarrow> \<forall>i\<in>{i \<in> N. a i = \<alpha> \<and> W i \<inter> I x \<noteq> {}} - {i \<in> N. a i = \<alpha> \<and> xa_ \<in> W i}. g i xa_ = 0
[PROOF STEP]
by (auto simp: g_def f_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
diff_fun k (charts_submanifold (I x)) (\<phi> \<alpha>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<alpha>2 \<in> A \<Longrightarrow> diff_fun k charts (\<phi> ?\<alpha>2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<alpha>2 \<in> A \<Longrightarrow> diff_fun k charts (\<phi> ?\<alpha>2)

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "0 \<le> \<phi> \<alpha> x" if "x \<in> carrier" for \<alpha> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<phi> \<alpha> x
[PROOF STEP]
by (auto simp: \<phi>_def intro!: sum_nonneg g_nonneg that)
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> ?\<alpha>2 ?x2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> ?\<alpha>2 ?x2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<phi> \<alpha> x \<le> 1" if "\<alpha> \<in> A" "x \<in> carrier" for \<alpha> x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> 1
[PROOF STEP]
have "\<phi> \<alpha> x \<le> (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<le> (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)
[PROOF STEP]
by (rule sum_mono2[OF finite_W]) (auto simp: intro!: g_nonneg \<open>x \<in> carrier\<close>)
[PROOF STATE]
proof (state)
this:
\<phi> \<alpha> x \<le> (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)

goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> \<alpha> x \<le> (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)

goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> 1
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x) = 1
[PROOF STEP]
by (rule sum_g) fact
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<in> N \<and> x \<in> W i. g i x) = 1

goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<phi> \<alpha> x \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> \<alpha> x \<le> 1

goal (1 subgoal):
 1. \<phi> \<alpha> x \<le> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<phi> \<alpha> x \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<alpha>2 \<in> A; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> ?\<alpha>2 ?x2 \<le> 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<alpha>2 \<in> A; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> ?\<alpha>2 ?x2 \<le> 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(\<Sum>\<alpha>\<in>{\<alpha>\<in>A. \<phi> \<alpha> x \<noteq> 0}. \<phi> \<alpha> x) = 1" if "x \<in> carrier" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
have "(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) =
      (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x)
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) = (\<Sum>\<alpha> | \<alpha> \<in> A \<and> (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) = (\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)
[PROOF STEP]
apply (rule sum.Sigma)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}
 2. \<forall>\<alpha>\<in>{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. finite {i \<in> N. a i = \<alpha> \<and> x \<in> W i}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}
[PROOF STEP]
apply (rule finite_subset[where B="a ` {j \<in> N. x \<in> W j}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0} \<subseteq> a ` {j \<in> N. x \<in> W j}
 2. finite (a ` {j \<in> N. x \<in> W j})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0} \<subseteq> a ` {j \<in> N. x \<in> W j}
[PROOF STEP]
apply (auto simp: \<phi>_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa \<in> A; (\<Sum>i | i \<in> N \<and> a i = xa \<and> x \<in> W i. g i x) \<noteq> 0\<rbrakk> \<Longrightarrow> xa \<in> a ` {j \<in> N. x \<in> W j}
[PROOF STEP]
apply (subst (asm) sum_nonneg_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. xa \<in> A \<Longrightarrow> finite {i \<in> N. a i = xa \<and> x \<in> W i}
 2. \<And>xa xaa. \<lbrakk>xa \<in> A; xaa \<in> {i \<in> N. a i = xa \<and> x \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xaa x
 3. \<And>xa. \<lbrakk>xa \<in> A; \<not> (\<forall>xa\<in>{i \<in> N. a i = xa \<and> x \<in> W i}. g xa x = 0)\<rbrakk> \<Longrightarrow> xa \<in> a ` {j \<in> N. x \<in> W j}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> A \<Longrightarrow> finite {i \<in> N. a i = xa_ \<and> x \<in> W i}
[PROOF STEP]
using _ finite_W[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite {j \<in> N. x \<in> W j}

goal (1 subgoal):
 1. xa_ \<in> A \<Longrightarrow> finite {i \<in> N. a i = xa_ \<and> x \<in> W i}
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. \<lbrakk>xa \<in> A; xaa \<in> {i \<in> N. a i = xa \<and> x \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xaa x
 2. \<And>xa. \<lbrakk>xa \<in> A; \<not> (\<forall>xa\<in>{i \<in> N. a i = xa \<and> x \<in> W i}. g xa x = 0)\<rbrakk> \<Longrightarrow> xa \<in> a ` {j \<in> N. x \<in> W j}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa_ \<in> A; xaa_ \<in> {i \<in> N. a i = xa_ \<and> x \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xaa_ x
[PROOF STEP]
by (rule g_nonneg[OF _ \<open>x \<in> carrier\<close>]) auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa \<in> A; \<not> (\<forall>xa\<in>{i \<in> N. a i = xa \<and> x \<in> W i}. g xa x = 0)\<rbrakk> \<Longrightarrow> xa \<in> a ` {j \<in> N. x \<in> W j}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa_ \<in> A; \<not> (\<forall>xa\<in>{i \<in> N. a i = xa_ \<and> x \<in> W i}. g xa x = 0)\<rbrakk> \<Longrightarrow> xa_ \<in> a ` {j \<in> N. x \<in> W j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (a ` {j \<in> N. x \<in> W j})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (a ` {j \<in> N. x \<in> W j})
[PROOF STEP]
using finite_W[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
finite {j \<in> N. x \<in> W j}

goal (1 subgoal):
 1. finite (a ` {j \<in> N. x \<in> W j})
[PROOF STEP]
by (rule finite_imageI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<alpha>\<in>{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. finite {i \<in> N. a i = \<alpha> \<and> x \<in> W i}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<alpha>\<in>{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. finite {i \<in> N. a i = \<alpha> \<and> x \<in> W i}
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<alpha>. \<lbrakk>\<alpha> \<in> A; \<phi> \<alpha> x \<noteq> 0\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = \<alpha> \<and> x \<in> W i}
[PROOF STEP]
using _ finite_W[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite {j \<in> N. x \<in> W j}

goal (1 subgoal):
 1. \<And>\<alpha>. \<lbrakk>\<alpha> \<in> A; \<phi> \<alpha> x \<noteq> 0\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = \<alpha> \<and> x \<in> W i}
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) = (\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) = (\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x) = (\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)
[PROOF STEP]
apply (rule sum.reindex_cong[where l="\<lambda>i. (a i, i)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. inj_on (\<lambda>i. (a i, i)) (snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}))
 2. (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) = (\<lambda>i. (a i, i)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
 3. \<And>xa. xa \<in> snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<Longrightarrow> (case (a xa, xa) of (\<alpha>, i) \<Rightarrow> g i x) = g xa x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>i. (a i, i)) (snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}))
[PROOF STEP]
by (auto simp: inj_on_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) = (\<lambda>i. (a i, i)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
 2. \<And>xa. xa \<in> snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<Longrightarrow> (case (a xa, xa) of (\<alpha>, i) \<Rightarrow> g i x) = g xa x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) = (\<lambda>i. (a i, i)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply (auto simp: a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<phi> (a b) x \<noteq> 0; b \<in> N; x \<in> W b\<rbrakk> \<Longrightarrow> (a b, b) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply (auto simp: \<phi>_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(\<Sum>i | i \<in> N \<and> a i = a b \<and> x \<in> W i. g i x) \<noteq> 0; b \<in> N; x \<in> W b\<rbrakk> \<Longrightarrow> (a b, b) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply (subst (asm) sum_nonneg_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>b \<in> N; x \<in> W b\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = a b \<and> x \<in> W i}
 2. \<And>b xa. \<lbrakk>b \<in> N; x \<in> W b; xa \<in> {i \<in> N. a i = a b \<and> x \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xa x
 3. \<And>b. \<lbrakk>\<not> (\<forall>xa\<in>{i \<in> N. a i = a b \<and> x \<in> W i}. g xa x = 0); b \<in> N; x \<in> W b\<rbrakk> \<Longrightarrow> (a b, b) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ \<in> N; x \<in> W b_\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = a b_ \<and> x \<in> W i}
[PROOF STEP]
using _ finite_W[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite {j \<in> N. x \<in> W j}

goal (1 subgoal):
 1. \<lbrakk>b_ \<in> N; x \<in> W b_\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = a b_ \<and> x \<in> W i}
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b xa. \<lbrakk>b \<in> N; x \<in> W b; xa \<in> {i \<in> N. a i = a b \<and> x \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xa x
 2. \<And>b. \<lbrakk>\<not> (\<forall>xa\<in>{i \<in> N. a i = a b \<and> x \<in> W i}. g xa x = 0); b \<in> N; x \<in> W b\<rbrakk> \<Longrightarrow> (a b, b) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ \<in> N; x \<in> W b_; xa_ \<in> {i \<in> N. a i = a b_ \<and> x \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xa_ x
[PROOF STEP]
by (auto intro!: g_nonneg \<open>x \<in> carrier\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<not> (\<forall>xa\<in>{i \<in> N. a i = a b \<and> x \<in> W i}. g xa x = 0); b \<in> N; x \<in> W b\<rbrakk> \<Longrightarrow> (a b, b) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (\<forall>xa\<in>{ia \<in> N. a ia = a i \<and> x \<in> W ia}. g xa x = 0); i \<in> N; x \<in> W i\<rbrakk> \<Longrightarrow> (a i, i) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>i \<in> N; x \<in> W i; xa \<in> N; a xa = a i; x \<in> W xa; g xa x \<noteq> 0\<rbrakk> \<Longrightarrow> (a i, i) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
subgoal for yy
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> (a i, i) \<in> (\<lambda>x. (a x, x)) ` snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply (rule imageI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> i \<in> snd ` (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply (rule image_eqI[where x="(a i, i)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> i = snd (a i, i)
 2. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> (a i, i) \<in> (SIGMA xa:{\<alpha> \<in> A. (\<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i})
[PROOF STEP]
apply (auto intro!: a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; (\<Sum>i | i \<in> N \<and> a i = a i \<and> x \<in> W i. g i x) = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subst (asm) sum_nonneg_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> finite {ia \<in> N. a ia = a i \<and> x \<in> W ia}
 2. \<And>xa. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; xa \<in> {ia \<in> N. a ia = a i \<and> x \<in> W ia}\<rbrakk> \<Longrightarrow> 0 \<le> g xa x
 3. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; \<forall>xa\<in>{ia \<in> N. a ia = a i \<and> x \<in> W ia}. g xa x = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> finite {ia \<in> N. a ia = a i \<and> x \<in> W ia}
[PROOF STEP]
using _ finite_W[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite {j \<in> N. x \<in> W j}

goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0\<rbrakk> \<Longrightarrow> finite {ia \<in> N. a ia = a i \<and> x \<in> W ia}
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; xa \<in> {ia \<in> N. a ia = a i \<and> x \<in> W ia}\<rbrakk> \<Longrightarrow> 0 \<le> g xa x
 2. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; \<forall>xa\<in>{ia \<in> N. a ia = a i \<and> x \<in> W ia}. g xa x = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; xa_ \<in> {ia \<in> N. a ia = a i \<and> x \<in> W ia}\<rbrakk> \<Longrightarrow> 0 \<le> g xa_ x
[PROOF STEP]
by (rule g_nonneg[OF _ \<open>x \<in> carrier\<close>]) auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; \<forall>xa\<in>{ia \<in> N. a ia = a i \<and> x \<in> W ia}. g xa x = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<in> N; x \<in> W i; yy \<in> N; a yy = a i; x \<in> W yy; g yy x \<noteq> 0; \<forall>xa\<in>{ia \<in> N. a ia = a i \<and> x \<in> W ia}. g xa x = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<Longrightarrow> (case (a xa, xa) of (\<alpha>, i) \<Rightarrow> g i x) = g xa x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<Longrightarrow> (case (a xa_, xa_) of (\<alpha>, i) \<Rightarrow> g i x) = g xa_ x
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x) = (\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(\<alpha>, i)\<in>(SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x) = (\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
have "\<dots> = (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x) = (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)
[PROOF STEP]
apply (rule sum.mono_neutral_left)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {i \<in> N. x \<in> W i}
 2. snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<subseteq> {i \<in> N. x \<in> W i}
 3. \<forall>i\<in>{i \<in> N. x \<in> W i} - snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i \<in> N. x \<in> W i}
[PROOF STEP]
by (rule finite_W) fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<subseteq> {i \<in> N. x \<in> W i}
 2. \<forall>i\<in>{i \<in> N. x \<in> W i} - snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}) \<subseteq> {i \<in> N. x \<in> W i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{i \<in> N. x \<in> W i} - snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{i \<in> N. x \<in> W i} - snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x = 0
[PROOF STEP]
apply (auto simp: Sigma_def image_iff a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<phi> (a i) x = 0; i \<in> N; x \<in> W i\<rbrakk> \<Longrightarrow> g i x = 0
[PROOF STEP]
apply (auto simp: \<phi>_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>(\<Sum>i | i \<in> N \<and> a i = a i \<and> x \<in> W i. g i x) = 0; i \<in> N; x \<in> W i\<rbrakk> \<Longrightarrow> g i x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Sum>i | i \<in> N \<and> a i = a i_ \<and> x \<in> W i. g i x) = 0; i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> g i_ x = 0
[PROOF STEP]
apply (subst (asm) sum_nonneg_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> finite {ia \<in> N. a ia = a i_ \<and> x \<in> W ia}
 2. \<And>xa. \<lbrakk>i_ \<in> N; x \<in> W i_; xa \<in> {ia \<in> N. a ia = a i_ \<and> x \<in> W ia}\<rbrakk> \<Longrightarrow> 0 \<le> g xa x
 3. \<lbrakk>\<forall>xa\<in>{ia \<in> N. a ia = a i_ \<and> x \<in> W ia}. g xa x = 0; i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> g i_ x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> finite {ia \<in> N. a ia = a i_ \<and> x \<in> W ia}
[PROOF STEP]
using _ finite_W[OF \<open>x \<in> carrier\<close>]
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite {j \<in> N. x \<in> W j}

goal (1 subgoal):
 1. \<lbrakk>i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> finite {ia \<in> N. a ia = a i_ \<and> x \<in> W ia}
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>i_ \<in> N; x \<in> W i_; xa \<in> {ia \<in> N. a ia = a i_ \<and> x \<in> W ia}\<rbrakk> \<Longrightarrow> 0 \<le> g xa x
 2. \<lbrakk>\<forall>xa\<in>{ia \<in> N. a ia = a i_ \<and> x \<in> W ia}. g xa x = 0; i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> g i_ x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i_ \<in> N; x \<in> W i_; xa_ \<in> {ia \<in> N. a ia = a i_ \<and> x \<in> W ia}\<rbrakk> \<Longrightarrow> 0 \<le> g xa_ x
[PROOF STEP]
by (rule g_nonneg[OF _ \<open>x \<in> carrier\<close>]) auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa\<in>{ia \<in> N. a ia = a i_ \<and> x \<in> W ia}. g xa x = 0; i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> g i_ x = 0
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa\<in>{ia \<in> N. a ia = a i_ \<and> x \<in> W ia}. g xa x = 0; i_ \<in> N; x \<in> W i_\<rbrakk> \<Longrightarrow> g i_ x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x) = (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>snd ` (SIGMA xa:{\<alpha> \<in> A. \<phi> \<alpha> x \<noteq> 0}. {i \<in> N. a i = xa \<and> x \<in> W i}). g i x) = (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x)

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i \<in> N \<and> x \<in> W i. g i x) = 1
[PROOF STEP]
by (rule sum_g) fact
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i \<in> N \<and> x \<in> W i. g i x) = 1

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1

goal (1 subgoal):
 1. (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> x \<noteq> 0. \<phi> \<alpha> x) = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> ?x2 \<noteq> 0. \<phi> \<alpha> ?x2) = 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x2 \<in> carrier \<Longrightarrow> (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> ?x2 \<noteq> 0. \<phi> \<alpha> ?x2) = 1

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have g_supp_le_V: "support_on carrier (g i) \<subseteq> V i" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_on carrier (g i) \<subseteq> V i
[PROOF STEP]
apply (auto simp: support_on_def g_def f_def V_def dest!: H_neq_zeroD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> W i; x \<in> carrier; (\<Sum>i\<in>{j \<in> N. x \<in> W j}. H (apply_chart (\<psi> i) x)) \<noteq> 0; norm (apply_chart (\<psi> i) x) < 2\<rbrakk> \<Longrightarrow> x \<in> inv_chart (\<psi> i) ` ball (0::'b) 2
[PROOF STEP]
apply (rule image_eqI[OF ])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> W i; x \<in> carrier; (\<Sum>i\<in>{j \<in> N. x \<in> W j}. H (apply_chart (\<psi> i) x)) \<noteq> 0; norm (apply_chart (\<psi> i) x) < 2\<rbrakk> \<Longrightarrow> x = inv_chart (\<psi> i) (?x21 x)
 2. \<And>x. \<lbrakk>x \<in> W i; x \<in> carrier; (\<Sum>i\<in>{j \<in> N. x \<in> W j}. H (apply_chart (\<psi> i) x)) \<noteq> 0; norm (apply_chart (\<psi> i) x) < 2\<rbrakk> \<Longrightarrow> ?x21 x \<in> ball (0::'b) 2
[PROOF STEP]
apply (rule inv_chart_inverse[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> W i; x \<in> carrier; (\<Sum>i\<in>{j \<in> N. x \<in> W j}. H (apply_chart (\<psi> i) x)) \<noteq> 0; norm (apply_chart (\<psi> i) x) < 2\<rbrakk> \<Longrightarrow> x \<in> domain (\<psi> i)
 2. \<And>x. \<lbrakk>x \<in> W i; x \<in> carrier; (\<Sum>i\<in>{j \<in> N. x \<in> W j}. H (apply_chart (\<psi> i) x)) \<noteq> 0; norm (apply_chart (\<psi> i) x) < 2\<rbrakk> \<Longrightarrow> apply_chart (\<psi> i) x \<in> ball (0::'b) 2
[PROOF STEP]
apply (simp add: W_eq that)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> W i; x \<in> carrier; (\<Sum>i\<in>{j \<in> N. x \<in> W j}. H (apply_chart (\<psi> i) x)) \<noteq> 0; norm (apply_chart (\<psi> i) x) < 2\<rbrakk> \<Longrightarrow> apply_chart (\<psi> i) x \<in> ball (0::'b) 2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2
[PROOF STEP]
have clsupp_g_le_W: "closure (support_on carrier (g i)) \<subseteq> W i" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2

goal (1 subgoal):
 1. closure (support_on carrier (g i)) \<subseteq> W i
[PROOF STEP]
unfolding csupport_on_def
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2

goal (1 subgoal):
 1. closure (support_on carrier (g i)) \<subseteq> W i
[PROOF STEP]
using V_subset_W closure_mono that
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2
?i2 \<in> N \<Longrightarrow> closure (V ?i2) \<subseteq> W ?i2
?S \<subseteq> ?T \<Longrightarrow> closure ?S \<subseteq> closure ?T
i \<in> N

goal (1 subgoal):
 1. closure (support_on carrier (g i)) \<subseteq> W i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> closure (support_on carrier (g ?i2)) \<subseteq> W ?i2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i2 \<in> N \<Longrightarrow> closure (support_on carrier (g ?i2)) \<subseteq> W ?i2
[PROOF STEP]
have csupp_g_le_W: "csupport_on carrier (g i) \<subseteq> W i" if "i \<in> N" for i
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> closure (support_on carrier (g ?i2)) \<subseteq> W ?i2

goal (1 subgoal):
 1. csupport_on carrier (g i) \<subseteq> W i
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> closure (support_on carrier (g ?i2)) \<subseteq> W ?i2
i \<in> N

goal (1 subgoal):
 1. csupport_on carrier (g i) \<subseteq> W i
[PROOF STEP]
by (auto simp: csupport_on_def)
[PROOF STATE]
proof (state)
this:
?i2 \<in> N \<Longrightarrow> csupport_on carrier (g ?i2) \<subseteq> W ?i2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have *: "{i \<in> N. domain (\<psi> i) \<inter> Na \<noteq> {}} = {i \<in> N. W i \<inter> Na \<noteq> {}}" for Na
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i \<in> N. domain (\<psi> i) \<inter> Na \<noteq> {}} = {i \<in> N. W i \<inter> Na \<noteq> {}}
[PROOF STEP]
by (auto simp: W_eq)
[PROOF STATE]
proof (state)
this:
{i \<in> N. domain (\<psi> i) \<inter> ?Na2 \<noteq> {}} = {i \<in> N. W i \<inter> ?Na2 \<noteq> {}}

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{i \<in> N. domain (\<psi> i) \<inter> ?Na2 \<noteq> {}} = {i \<in> N. W i \<inter> ?Na2 \<noteq> {}}
[PROOF STEP]
have lfW: "locally_finite_on carrier N W"
[PROOF STATE]
proof (prove)
using this:
{i \<in> N. domain (\<psi> i) \<inter> ?Na2 \<noteq> {}} = {i \<in> N. W i \<inter> ?Na2 \<noteq> {}}

goal (1 subgoal):
 1. locally_finite_on carrier N W
[PROOF STEP]
using regular_cover(3)
[PROOF STATE]
proof (prove)
using this:
{i \<in> N. domain (\<psi> i) \<inter> ?Na2 \<noteq> {}} = {i \<in> N. W i \<inter> ?Na2 \<noteq> {}}
locally_finite_on carrier N (domain \<circ> \<psi>)

goal (1 subgoal):
 1. locally_finite_on carrier N W
[PROOF STEP]
by (simp add: locally_finite_on_def)
[PROOF STATE]
proof (state)
this:
locally_finite_on carrier N W

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
locally_finite_on carrier N W
[PROOF STEP]
have lf_supp_g: "locally_finite_on carrier {i \<in> N. a i = \<alpha>} (\<lambda>i. support_on carrier (g i))" if "\<alpha> \<in> A" for \<alpha>
[PROOF STATE]
proof (prove)
using this:
locally_finite_on carrier N W

goal (1 subgoal):
 1. locally_finite_on carrier {i \<in> N. a i = \<alpha>} (\<lambda>i. support_on carrier (g i))
[PROOF STEP]
apply (rule locally_finite_on_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i \<in> {i \<in> N. a i = \<alpha>} \<Longrightarrow> support_on carrier (g i) \<subseteq> W i
 2. {i \<in> N. a i = \<alpha>} \<subseteq> N
[PROOF STEP]
using g_supp_le_V V_subset_W
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2
?i2 \<in> N \<Longrightarrow> closure (V ?i2) \<subseteq> W ?i2

goal (2 subgoals):
 1. \<And>i. i \<in> {i \<in> N. a i = \<alpha>} \<Longrightarrow> support_on carrier (g i) \<subseteq> W i
 2. {i \<in> N. a i = \<alpha>} \<subseteq> N
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
?\<alpha>2 \<in> A \<Longrightarrow> locally_finite_on carrier {i \<in> N. a i = ?\<alpha>2} (\<lambda>i. support_on carrier (g i))

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>" if "\<alpha> \<in> A" for \<alpha>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
have *: "closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<subseteq> closure (\<Union>i\<in>N. V i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<subseteq> closure (\<Union> (V ` N))
[PROOF STEP]
by (rule closure_mono) (use g_supp_le_V in auto)
[PROOF STATE]
proof (state)
this:
closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<subseteq> closure (\<Union> (V ` N))

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
have "support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
[PROOF STEP]
unfolding \<phi>_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. support_on carrier (\<lambda>x. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. support_on carrier (\<lambda>x. \<Sum>i | i \<in> N \<and> a i = \<alpha> \<and> x \<in> W i. g i x) \<subseteq> ?y1
 2. ?y1 \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
[PROOF STEP]
apply (rule support_on_nonneg_sum_subset')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>carrier. \<Union>i\<in>{i \<in> N. a i = \<alpha> \<and> x \<in> W i}. support_on carrier (g i)) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
[PROOF STEP]
using g_supp_le_V
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> support_on carrier (g ?i2) \<subseteq> V ?i2

goal (1 subgoal):
 1. (\<Union>x\<in>carrier. \<Union>i\<in>{i \<in> N. a i = \<alpha> \<and> x \<in> W i}. support_on carrier (g i)) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
[PROOF STEP]
by (auto simp: carrier_V)
[PROOF STATE]
proof (state)
this:
support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
[PROOF STEP]
have "csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> closure \<dots> \<inter> carrier"
[PROOF STATE]
proof (prove)
using this:
support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier
[PROOF STEP]
unfolding csupport_on_def
[PROOF STATE]
proof (prove)
using this:
support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))

goal (1 subgoal):
 1. closure (support_on carrier (\<phi> \<alpha>)) \<inter> carrier \<subseteq> closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier
[PROOF STEP]
using closure_mono
[PROOF STATE]
proof (prove)
using this:
support_on carrier (\<phi> \<alpha>) \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i))
?S \<subseteq> ?T \<Longrightarrow> closure ?S \<subseteq> closure ?T

goal (1 subgoal):
 1. closure (support_on carrier (\<phi> \<alpha>)) \<inter> carrier \<subseteq> closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
have "\<dots> = (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier = (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i)))
[PROOF STEP]
apply (rule locally_finite_on_closure_Union[OF lf_supp_g[OF that], symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {i \<in> N. a i = \<alpha>} \<Longrightarrow> closure (support_on carrier (g i)) \<subseteq> carrier
[PROOF STEP]
using closure_mono[OF g_supp_le_V] V_subset_W
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> N \<Longrightarrow> closure (support_on carrier (g ?i3)) \<subseteq> closure (V ?i3)
?i2 \<in> N \<Longrightarrow> closure (V ?i2) \<subseteq> W ?i2

goal (1 subgoal):
 1. \<And>i. i \<in> {i \<in> N. a i = \<alpha>} \<Longrightarrow> closure (support_on carrier (g i)) \<subseteq> carrier
[PROOF STEP]
by (force simp: carrier_W)
[PROOF STATE]
proof (state)
this:
closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier = (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i)))

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
closure (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. support_on carrier (g i)) \<inter> carrier = (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i)))

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
have "\<dots> \<subseteq> (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. W i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i))) \<subseteq> \<Union> (W ` {i \<in> N. a i = \<alpha>})
[PROOF STEP]
apply (rule UN_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {i \<in> N. a i = \<alpha>} \<subseteq> {i \<in> N. a i = \<alpha>}
 2. \<And>i. i \<in> {i \<in> N. a i = \<alpha>} \<Longrightarrow> closure (support_on carrier (g i)) \<subseteq> W i
[PROOF STEP]
using clsupp_g_le_W
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> closure (support_on carrier (g ?i2)) \<subseteq> W ?i2

goal (2 subgoals):
 1. {i \<in> N. a i = \<alpha>} \<subseteq> {i \<in> N. a i = \<alpha>}
 2. \<And>i. i \<in> {i \<in> N. a i = \<alpha>} \<Longrightarrow> closure (support_on carrier (g i)) \<subseteq> W i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i))) \<subseteq> \<Union> (W ` {i \<in> N. a i = \<alpha>})

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{i \<in> N. a i = \<alpha>}. closure (support_on carrier (g i))) \<subseteq> \<Union> (W ` {i \<in> N. a i = \<alpha>})

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
have "\<dots> \<subseteq> X \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (W ` {i \<in> N. a i = \<alpha>}) \<subseteq> X \<alpha>
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
?i2 \<in> N \<Longrightarrow> W ?i2 \<subseteq> X (a ?i2)
?i2 \<in> N \<Longrightarrow> a ?i2 \<in> A

goal (1 subgoal):
 1. \<Union> (W ` {i \<in> N. a i = \<alpha>}) \<subseteq> X \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (W ` {i \<in> N. a i = \<alpha>}) \<subseteq> X \<alpha>

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>

goal (1 subgoal):
 1. csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
csupport_on carrier (\<phi> \<alpha>) \<inter> carrier \<subseteq> X \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<alpha>2 \<in> A \<Longrightarrow> csupport_on carrier (\<phi> ?\<alpha>2) \<inter> carrier \<subseteq> X ?\<alpha>2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<alpha>2 \<in> A \<Longrightarrow> csupport_on carrier (\<phi> ?\<alpha>2) \<inter> carrier \<subseteq> X ?\<alpha>2

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "locally_finite_on carrier A (\<lambda>i. support_on carrier (\<phi> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. locally_finite_on carrier A (\<lambda>i. support_on carrier (\<phi> i))
[PROOF STEP]
proof (rule locally_finite_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> N \<noteq> {}}
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> N \<noteq> {}}
[PROOF STEP]
assume "p \<in> carrier"
[PROOF STATE]
proof (state)
this:
p \<in> carrier

goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> N \<noteq> {}}
[PROOF STEP]
from locally_finite_onE[OF lfW this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>Na. \<lbrakk>p \<in> Na; open Na; finite {i \<in> N. W i \<inter> Na \<noteq> {}}\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain Nhd where Nhd: "p \<in> Nhd" "open Nhd" "finite {i \<in> N. W i \<inter> Nhd \<noteq> {}}"
[PROOF STATE]
proof (prove)
using this:
(\<And>Na. \<lbrakk>p \<in> Na; open Na; finite {i \<in> N. W i \<inter> Na \<noteq> {}}\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>Nhd. \<lbrakk>p \<in> Nhd; open Nhd; finite {i \<in> N. W i \<inter> Nhd \<noteq> {}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p \<in> Nhd
open Nhd
finite {i \<in> N. W i \<inter> Nhd \<noteq> {}}

goal (1 subgoal):
 1. \<And>p. p \<in> carrier \<Longrightarrow> \<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> N \<noteq> {}}
[PROOF STEP]
show "\<exists>Nhd. p \<in> Nhd \<and> open Nhd \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Nhd. p \<in> Nhd \<and> open Nhd \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}}
[PROOF STEP]
apply (rule exI[where x=Nhd])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> Nhd \<and> open Nhd \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}}
[PROOF STEP]
apply (auto simp: Nhd)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}}
[PROOF STEP]
apply (rule finite_subset[where B="a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}} \<subseteq> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}
 2. finite (a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}} \<subseteq> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}
[PROOF STEP]
apply (auto simp: support_on_def \<phi>_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> A; x \<notin> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}; xa \<in> Nhd; xa \<in> carrier; (\<Sum>i | i \<in> N \<and> a i = x \<and> xa \<in> W i. g i xa) \<noteq> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subst (asm) sum_nonneg_eq_0_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x \<in> A; x \<notin> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}; xa \<in> Nhd; xa \<in> carrier\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = x \<and> xa \<in> W i}
 2. \<And>x xa xb. \<lbrakk>x \<in> A; x \<notin> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}; xa \<in> Nhd; xa \<in> carrier; xb \<in> {i \<in> N. a i = x \<and> xa \<in> W i}\<rbrakk> \<Longrightarrow> 0 \<le> g xb xa
 3. \<And>x xa. \<lbrakk>x \<in> A; x \<notin> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}; xa \<in> Nhd; xa \<in> carrier; \<not> (\<forall>x\<in>{i \<in> N. a i = x \<and> xa \<in> W i}. g x xa = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp: intro!: g_nonneg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> A; x \<notin> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}; xa \<in> Nhd; xa \<in> carrier\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = x \<and> xa \<in> W i}
[PROOF STEP]
using _ finite_W
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
?y2 \<in> carrier \<Longrightarrow> finite {j \<in> N. ?y2 \<in> W j}

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> A; x \<notin> a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}}; xa \<in> Nhd; xa \<in> carrier\<rbrakk> \<Longrightarrow> finite {i \<in> N. a i = x \<and> xa \<in> W i}
[PROOF STEP]
by (rule finite_subset) auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (a ` {i \<in> N. W i \<inter> Nhd \<noteq> {}})
[PROOF STEP]
by (rule finite_imageI) fact
[PROOF STATE]
proof (state)
this:
\<exists>Nhd. p \<in> Nhd \<and> open Nhd \<and> finite {i \<in> A. support_on carrier (\<phi> i) \<inter> Nhd \<noteq> {}}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
locally_finite_on carrier A (\<lambda>i. support_on carrier (\<phi> i))

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
locally_finite_on carrier A (\<lambda>i. support_on carrier (\<phi> i))
[PROOF STEP]
have "locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))"
[PROOF STATE]
proof (prove)
using this:
locally_finite_on carrier A (\<lambda>i. support_on carrier (\<phi> i))

goal (1 subgoal):
 1. locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))
[PROOF STEP]
unfolding csupport_on_def
[PROOF STATE]
proof (prove)
using this:
locally_finite_on carrier A (\<lambda>i. support_on carrier (\<phi> i))

goal (1 subgoal):
 1. locally_finite_on carrier A (\<lambda>i. closure (support_on carrier (\<phi> i)))
[PROOF STEP]
by (rule locally_finite_on_closure)
[PROOF STATE]
proof (state)
this:
locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))

goal (1 subgoal):
 1. (\<And>\<phi>. \<lbrakk>\<And>i. i \<in> A \<Longrightarrow> diff_fun k charts (\<phi> i); \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> 0 \<le> \<phi> i x; \<And>i x. \<lbrakk>i \<in> A; x \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> i x \<le> 1; \<And>x. x \<in> carrier \<Longrightarrow> (\<Sum>i | i \<in> A \<and> \<phi> i x \<noteq> 0. \<phi> i x) = 1; \<And>i. i \<in> A \<Longrightarrow> csupport_on carrier (\<phi> i) \<inter> carrier \<subseteq> X i; locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<alpha>2 \<in> A \<Longrightarrow> diff_fun k charts (\<phi> ?\<alpha>2)
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> ?\<alpha>2 ?x2
\<lbrakk>?\<alpha>2 \<in> A; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> ?\<alpha>2 ?x2 \<le> 1
?x2 \<in> carrier \<Longrightarrow> (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> ?x2 \<noteq> 0. \<phi> \<alpha> ?x2) = 1
?\<alpha>2 \<in> A \<Longrightarrow> csupport_on carrier (\<phi> ?\<alpha>2) \<inter> carrier \<subseteq> X ?\<alpha>2
locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<alpha>2 \<in> A \<Longrightarrow> diff_fun k charts (\<phi> ?\<alpha>2)
?x2 \<in> carrier \<Longrightarrow> 0 \<le> \<phi> ?\<alpha>2 ?x2
\<lbrakk>?\<alpha>2 \<in> A; ?x2 \<in> carrier\<rbrakk> \<Longrightarrow> \<phi> ?\<alpha>2 ?x2 \<le> 1
?x2 \<in> carrier \<Longrightarrow> (\<Sum>\<alpha> | \<alpha> \<in> A \<and> \<phi> \<alpha> ?x2 \<noteq> 0. \<phi> \<alpha> ?x2) = 1
?\<alpha>2 \<in> A \<Longrightarrow> csupport_on carrier (\<phi> ?\<alpha>2) \<inter> carrier \<subseteq> X ?\<alpha>2
locally_finite_on carrier A (\<lambda>i. csupport_on carrier (\<phi> i))

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

goal:
No subgoals!
[PROOF STEP]
qed