[STATEMENT]
lemma small_hom:
    shows "small (hom a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (hom a b)
[PROOF STEP]
proof (cases "ide a \<and> ide b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
 2. \<not> (ide a \<and> ide b) \<Longrightarrow> small (hom a b)
[PROOF STEP]
assume 1: "\<not> (ide a \<and> ide b)"
[PROOF STATE]
proof (state)
this:
\<not> (ide a \<and> ide b)

goal (2 subgoals):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
 2. \<not> (ide a \<and> ide b) \<Longrightarrow> small (hom a b)
[PROOF STEP]
have "\<And>f. \<not> \<guillemotleft>f : a \<rightarrow> b\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<not> \<guillemotleft>f : a \<rightarrow> b\<guillemotright>
[PROOF STEP]
using 1 in_hom_def ide_cod ide_dom
[PROOF STATE]
proof (prove)
using this:
\<not> (ide a \<and> ide b)
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> \<equiv> ?a \<in> domains ?f \<and> ?b \<in> codomains ?f
arr ?f \<Longrightarrow> ide (cod ?f)
arr ?f \<Longrightarrow> ide (local.dom ?f)

goal (1 subgoal):
 1. \<And>f. \<not> \<guillemotleft>f : a \<rightarrow> b\<guillemotright>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> \<guillemotleft>?f1 : a \<rightarrow> b\<guillemotright>

goal (2 subgoals):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
 2. \<not> (ide a \<and> ide b) \<Longrightarrow> small (hom a b)
[PROOF STEP]
hence "hom a b = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> \<guillemotleft>?f1 : a \<rightarrow> b\<guillemotright>

goal (1 subgoal):
 1. hom a b = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hom a b = {}

goal (2 subgoals):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
 2. \<not> (ide a \<and> ide b) \<Longrightarrow> small (hom a b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hom a b = {}

goal (1 subgoal):
 1. small (hom a b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
small (hom a b)

goal (1 subgoal):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
[PROOF STEP]
assume 1: "ide a \<and> ide b"
[PROOF STATE]
proof (state)
this:
ide a \<and> ide b

goal (1 subgoal):
 1. ide a \<and> ide b \<Longrightarrow> small (hom a b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (hom a b)
[PROOF STEP]
using 1 bij_betw_hom_vfun(5) small_Collect_vfun small_def
[PROOF STATE]
proof (prove)
using this:
ide a \<and> ide b
\<lbrakk>ide ?a; ide ?b\<rbrakk> \<Longrightarrow> bij_betw V_of_arr (hom ?a ?b) (Collect (vfun (V_of_ide ?a) (V_of_ide ?b)))
small (Collect (vfun ?A ?B))
small ?X \<equiv> \<exists>V_of. inj_on V_of ?X \<and> V_of ` ?X \<in> range elts

goal (1 subgoal):
 1. small (hom a b)
[PROOF STEP]
by (metis (no_types, lifting) bij_betw_def small_iff_range)
[PROOF STATE]
proof (state)
this:
small (hom a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_small_V_products:
    assumes "small (I :: V set)"
    shows "has_products I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_products I
[PROOF STEP]
proof (unfold has_products_def, intro conjI impI allI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. I \<noteq> UNIV
 2. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
show "I \<noteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<noteq> UNIV
[PROOF STEP]
using assms big_UNIV
[PROOF STATE]
proof (prove)
using this:
small I
\<not> small UNIV

goal (1 subgoal):
 1. I \<noteq> UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I \<noteq> UNIV

goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
fix J D
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
assume D: "discrete_diagram J comp D \<and> Collect (partial_magma.arr J) = I"
[PROOF STATE]
proof (state)
this:
discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I

goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
interpret J: category J
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category J
[PROOF STEP]
using D discrete_diagram_def
[PROOF STATE]
proof (prove)
using this:
discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I
discrete_diagram ?J ?C ?D \<equiv> category ?J \<and> diagram ?J ?C ?D \<and> discrete_diagram_axioms ?J

goal (1 subgoal):
 1. category J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
interpret D: discrete_diagram J comp D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. discrete_diagram J local.comp D
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
discrete_diagram J local.comp D \<and> Collect J.arr = I

goal (1 subgoal):
 1. discrete_diagram J local.comp D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
interpret incloD: composite_functor J comp Cls.comp D map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. composite_functor J local.comp Cls.comp D local.map
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
interpret incloD: discrete_diagram J Cls.comp incloD.map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. discrete_diagram J Cls.comp incloD.map
[PROOF STEP]
using D.is_discrete
[PROOF STATE]
proof (prove)
using this:
J.arr = J.ide

goal (1 subgoal):
 1. discrete_diagram J Cls.comp incloD.map
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
interpret incloD: diagram_in_set_category J Cls.comp \<open>\<lambda>A. A \<subseteq> Cls.Univ\<close> incloD.map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagram_in_set_category J Cls.comp (\<lambda>A. A \<subseteq> Cls.Univ) incloD.map
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
have 1: "small (Collect J.ide)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (Collect J.ide)
[PROOF STEP]
using assms D D.is_discrete
[PROOF STATE]
proof (prove)
using this:
small I
discrete_diagram J local.comp D \<and> Collect J.arr = I
J.arr = J.ide

goal (1 subgoal):
 1. small (Collect J.ide)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
small (Collect J.ide)

goal (1 subgoal):
 1. \<And>J D. discrete_diagram J local.comp D \<and> Collect (partial_magma.arr J) = I \<Longrightarrow> \<exists>a. has_as_product J D a
[PROOF STEP]
show "\<exists>a. has_as_product J D a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
have 2: "\<exists>a. Cls.has_as_product J incloD.map a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. Cls.has_as_product J incloD.map a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. Cls.has_as_product J incloD.map a
[PROOF STEP]
have "Collect J.ide \<noteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect J.ide \<noteq> UNIV
[PROOF STEP]
using J.ide_def
[PROOF STATE]
proof (prove)
using this:
J.ide ?a \<equiv> J ?a ?a \<noteq> J.null \<and> (\<forall>f. (J f ?a \<noteq> J.null \<longrightarrow> J f ?a = f) \<and> (J ?a f \<noteq> J.null \<longrightarrow> J ?a f = f))

goal (1 subgoal):
 1. Collect J.ide \<noteq> UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Collect J.ide \<noteq> UNIV

goal (1 subgoal):
 1. \<exists>a. Cls.has_as_product J incloD.map a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Collect J.ide \<noteq> UNIV

goal (1 subgoal):
 1. \<exists>a. Cls.has_as_product J incloD.map a
[PROOF STEP]
using 1 D.is_discrete Cls.has_small_products [of "Collect J.ide"]
                  Cls.has_products_def [of "Collect J.ide"] incloD.discrete_diagram_axioms
[PROOF STATE]
proof (prove)
using this:
Collect J.ide \<noteq> UNIV
small (Collect J.ide)
J.arr = J.ide
\<lbrakk>small (Collect J.ide); Collect J.ide \<noteq> UNIV\<rbrakk> \<Longrightarrow> Cls.has_products (Collect J.ide)
Cls.has_products (Collect J.ide) \<equiv> Collect J.ide \<noteq> UNIV \<and> (\<forall>J D. discrete_diagram J Cls.comp D \<and> Collect (partial_magma.arr J) = Collect J.ide \<longrightarrow> (\<exists>a. Cls.has_as_product J D a))
discrete_diagram J Cls.comp incloD.map

goal (1 subgoal):
 1. \<exists>a. Cls.has_as_product J incloD.map a
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<exists>a. Cls.has_as_product J incloD.map a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. Cls.has_as_product J incloD.map a

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
obtain \<Pi>D where \<Pi>D: "Cls.has_as_product J incloD.map \<Pi>D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Pi>D. Cls.has_as_product J incloD.map \<Pi>D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<exists>a. Cls.has_as_product J incloD.map a

goal (1 subgoal):
 1. (\<And>\<Pi>D. Cls.has_as_product J incloD.map \<Pi>D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.has_as_product J incloD.map \<Pi>D

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
interpret \<Pi>D: constant_functor J Cls.comp \<Pi>D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_functor J Cls.comp \<Pi>D
[PROOF STEP]
using \<Pi>D Cls.product_is_ide
[PROOF STATE]
proof (prove)
using this:
Cls.has_as_product J incloD.map \<Pi>D
Cls.has_as_product ?J ?D ?a \<Longrightarrow> Cls.ide ?a

goal (1 subgoal):
 1. constant_functor J Cls.comp \<Pi>D
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
obtain \<pi> where \<pi>: "product_cone J Cls.comp incloD.map \<Pi>D \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>. product_cone J Cls.comp incloD.map \<Pi>D \<pi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<Pi>D Cls.has_as_product_def
[PROOF STATE]
proof (prove)
using this:
Cls.has_as_product J incloD.map \<Pi>D
Cls.has_as_product ?J ?D ?a \<equiv> \<exists>\<pi>. product_cone ?J Cls.comp ?D ?a \<pi>

goal (1 subgoal):
 1. (\<And>\<pi>. product_cone J Cls.comp incloD.map \<Pi>D \<pi> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
product_cone J Cls.comp incloD.map \<Pi>D \<pi>

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
interpret \<pi>: product_cone J Cls.comp incloD.map \<Pi>D \<pi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. product_cone J Cls.comp incloD.map \<Pi>D \<pi>
[PROOF STEP]
using \<pi>
[PROOF STATE]
proof (prove)
using this:
product_cone J Cls.comp incloD.map \<Pi>D \<pi>

goal (1 subgoal):
 1. product_cone J Cls.comp incloD.map \<Pi>D \<pi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
have "small (Cls.hom Cls.unity \<Pi>D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
obtain \<phi> where \<phi>: "bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<phi>. bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using incloD.limits_are_sets_of_cones \<pi>.limit_cone_axioms
[PROOF STATE]
proof (prove)
using this:
incloD.has_as_limit ?a = (Cls.ide ?a \<and> (\<exists>\<phi>. bij_betw \<phi> (Cls.hom Cls.unity ?a) (incloD.cones Cls.unity)))
incloD.limit_cone \<Pi>D \<pi>

goal (1 subgoal):
 1. (\<And>\<phi>. bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity)

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
let ?J = "ZFC_in_HOL.set (Collect J.arr)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
let ?V_of_point = "\<lambda>x. VLambda ?J (\<lambda>j. V_of_arr (\<phi> x j))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
let ?Tuples = "VPi ?J (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
have V_of_point: "?V_of_point \<in> Cls.hom Cls.unity \<Pi>D \<rightarrow> elts ?Tuples"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) \<in> Cls.hom Cls.unity \<Pi>D \<rightarrow> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.hom Cls.unity \<Pi>D \<Longrightarrow> VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.hom Cls.unity \<Pi>D \<Longrightarrow> VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
assume x: "x \<in> Cls.hom Cls.unity \<Pi>D"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.hom Cls.unity \<Pi>D \<Longrightarrow> VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
have \<phi>x: "\<phi> x \<in> incloD.cones Cls.unity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x \<in> incloD.cones Cls.unity
[PROOF STEP]
using \<phi> x
[PROOF STATE]
proof (prove)
using this:
bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity)
x \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<phi> x \<in> incloD.cones Cls.unity
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj_on \<phi> (Cls.hom Cls.unity \<Pi>D) \<and> \<phi> ` Cls.hom Cls.unity \<Pi>D = incloD.cones Cls.unity
x \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<phi> x \<in> incloD.cones Cls.unity
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> x \<in> incloD.cones Cls.unity

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.hom Cls.unity \<Pi>D \<Longrightarrow> VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
interpret \<phi>x: cone J Cls.comp incloD.map Cls.unity \<open>\<phi> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incloD.cone Cls.unity (\<phi> x)
[PROOF STEP]
using \<phi>x
[PROOF STATE]
proof (prove)
using this:
\<phi> x \<in> incloD.cones Cls.unity

goal (1 subgoal):
 1. incloD.cone Cls.unity (\<phi> x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Cls.hom Cls.unity \<Pi>D \<Longrightarrow> VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
have "\<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j)
                                    \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
assume j: "J.arr j"
[PROOF STATE]
proof (state)
this:
J.arr j

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
have "\<phi> x j \<in> hom Cls.unity (D j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x j \<in> hom Cls.unity (D j)
[PROOF STEP]
by (metis (mono_tags, lifting) D.preserves_ide \<phi>x.component_in_hom cod_simp
                    ideD(1,3) in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C incloD.is_discrete incloD.preserves_cod j map_simp
                    mem_Collect_eq o_apply terminal_char2 terminal_unity\<^sub>S\<^sub>S\<^sub>C)
[PROOF STATE]
proof (state)
this:
\<phi> x j \<in> hom Cls.unity (D j)

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> x j \<in> hom Cls.unity (D j)

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
have "V_of_arr ` hom Cls.unity (D j) =
                             elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
using small_hom replacement
[PROOF STATE]
proof (prove)
using this:
small (hom ?a ?b)
small ?X \<Longrightarrow> small (?f ` ?X)

goal (1 subgoal):
 1. V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> x j \<in> hom Cls.unity (D j)
V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
show "V_of_arr (\<phi> x j)
                                 \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))"
[PROOF STATE]
proof (prove)
using this:
\<phi> x j \<in> hom Cls.unity (D j)
V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))

goal (1 subgoal):
 1. V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
using j \<phi>x bij_betw_hom_vfun(1)
[PROOF STATE]
proof (prove)
using this:
\<phi> x j \<in> hom Cls.unity (D j)
V_of_arr ` hom Cls.unity (D j) = elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
J.arr j
\<phi> x \<in> incloD.cones Cls.unity
V_of_arr \<in> hom ?a ?b \<rightarrow> Collect (vfun (V_of_ide ?a) (V_of_ide ?b))

goal (1 subgoal):
 1. V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
V_of_arr (\<phi> x j) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
J.arr ?j1 \<Longrightarrow> V_of_arr (\<phi> x ?j1) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D ?j1)))

goal (1 subgoal):
 1. \<And>x. x \<in> Cls.hom Cls.unity \<Pi>D \<Longrightarrow> VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
thus "?V_of_point x \<in> elts ?Tuples"
[PROOF STATE]
proof (prove)
using this:
J.arr ?j1 \<Longrightarrow> V_of_arr (\<phi> x ?j1) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D ?j1)))

goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
using VPi_I
[PROOF STATE]
proof (prove)
using this:
J.arr ?j1 \<Longrightarrow> V_of_arr (\<phi> x ?j1) \<in> elts (ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D ?j1)))
(\<And>x. x \<in> elts ?A \<Longrightarrow> ?b x \<in> elts (?B x)) \<Longrightarrow> VLambda ?A ?b \<in> elts (VPi ?A ?B)

goal (1 subgoal):
 1. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) \<in> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) \<in> Cls.hom Cls.unity \<Pi>D \<rightarrow> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
have "?V_of_point ` Cls.hom Cls.unity \<Pi>D \<in> range elts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
[PROOF STEP]
have "?V_of_point ` Cls.hom Cls.unity \<Pi>D \<subseteq> elts ?Tuples"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<subseteq> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
using V_of_point
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) \<in> Cls.hom Cls.unity \<Pi>D \<rightarrow> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))

goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<subseteq> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<subseteq> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))

goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<subseteq> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))

goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
[PROOF STEP]
using smaller_than_small down_raw
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<subseteq> elts (VPi (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. ZFC_in_HOL.set (V_of_arr ` hom Cls.unity (D j))))
\<lbrakk>small ?A; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> small ?B
?Y \<subseteq> elts ?x \<Longrightarrow> ?Y \<in> range elts

goal (1 subgoal):
 1. (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
have "inj_on ?V_of_point (Cls.hom Cls.unity \<Pi>D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume x: "x \<in> Cls.hom Cls.unity \<Pi>D" and y: "y \<in> Cls.hom Cls.unity \<Pi>D"
            and eq: "?V_of_point x = ?V_of_point y"
[PROOF STATE]
proof (state)
this:
x \<in> Cls.hom Cls.unity \<Pi>D
y \<in> Cls.hom Cls.unity \<Pi>D
VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have \<phi>x: "\<phi> x \<in> incloD.cones Cls.unity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x \<in> incloD.cones Cls.unity
[PROOF STEP]
using \<phi> x
[PROOF STATE]
proof (prove)
using this:
bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity)
x \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<phi> x \<in> incloD.cones Cls.unity
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj_on \<phi> (Cls.hom Cls.unity \<Pi>D) \<and> \<phi> ` Cls.hom Cls.unity \<Pi>D = incloD.cones Cls.unity
x \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<phi> x \<in> incloD.cones Cls.unity
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> x \<in> incloD.cones Cls.unity

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have \<phi>y: "\<phi> y \<in> incloD.cones Cls.unity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> y \<in> incloD.cones Cls.unity
[PROOF STEP]
using \<phi> y
[PROOF STATE]
proof (prove)
using this:
bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity)
y \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<phi> y \<in> incloD.cones Cls.unity
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj_on \<phi> (Cls.hom Cls.unity \<Pi>D) \<and> \<phi> ` Cls.hom Cls.unity \<Pi>D = incloD.cones Cls.unity
y \<in> Cls.hom Cls.unity \<Pi>D

goal (1 subgoal):
 1. \<phi> y \<in> incloD.cones Cls.unity
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> y \<in> incloD.cones Cls.unity

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
interpret \<phi>x: cone J Cls.comp incloD.map Cls.unity \<open>\<phi> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incloD.cone Cls.unity (\<phi> x)
[PROOF STEP]
using \<phi>x
[PROOF STATE]
proof (prove)
using this:
\<phi> x \<in> incloD.cones Cls.unity

goal (1 subgoal):
 1. incloD.cone Cls.unity (\<phi> x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
interpret \<phi>y: cone J Cls.comp incloD.map Cls.unity \<open>\<phi> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incloD.cone Cls.unity (\<phi> y)
[PROOF STEP]
using \<phi>y
[PROOF STATE]
proof (prove)
using this:
\<phi> y \<in> incloD.cones Cls.unity

goal (1 subgoal):
 1. incloD.cone Cls.unity (\<phi> y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "\<phi> x = \<phi> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
have "\<And>j. j \<in> elts ?J \<Longrightarrow> \<phi> x j = \<phi> y j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
assume j: "j \<in> elts ?J"
[PROOF STATE]
proof (state)
this:
j \<in> elts (ZFC_in_HOL.set (Collect J.arr))

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
hence 3: "J.arr j"
[PROOF STATE]
proof (prove)
using this:
j \<in> elts (ZFC_in_HOL.set (Collect J.arr))

goal (1 subgoal):
 1. J.arr j
[PROOF STEP]
by (simp add: 1 incloD.is_discrete)
[PROOF STATE]
proof (state)
this:
J.arr j

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
have 4: "ide (D j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (D j)
[PROOF STEP]
using 3 incloD.is_discrete D.preserves_ide
[PROOF STATE]
proof (prove)
using this:
J.arr j
J.arr = J.ide
J.ide ?a \<Longrightarrow> ide (D ?a)

goal (1 subgoal):
 1. ide (D j)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ide (D j)

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
have 5:"ide Cls.unity"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide Cls.unity
[PROOF STEP]
using Cls.terminal_unity\<^sub>S\<^sub>C terminal_char terminal_def
[PROOF STATE]
proof (prove)
using this:
Cls.terminal Cls.unity
terminal ?t = Cls.terminal ?t
terminal ?b \<equiv> ide ?b \<and> (\<forall>a. ide a \<longrightarrow> (\<exists>!f. \<guillemotleft>f : a \<rightarrow> ?b\<guillemotright>))

goal (1 subgoal):
 1. ide Cls.unity
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide Cls.unity

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
have \<phi>xj: "\<phi> x j \<in> hom Cls.unity (D j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x j \<in> hom Cls.unity (D j)
[PROOF STEP]
using 3 4 5 incloD.is_discrete \<phi>x.preserves_hom \<phi>x.A.map_simp in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
J.arr j
ide (D j)
ide Cls.unity
J.arr = J.ide
\<guillemotleft>?f : ?a \<rightarrow>\<^sub>J ?b\<guillemotright> \<Longrightarrow> Cls.in_hom (\<phi> x ?f) (\<phi>x.A.map ?a) (incloD.map ?b)
J.arr ?f \<Longrightarrow> \<phi>x.A.map ?f = Cls.unity
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. \<phi> x j \<in> hom Cls.unity (D j)
[PROOF STEP]
by (metis (no_types, lifting) J.ide_char \<phi>x.component_in_hom ideD(1) map_simp
                      mem_Collect_eq o_apply)
[PROOF STATE]
proof (state)
this:
\<phi> x j \<in> hom Cls.unity (D j)

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
have \<phi>yj: "\<phi> y j \<in> hom Cls.unity (D j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> y j \<in> hom Cls.unity (D j)
[PROOF STEP]
using 3 4 5 incloD.is_discrete \<phi>y.preserves_hom \<phi>x.A.map_simp in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
J.arr j
ide (D j)
ide Cls.unity
J.arr = J.ide
\<guillemotleft>?f : ?a \<rightarrow>\<^sub>J ?b\<guillemotright> \<Longrightarrow> Cls.in_hom (\<phi> y ?f) (\<phi>x.A.map ?a) (incloD.map ?b)
J.arr ?f \<Longrightarrow> \<phi>x.A.map ?f = Cls.unity
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. \<phi> y j \<in> hom Cls.unity (D j)
[PROOF STEP]
by (metis (no_types, lifting) J.ide_char \<phi>y.component_in_hom ideD(1) map_simp
                      mem_Collect_eq o_apply)
[PROOF STATE]
proof (state)
this:
\<phi> y j \<in> hom Cls.unity (D j)

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x j = \<phi> y j
[PROOF STEP]
show "\<phi> x j = \<phi> y j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> x j = \<phi> y j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> x j = \<phi> y j
[PROOF STEP]
have "\<And>j. j \<in> elts ?J \<Longrightarrow> V_of_arr (\<phi> x j) = V_of_arr (\<phi> y j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> V_of_arr (\<phi> x j) = V_of_arr (\<phi> y j)
[PROOF STEP]
using x eq VLambda_eq_D2
[PROOF STATE]
proof (prove)
using this:
x \<in> Cls.hom Cls.unity \<Pi>D
VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))
\<lbrakk>VLambda ?A ?f = VLambda ?A ?g; ?x \<in> elts ?A\<rbrakk> \<Longrightarrow> ?f ?x = ?g ?x

goal (1 subgoal):
 1. \<And>j. j \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> V_of_arr (\<phi> x j) = V_of_arr (\<phi> y j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> V_of_arr (\<phi> x ?j1) = V_of_arr (\<phi> y ?j1)

goal (1 subgoal):
 1. \<phi> x j = \<phi> y j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> V_of_arr (\<phi> x ?j1) = V_of_arr (\<phi> y ?j1)

goal (1 subgoal):
 1. \<phi> x j = \<phi> y j
[PROOF STEP]
using V_of_arr_def
[PROOF STATE]
proof (prove)
using this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> V_of_arr (\<phi> x ?j1) = V_of_arr (\<phi> y ?j1)
V_of_arr ?f \<equiv> VLambda (V_of_ide (local.dom ?f)) (Cls.DN \<circ> Cls.Fun ?f \<circ> Cls.arr_of)

goal (1 subgoal):
 1. \<phi> x j = \<phi> y j
[PROOF STEP]
by (metis (mono_tags, lifting) j \<phi>xj \<phi>yj bij_betw_hom_vfun(3) mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<phi> x j = \<phi> y j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> x j = \<phi> y j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x ?j1 = \<phi> y ?j1

goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x ?j1 = \<phi> y ?j1

goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
have "elts ?J = Collect J.arr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (ZFC_in_HOL.set (Collect J.arr)) = Collect J.arr
[PROOF STEP]
by (simp add: 1 incloD.is_discrete)
[PROOF STATE]
proof (state)
this:
elts (ZFC_in_HOL.set (Collect J.arr)) = Collect J.arr

goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x ?j1 = \<phi> y ?j1
elts (ZFC_in_HOL.set (Collect J.arr)) = Collect J.arr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x ?j1 = \<phi> y ?j1
elts (ZFC_in_HOL.set (Collect J.arr)) = Collect J.arr

goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
using \<phi>x.is_extensional \<phi>y.is_extensional
[PROOF STATE]
proof (prove)
using this:
?j1 \<in> elts (ZFC_in_HOL.set (Collect J.arr)) \<Longrightarrow> \<phi> x ?j1 = \<phi> y ?j1
elts (ZFC_in_HOL.set (Collect J.arr)) = Collect J.arr
\<not> J.arr ?f \<Longrightarrow> \<phi> x ?f = Cls.null
\<not> J.arr ?f \<Longrightarrow> \<phi> y ?f = Cls.null

goal (1 subgoal):
 1. \<phi> x = \<phi> y
[PROOF STEP]
by (metis HOL.ext mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<phi> x = \<phi> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> x = \<phi> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> Cls.hom Cls.unity \<Pi>D; y \<in> Cls.hom Cls.unity \<Pi>D; VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j)) = VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> y j))\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
\<phi> x = \<phi> y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using x y \<phi> bij_betw_imp_inj_on inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<phi> x = \<phi> y
x \<in> Cls.hom Cls.unity \<Pi>D
y \<in> Cls.hom Cls.unity \<Pi>D
bij_betw \<phi> (Cls.hom Cls.unity \<Pi>D) (incloD.cones Cls.unity)
bij_betw ?f ?A ?B \<Longrightarrow> inj_on ?f ?A
inj_on ?f ?A = (\<forall>x\<in>?A. \<forall>y\<in>?A. ?f x = ?f y \<longrightarrow> x = y)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) (Cls.hom Cls.unity \<Pi>D)

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
inj_on (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
show "small (Cls.hom Cls.unity \<Pi>D)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
inj_on (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) (Cls.hom Cls.unity \<Pi>D)

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
using small_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) ` Cls.hom Cls.unity \<Pi>D \<in> range elts
inj_on (\<lambda>x. VLambda (ZFC_in_HOL.set (Collect J.arr)) (\<lambda>j. V_of_arr (\<phi> x j))) (Cls.hom Cls.unity \<Pi>D)
small ?X \<equiv> \<exists>V_of. inj_on V_of ?X \<and> V_of ` ?X \<in> range elts

goal (1 subgoal):
 1. small (Cls.hom Cls.unity \<Pi>D)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
small (Cls.hom Cls.unity \<Pi>D)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
small (Cls.hom Cls.unity \<Pi>D)

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
hence "small (Cls.set \<Pi>D)"
[PROOF STATE]
proof (prove)
using this:
small (Cls.hom Cls.unity \<Pi>D)

goal (1 subgoal):
 1. small (Cls.set \<Pi>D)
[PROOF STEP]
by (simp add: Cls.set_def)
[PROOF STATE]
proof (state)
this:
small (Cls.set \<Pi>D)

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
hence 2: "ide \<Pi>D"
[PROOF STATE]
proof (prove)
using this:
small (Cls.set \<Pi>D)

goal (1 subgoal):
 1. ide \<Pi>D
[PROOF STEP]
using ide_char\<^sub>S\<^sub>S\<^sub>C Cls.setp_set_ide Cls.product_is_ide \<Pi>D
[PROOF STATE]
proof (prove)
using this:
small (Cls.set \<Pi>D)
ide ?a = (Cls.ide ?a \<and> Cls.set ?a \<subseteq> Cls.Univ \<and> small (Cls.set ?a))
Cls.ide ?a \<Longrightarrow> Cls.set ?a \<subseteq> Cls.Univ
Cls.has_as_product ?J ?D ?a \<Longrightarrow> Cls.ide ?a
Cls.has_as_product J incloD.map \<Pi>D

goal (1 subgoal):
 1. ide \<Pi>D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ide \<Pi>D

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
interpret \<Pi>D': constant_functor J comp \<Pi>D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constant_functor J (\<cdot>) \<Pi>D
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
ide \<Pi>D

goal (1 subgoal):
 1. constant_functor J (\<cdot>) \<Pi>D
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
interpret \<pi>': cone J comp D \<Pi>D \<pi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
have "\<And>j. J.arr j \<Longrightarrow> \<guillemotleft>\<pi> j : \<Pi>D \<rightarrow> D j\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> \<guillemotleft>\<pi> j : \<Pi>D \<rightarrow> D j\<guillemotright>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>j. J.arr j \<Longrightarrow> arr (\<pi> j)
 2. \<And>j. J.arr j \<Longrightarrow> local.dom (\<pi> j) = \<Pi>D
 3. \<And>j. J.arr j \<Longrightarrow> cod (\<pi> j) = D j
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>j. J.arr j \<Longrightarrow> arr (\<pi> j)
 2. \<And>j. J.arr j \<Longrightarrow> local.dom (\<pi> j) = \<Pi>D
 3. \<And>j. J.arr j \<Longrightarrow> cod (\<pi> j) = D j
[PROOF STEP]
assume j: "J.arr j"
[PROOF STATE]
proof (state)
this:
J.arr j

goal (3 subgoals):
 1. \<And>j. J.arr j \<Longrightarrow> arr (\<pi> j)
 2. \<And>j. J.arr j \<Longrightarrow> local.dom (\<pi> j) = \<Pi>D
 3. \<And>j. J.arr j \<Longrightarrow> cod (\<pi> j) = D j
[PROOF STEP]
show 3: "arr (\<pi> j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr (\<pi> j)
[PROOF STEP]
by (metis (mono_tags, lifting) 2 D.as_nat_trans.preserves_cod D.is_discrete
                  D.preserves_ide \<pi>.component_in_hom ideD(1) ideD(3) in_homE in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
                  j map_simp o_apply)
[PROOF STATE]
proof (state)
this:
arr (\<pi> j)

goal (2 subgoals):
 1. \<And>j. J.arr j \<Longrightarrow> local.dom (\<pi> j) = \<Pi>D
 2. \<And>j. J.arr j \<Longrightarrow> cod (\<pi> j) = D j
[PROOF STEP]
show "dom (\<pi> j) = \<Pi>D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom (\<pi> j) = \<Pi>D
[PROOF STEP]
using 3 arr_char\<^sub>S\<^sub>b\<^sub>C dom_char\<^sub>S\<^sub>b\<^sub>C \<pi>.preserves_dom
[PROOF STATE]
proof (prove)
using this:
arr (\<pi> j)
arr ?f = (Cls.arr ?f \<and> (Cls.ide (Cls.dom ?f) \<and> Cls.Dom ?f \<subseteq> Cls.Univ \<and> small (Cls.Dom ?f)) \<and> Cls.ide (Cls.cod ?f) \<and> Cls.Cod ?f \<subseteq> Cls.Univ \<and> small (Cls.Cod ?f))
local.dom ?f = (if arr ?f then Cls.dom ?f else Cls.null)
J.arr ?f \<Longrightarrow> Cls.dom (\<pi> ?f) = \<Pi>D.map (J.dom ?f)

goal (1 subgoal):
 1. local.dom (\<pi> j) = \<Pi>D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.dom (\<pi> j) = \<Pi>D

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> cod (\<pi> j) = D j
[PROOF STEP]
show "cod (\<pi> j) = D j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod (\<pi> j) = D j
[PROOF STEP]
using 3 arr_char\<^sub>S\<^sub>b\<^sub>C cod_char\<^sub>S\<^sub>b\<^sub>C \<pi>.preserves_cod
[PROOF STATE]
proof (prove)
using this:
arr (\<pi> j)
arr ?f = (Cls.arr ?f \<and> (Cls.ide (Cls.dom ?f) \<and> Cls.Dom ?f \<subseteq> Cls.Univ \<and> small (Cls.Dom ?f)) \<and> Cls.ide (Cls.cod ?f) \<and> Cls.Cod ?f \<subseteq> Cls.Univ \<and> small (Cls.Cod ?f))
cod ?f = (if arr ?f then Cls.cod ?f else Cls.null)
J.arr ?f \<Longrightarrow> Cls.cod (\<pi> ?f) = incloD.map (J.cod ?f)

goal (1 subgoal):
 1. cod (\<pi> j) = D j
[PROOF STEP]
by (metis (no_types, lifting) Cls.ideD(3) D.preserves_arr functor.preserves_ide
                  incloD.is_discrete incloD.is_functor incloD.preserves_cod j map_simp o_apply)
[PROOF STATE]
proof (state)
this:
cod (\<pi> j) = D j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
J.arr ?j1 \<Longrightarrow> \<guillemotleft>\<pi> ?j1 : \<Pi>D \<rightarrow> D ?j1\<guillemotright>

goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
J.arr ?j1 \<Longrightarrow> \<guillemotleft>\<pi> ?j1 : \<Pi>D \<rightarrow> D ?j1\<guillemotright>

goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
have "D.mkCone \<pi> = \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.mkCone \<pi> = \<pi>
[PROOF STEP]
using \<pi>.is_extensional null_char
[PROOF STATE]
proof (prove)
using this:
\<not> J.arr ?f \<Longrightarrow> \<pi> ?f = Cls.null
null = Cls.null

goal (1 subgoal):
 1. D.mkCone \<pi> = \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D.mkCone \<pi> = \<pi>

goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
J.arr ?j1 \<Longrightarrow> \<guillemotleft>\<pi> ?j1 : \<Pi>D \<rightarrow> D ?j1\<guillemotright>
D.mkCone \<pi> = \<pi>
[PROOF STEP]
show "cone J comp D \<Pi>D \<pi>"
[PROOF STATE]
proof (prove)
using this:
J.arr ?j1 \<Longrightarrow> \<guillemotleft>\<pi> ?j1 : \<Pi>D \<rightarrow> D ?j1\<guillemotright>
D.mkCone \<pi> = \<pi>

goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
using 2 D.cone_mkCone [of \<Pi>D \<pi>]
[PROOF STATE]
proof (prove)
using this:
J.arr ?j1 \<Longrightarrow> \<guillemotleft>\<pi> ?j1 : \<Pi>D \<rightarrow> D ?j1\<guillemotright>
D.mkCone \<pi> = \<pi>
ide \<Pi>D
\<lbrakk>ide \<Pi>D; \<And>j. J.arr j \<Longrightarrow> \<guillemotleft>\<pi> j : \<Pi>D \<rightarrow> D j\<guillemotright>\<rbrakk> \<Longrightarrow> D.cone \<Pi>D (D.mkCone \<pi>)

goal (1 subgoal):
 1. D.cone \<Pi>D \<pi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.cone \<Pi>D \<pi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
interpret \<pi>': product_cone J comp D \<Pi>D \<pi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. product_cone J (\<cdot>) D \<Pi>D \<pi>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
fix a \<chi>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
assume \<chi>': "D.cone a \<chi>'"
[PROOF STATE]
proof (state)
this:
D.cone a \<chi>'

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
interpret \<chi>': cone J comp D a \<chi>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.cone a \<chi>'
[PROOF STEP]
using \<chi>'
[PROOF STATE]
proof (prove)
using this:
D.cone a \<chi>'

goal (1 subgoal):
 1. D.cone a \<chi>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have a: "Cls.ide a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cls.ide a
[PROOF STEP]
using ide_char\<^sub>S\<^sub>b\<^sub>C \<chi>'.A.value_is_ide
[PROOF STATE]
proof (prove)
using this:
ide ?a = (arr ?a \<and> Cls.ide ?a)
ide a

goal (1 subgoal):
 1. Cls.ide a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Cls.ide a

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Cls.ide a

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have "\<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
assume j: "J.arr j"
[PROOF STATE]
proof (state)
this:
J.arr j

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
have "\<guillemotleft>\<chi>' j : a \<rightarrow> D j\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>\<chi>' j : a \<rightarrow> D j\<guillemotright>
[PROOF STEP]
using j D.is_discrete \<chi>'.component_in_hom
[PROOF STATE]
proof (prove)
using this:
J.arr j
J.arr = J.ide
J.arr ?j \<Longrightarrow> \<guillemotleft>\<chi>' ?j : a \<rightarrow> D (J.cod ?j)\<guillemotright>

goal (1 subgoal):
 1. \<guillemotleft>\<chi>' j : a \<rightarrow> D j\<guillemotright>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<guillemotleft>\<chi>' j : a \<rightarrow> D j\<guillemotright>

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
thus "Cls.in_hom (\<chi>' j) a (incloD.map j)"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>\<chi>' j : a \<rightarrow> D j\<guillemotright>

goal (1 subgoal):
 1. Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
using a j D.is_discrete in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C map_simp
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>\<chi>' j : a \<rightarrow> D j\<guillemotright>
Cls.ide a
J.arr j
J.arr = J.ide
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)
arr ?f \<Longrightarrow> local.map ?f = ?f

goal (1 subgoal):
 1. Cls.in_hom (\<chi>' j) a (incloD.map j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Cls.in_hom (\<chi>' j) a (incloD.map j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
J.arr ?j1 \<Longrightarrow> Cls.in_hom (\<chi>' ?j1) a (incloD.map ?j1)

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Cls.ide a
J.arr ?j1 \<Longrightarrow> Cls.in_hom (\<chi>' ?j1) a (incloD.map ?j1)
[PROOF STEP]
have 3: "incloD.cone a (incloD.mkCone \<chi>')"
[PROOF STATE]
proof (prove)
using this:
Cls.ide a
J.arr ?j1 \<Longrightarrow> Cls.in_hom (\<chi>' ?j1) a (incloD.map ?j1)

goal (1 subgoal):
 1. incloD.cone a (incloD.mkCone \<chi>')
[PROOF STEP]
using incloD.cone_mkCone [of a \<chi>']
[PROOF STATE]
proof (prove)
using this:
Cls.ide a
J.arr ?j1 \<Longrightarrow> Cls.in_hom (\<chi>' ?j1) a (incloD.map ?j1)
\<lbrakk>Cls.ide a; \<And>j. J.arr j \<Longrightarrow> Cls.in_hom (\<chi>' j) a (incloD.map j)\<rbrakk> \<Longrightarrow> incloD.cone a (incloD.mkCone \<chi>')

goal (1 subgoal):
 1. incloD.cone a (incloD.mkCone \<chi>')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
incloD.cone a (incloD.mkCone \<chi>')

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
interpret \<chi>: cone J Cls.comp incloD.map a \<open>incloD.mkCone \<chi>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incloD.cone a (incloD.mkCone \<chi>')
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
incloD.cone a (incloD.mkCone \<chi>')

goal (1 subgoal):
 1. incloD.cone a (incloD.mkCone \<chi>')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have univ: "\<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'
[PROOF STEP]
using \<chi>.cone_axioms \<pi>.is_universal [of a "incloD.mkCone \<chi>'"]
[PROOF STATE]
proof (prove)
using this:
incloD.cone a (incloD.mkCone \<chi>')
incloD.cone a (incloD.mkCone \<chi>') \<Longrightarrow> \<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'

goal (1 subgoal):
 1. \<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have 4: "incloD.mkCone \<chi>' = \<chi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incloD.mkCone \<chi>' = \<chi>'
[PROOF STEP]
using D.as_nat_trans.preserves_reflects_arr D.preserves_arr Limit.cone_def
                  \<chi>' \<chi>'.is_extensional identity_functor.intro identity_functor.map_def
                  incloD.as_nat_trans.is_extensional o_apply
[PROOF STATE]
proof (prove)
using this:
arr (D ?f) = J.arr ?f
J.arr ?f \<Longrightarrow> arr (D ?f)
Limit.cone ?J ?C ?D ?a ?\<chi> \<equiv> (category ?C \<and> category ?J) \<and> diagram ?J ?C ?D \<and> constant_functor ?J ?C ?a \<and> natural_transformation ?J ?C (constant_functor.map ?J ?C ?a) ?D ?\<chi>
D.cone a \<chi>'
\<not> J.arr ?f \<Longrightarrow> \<chi>' ?f = null
category ?C \<Longrightarrow> identity_functor ?C
identity_functor ?C \<Longrightarrow> identity_functor.map ?C ?f = (if partial_magma.arr ?C ?f then ?f else partial_magma.null ?C)
\<not> J.arr ?f \<Longrightarrow> incloD.map ?f = Cls.null
(?f \<circ> ?g) ?x = ?f (?g ?x)

goal (1 subgoal):
 1. incloD.mkCone \<chi>' = \<chi>'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
incloD.mkCone \<chi>' = \<chi>'

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have 5: "D.mkCone \<pi> = \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.mkCone \<pi> = \<pi>
[PROOF STEP]
using \<pi>.is_extensional null_char
[PROOF STATE]
proof (prove)
using this:
\<not> J.arr ?f \<Longrightarrow> \<pi> ?f = Cls.null
null = Cls.null

goal (1 subgoal):
 1. D.mkCone \<pi> = \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D.mkCone \<pi> = \<pi>

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have 6: "\<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
assume f: "Cls.in_hom f a \<Pi>D"
[PROOF STATE]
proof (state)
this:
Cls.in_hom f a \<Pi>D

goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
have "incloD.cones_map f \<pi> = (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incloD.cones_map f \<pi> = (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null)
[PROOF STEP]
using f \<pi>.cone_axioms
[PROOF STATE]
proof (prove)
using this:
Cls.in_hom f a \<Pi>D
incloD.cone \<Pi>D \<pi>

goal (1 subgoal):
 1. incloD.cones_map f \<pi> = (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
incloD.cones_map f \<pi> = (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null)

goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
incloD.cones_map f \<pi> = (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null)

goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
have "... = (\<lambda>j. if J.arr j then comp (\<pi> j) f else null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)
[PROOF STEP]
have "\<And>j. J.arr j \<Longrightarrow> Cls.comp (\<pi> j) f = comp (\<pi> j) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.comp (\<pi> j) f = \<pi> j \<cdot> f
[PROOF STEP]
using f 2 comp_char in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C seq_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
Cls.in_hom f a \<Pi>D
ide \<Pi>D
?g \<cdot> ?f = (if arr ?f \<and> arr ?g \<and> Cls.seq ?g ?f then Cls.comp ?g ?f else Cls.null)
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)
seq ?g ?f = (arr ?f \<and> arr ?g \<and> Cls.seq ?g ?f)

goal (1 subgoal):
 1. \<And>j. J.arr j \<Longrightarrow> Cls.comp (\<pi> j) f = \<pi> j \<cdot> f
[PROOF STEP]
by (metis (no_types, lifting) Cls.ext Cls.in_homE \<chi>'.ide_apex
                    \<pi>'.preserves_reflects_arr arr_char\<^sub>S\<^sub>b\<^sub>C ide_char\<^sub>S\<^sub>S\<^sub>C)
[PROOF STATE]
proof (state)
this:
J.arr ?j1 \<Longrightarrow> Cls.comp (\<pi> ?j1) f = \<pi> ?j1 \<cdot> f

goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
J.arr ?j1 \<Longrightarrow> Cls.comp (\<pi> ?j1) f = \<pi> ?j1 \<cdot> f

goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)
[PROOF STEP]
using null_char
[PROOF STATE]
proof (prove)
using this:
J.arr ?j1 \<Longrightarrow> Cls.comp (\<pi> ?j1) f = \<pi> ?j1 \<cdot> f
null = Cls.null

goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)

goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>j. if J.arr j then Cls.comp (\<pi> j) f else Cls.null) = (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null)

goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
have "... = D.cones_map f \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>
[PROOF STEP]
have "\<pi> \<in> D.cones (cod f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> \<in> D.cones (cod f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> \<in> D.cones (cod f)
[PROOF STEP]
have "\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright>
[PROOF STEP]
using f 2 in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C \<chi>'.ide_apex ideD(1)
[PROOF STATE]
proof (prove)
using this:
Cls.in_hom f a \<Pi>D
ide \<Pi>D
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)
ide a
ide ?a \<Longrightarrow> arr ?a

goal (1 subgoal):
 1. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright>

goal (1 subgoal):
 1. \<pi> \<in> D.cones (cod f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright>

goal (1 subgoal):
 1. \<pi> \<in> D.cones (cod f)
[PROOF STEP]
using f \<pi>'.cone_axioms
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright>
Cls.in_hom f a \<Pi>D
D.cone \<Pi>D \<pi>

goal (1 subgoal):
 1. \<pi> \<in> D.cones (cod f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> \<in> D.cones (cod f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<pi> \<in> D.cones (cod f)

goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<pi> \<in> D.cones (cod f)

goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>
[PROOF STEP]
using \<open>\<pi> \<in> D.cones (cod f)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> \<in> D.cones (cod f)
\<pi> \<in> D.cones (cod f)

goal (1 subgoal):
 1. (\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>j. if J.arr j then \<pi> j \<cdot> f else null) = D.cones_map f \<pi>

goal (1 subgoal):
 1. \<And>f. Cls.in_hom f a \<Pi>D \<Longrightarrow> incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
show "incloD.cones_map f \<pi> = D.cones_map f \<pi>"
[PROOF STATE]
proof (prove)
using this:
incloD.cones_map f \<pi> = D.cones_map f \<pi>

goal (1 subgoal):
 1. incloD.cones_map f \<pi> = D.cones_map f \<pi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
incloD.cones_map f \<pi> = D.cones_map f \<pi>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cls.in_hom ?f1 a \<Pi>D \<Longrightarrow> incloD.cones_map ?f1 \<pi> = D.cones_map ?f1 \<pi>

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Cls.in_hom ?f1 a \<Pi>D \<Longrightarrow> incloD.cones_map ?f1 \<pi> = D.cones_map ?f1 \<pi>

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have "\<And>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<Longrightarrow> Cls.in_hom f a \<Pi>D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<Longrightarrow> Cls.in_hom f a \<Pi>D
[PROOF STEP]
using in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. \<And>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<Longrightarrow> Cls.in_hom f a \<Pi>D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<guillemotleft>?f1 : a \<rightarrow> \<Pi>D\<guillemotright> \<Longrightarrow> Cls.in_hom ?f1 a \<Pi>D

goal (1 subgoal):
 1. \<And>a' \<chi>'. D.cone a' \<chi>' \<Longrightarrow> \<exists>!f. \<guillemotleft>f : a' \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
show "\<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have "\<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
using 2 4 5 6 univ \<chi>'.ide_apex ideD(1) in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide \<Pi>D
incloD.mkCone \<chi>' = \<chi>'
D.mkCone \<pi> = \<pi>
Cls.in_hom ?f1 a \<Pi>D \<Longrightarrow> incloD.cones_map ?f1 \<pi> = D.cones_map ?f1 \<pi>
\<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'
ide a
ide ?a \<Longrightarrow> arr ?a
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. \<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
\<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'

goal (1 subgoal):
 1. \<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'

goal (1 subgoal):
 1. \<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
have "\<And>f g. \<lbrakk>\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>';
                                   \<guillemotleft>g : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map g \<pi> = \<chi>'\<rbrakk>
                                     \<Longrightarrow> f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'; \<guillemotleft>g : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map g \<pi> = \<chi>'\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
using 2 4 5 6 univ \<chi>'.ide_apex ideD(1) in_hom_char\<^sub>F\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide \<Pi>D
incloD.mkCone \<chi>' = \<chi>'
D.mkCone \<pi> = \<pi>
Cls.in_hom ?f1 a \<Pi>D \<Longrightarrow> incloD.cones_map ?f1 \<pi> = D.cones_map ?f1 \<pi>
\<exists>!f. Cls.in_hom f a \<Pi>D \<and> incloD.cones_map f \<pi> = incloD.mkCone \<chi>'
ide a
ide ?a \<Longrightarrow> arr ?a
\<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> = (arr ?a \<and> arr ?b \<and> Cls.in_hom ?f ?a ?b)

goal (1 subgoal):
 1. \<And>f g. \<lbrakk>\<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'; \<guillemotleft>g : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map g \<pi> = \<chi>'\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>?f1 : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map ?f1 \<pi> = \<chi>'; \<guillemotleft>?g1 : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map ?g1 \<pi> = \<chi>'\<rbrakk> \<Longrightarrow> ?f1 = ?g1

goal (1 subgoal):
 1. \<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
\<lbrakk>\<guillemotleft>?f1 : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map ?f1 \<pi> = \<chi>'; \<guillemotleft>?g1 : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map ?g1 \<pi> = \<chi>'\<rbrakk> \<Longrightarrow> ?f1 = ?g1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
\<lbrakk>\<guillemotleft>?f1 : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map ?f1 \<pi> = \<chi>'; \<guillemotleft>?g1 : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map ?g1 \<pi> = \<chi>'\<rbrakk> \<Longrightarrow> ?f1 = ?g1

goal (1 subgoal):
 1. \<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!f. \<guillemotleft>f : a \<rightarrow> \<Pi>D\<guillemotright> \<and> D.cones_map f \<pi> = \<chi>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
using \<pi>'.product_cone_axioms has_as_product_def
[PROOF STATE]
proof (prove)
using this:
product_cone J (\<cdot>) D \<Pi>D \<pi>
has_as_product ?J ?D ?a \<equiv> \<exists>\<pi>. product_cone ?J (\<cdot>) ?D ?a \<pi>

goal (1 subgoal):
 1. \<exists>a. has_as_product J D a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>a. has_as_product J D a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. has_as_product J D a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem has_small_limits:
    assumes "category (J :: 'j comp)" and "small (Collect (partial_magma.arr J))"
    shows "has_limits_of_shape J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
interpret J: category J
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category J
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
category J
small (Collect (partial_magma.arr J))

goal (1 subgoal):
 1. category J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
have "small (Collect J.ide)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (Collect J.ide)
[PROOF STEP]
using assms smaller_than_small [of "Collect J.arr" "Collect J.ide"]
[PROOF STATE]
proof (prove)
using this:
category J
small (Collect J.arr)
\<lbrakk>small (Collect J.arr); Collect J.ide \<subseteq> Collect J.arr\<rbrakk> \<Longrightarrow> small (Collect J.ide)

goal (1 subgoal):
 1. small (Collect J.ide)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
small (Collect J.ide)

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
small (Collect J.ide)

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
have "Collect J.ide \<noteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect J.ide \<noteq> UNIV
[PROOF STEP]
using J.ide_def
[PROOF STATE]
proof (prove)
using this:
J.ide ?a \<equiv> J ?a ?a \<noteq> J.null \<and> (\<forall>f. (J f ?a \<noteq> J.null \<longrightarrow> J f ?a = f) \<and> (J ?a f \<noteq> J.null \<longrightarrow> J ?a f = f))

goal (1 subgoal):
 1. Collect J.ide \<noteq> UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Collect J.ide \<noteq> UNIV

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Collect J.ide \<noteq> UNIV

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
have "Collect J.arr \<noteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect J.arr \<noteq> UNIV
[PROOF STEP]
using J.not_arr_null
[PROOF STATE]
proof (prove)
using this:
\<not> J.arr J.null

goal (1 subgoal):
 1. Collect J.arr \<noteq> UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Collect J.arr \<noteq> UNIV

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
small (Collect J.ide)
Collect J.ide \<noteq> UNIV
Collect J.arr \<noteq> UNIV
[PROOF STEP]
show "has_limits_of_shape J"
[PROOF STATE]
proof (prove)
using this:
small (Collect J.ide)
Collect J.ide \<noteq> UNIV
Collect J.arr \<noteq> UNIV

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
using assms has_small_products has_limits_if_has_products [of J]
[PROOF STATE]
proof (prove)
using this:
small (Collect J.ide)
Collect J.ide \<noteq> UNIV
Collect J.arr \<noteq> UNIV
category J
small (Collect J.arr)
\<lbrakk>small ?I; ?I \<noteq> UNIV\<rbrakk> \<Longrightarrow> has_products ?I
\<lbrakk>category J; has_products (Collect J.ide); has_products (Collect J.arr)\<rbrakk> \<Longrightarrow> has_limits_of_shape J

goal (1 subgoal):
 1. has_limits_of_shape J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
has_limits_of_shape J

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_concrete_set_category:
    shows "concrete_set_category comp setp UNIV Cls.UP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concrete_set_category local.comp (\<lambda>A. A \<subseteq> Cls.Univ \<and> small A) UNIV UP
[PROOF STEP]
..


[STATEMENT]
lemma has_ZFC_hom_functor:
    shows "hom_functor C S.comp S.setp Hom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hom_functor (\<cdot>) S.comp (\<lambda>A. A \<subseteq> S.S.Univ \<and> small A) Hom
[PROOF STEP]
..


[STATEMENT]
theorem ZFC_yoneda_lemma:
    assumes "ide a" and "functor Cop.comp S.comp F"
    shows "\<exists>\<phi>. bij_betw \<phi> (S.set (F a)) {\<tau>. natural_transformation Cop.comp S.comp (Y.Y a) F \<tau>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (S.set (F a)) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (S.set (F a)) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
interpret F: "functor" Cop.comp S.comp F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. functor (\<cdot>\<^sup>o\<^sup>p) S.comp F
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
functor (\<cdot>\<^sup>o\<^sup>p) S.comp F

goal (1 subgoal):
 1. functor (\<cdot>\<^sup>o\<^sup>p) S.comp F
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (S.set (F a)) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
interpret F: set_valued_functor Cop.comp S.comp S.setp F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_valued_functor (\<cdot>\<^sup>o\<^sup>p) S.comp (\<lambda>A. A \<subseteq> S.S.Univ \<and> small A) F
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
interpret Ya: yoneda_functor_fixed_object C S.comp S.setp Hom a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yoneda_functor_fixed_object (\<cdot>) S.comp (\<lambda>A. A \<subseteq> S.S.Univ \<and> small A) Hom a
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
ide a

goal (1 subgoal):
 1. yoneda_functor_fixed_object (\<cdot>) S.comp (\<lambda>A. A \<subseteq> S.S.Univ \<and> small A) Hom a
[PROOF STEP]
by unfold_locales blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
interpret Ya: yoneda_lemma C S.comp S.setp Hom F a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yoneda_lemma (\<cdot>) S.comp (\<lambda>A. A \<subseteq> S.S.Univ \<and> small A) Hom F a
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
using Ya.yoneda_lemma
[PROOF STATE]
proof (prove)
using this:
bij_betw Ya.\<T> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}

goal (1 subgoal):
 1. \<exists>\<phi>. bij_betw \<phi> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<phi>. bij_betw \<phi> (F.SET a) {\<tau>. natural_transformation (\<cdot>\<^sup>o\<^sup>p) S.comp (Y.Y a) F \<tau>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_ops_NilI [intro!]:
  shows "insert_ops []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops []
[PROOF STEP]
by (auto simp add: insert_ops_def spec_ops_def)


[STATEMENT]
lemma insert_ops_rem_last [dest]:
  assumes "insert_ops (xs @ [x])"
  shows "insert_ops xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops xs
[PROOF STEP]
using assms insert_ops_def spec_ops_rem_last
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ [x])
insert_ops ?list \<equiv> spec_ops ?list set_option
spec_ops (?xs @ [?x]) ?deps \<Longrightarrow> spec_ops ?xs ?deps

goal (1 subgoal):
 1. insert_ops xs
[PROOF STEP]
by blast


[STATEMENT]
lemma insert_ops_rem_cons:
  assumes "insert_ops (x # xs)"
  shows "insert_ops xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops xs
[PROOF STEP]
using assms insert_ops_def spec_ops_rem_cons
[PROOF STATE]
proof (prove)
using this:
insert_ops (x # xs)
insert_ops ?list \<equiv> spec_ops ?list set_option
spec_ops (?x # ?xs) ?deps \<Longrightarrow> spec_ops ?xs ?deps

goal (1 subgoal):
 1. insert_ops xs
[PROOF STEP]
by blast


[STATEMENT]
lemma insert_ops_appendD:
  assumes "insert_ops (xs @ ys)"
  shows "insert_ops xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (xs @ ys)

goal (1 subgoal):
 1. insert_ops xs
[PROOF STEP]
by (induction ys rule: List.rev_induct,
      auto, metis insert_ops_rem_last append_assoc)


[STATEMENT]
lemma insert_ops_rem_prefix:
  assumes "insert_ops (pre @ suf)"
  shows "insert_ops suf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops suf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ suf)

goal (1 subgoal):
 1. insert_ops suf
[PROOF STEP]
proof(induction pre)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. insert_ops ([] @ suf) \<Longrightarrow> insert_ops suf
 2. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
insert_ops ([] @ suf)

goal (2 subgoals):
 1. insert_ops ([] @ suf) \<Longrightarrow> insert_ops suf
 2. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops ([] @ suf)
[PROOF STEP]
show "insert_ops ([] @ suf) \<Longrightarrow> insert_ops suf"
[PROOF STATE]
proof (prove)
using this:
insert_ops ([] @ suf)

goal (1 subgoal):
 1. insert_ops ([] @ suf) \<Longrightarrow> insert_ops suf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert_ops ([] @ suf) \<Longrightarrow> insert_ops suf

goal (1 subgoal):
 1. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
case (Cons a pre)
[PROOF STATE]
proof (state)
this:
insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf
insert_ops ((a # pre) @ suf)

goal (1 subgoal):
 1. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
have "sorted (map fst suf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (map fst suf)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ suf)

goal (1 subgoal):
 1. sorted (map fst suf)
[PROOF STEP]
by (simp add: insert_ops_def sorted_append spec_ops_def)
[PROOF STATE]
proof (state)
this:
sorted (map fst suf)

goal (1 subgoal):
 1. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted (map fst suf)

goal (1 subgoal):
 1. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
have "distinct (map fst suf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst suf)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ suf)

goal (1 subgoal):
 1. distinct (map fst suf)
[PROOF STEP]
by (simp add: insert_ops_def spec_ops_def)
[PROOF STATE]
proof (state)
this:
distinct (map fst suf)

goal (1 subgoal):
 1. \<And>a pre. \<lbrakk>insert_ops (pre @ suf) \<Longrightarrow> insert_ops suf; insert_ops ((a # pre) @ suf)\<rbrakk> \<Longrightarrow> insert_ops suf
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted (map fst suf)
distinct (map fst suf)
[PROOF STEP]
show "insert_ops ((a # pre) @ suf) \<Longrightarrow> insert_ops suf"
[PROOF STATE]
proof (prove)
using this:
sorted (map fst suf)
distinct (map fst suf)

goal (1 subgoal):
 1. insert_ops ((a # pre) @ suf) \<Longrightarrow> insert_ops suf
[PROOF STEP]
by (simp add: insert_ops_def spec_ops_def)
[PROOF STATE]
proof (state)
this:
insert_ops ((a # pre) @ suf) \<Longrightarrow> insert_ops suf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_ops_remove1:
  assumes "insert_ops xs"
  shows "insert_ops (remove1 x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops (remove1 x xs)
[PROOF STEP]
using assms insert_ops_def spec_ops_remove1
[PROOF STATE]
proof (prove)
using this:
insert_ops xs
insert_ops ?list \<equiv> spec_ops ?list set_option
spec_ops ?xs ?deps \<Longrightarrow> spec_ops (remove1 ?x ?xs) ?deps

goal (1 subgoal):
 1. insert_ops (remove1 x xs)
[PROOF STEP]
by blast


[STATEMENT]
lemma last_op_greatest:
  assumes "insert_ops (op_list @ [(oid, oper)])"
    and "x \<in> set (map fst op_list)"
  shows "x < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < oid
[PROOF STEP]
using assms spec_ops_id_inc insert_ops_def
[PROOF STATE]
proof (prove)
using this:
insert_ops (op_list @ [(oid, oper)])
x \<in> set (map fst op_list)
\<lbrakk>spec_ops (?xs @ [(?oid, ?oper)]) ?deps; ?x \<in> set (map fst ?xs)\<rbrakk> \<Longrightarrow> ?x < ?oid
insert_ops ?list \<equiv> spec_ops ?list set_option

goal (1 subgoal):
 1. x < oid
[PROOF STEP]
by metis


[STATEMENT]
lemma insert_ops_ref_older:
  assumes "insert_ops (pre @ [(oid, Some ref)] @ suf)"
  shows "ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops (pre @ [(oid, Some ref)] @ suf)

goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
by (auto simp add: insert_ops_def spec_ops_def)


[STATEMENT]
lemma insert_ops_memb_ref_older:
  assumes "insert_ops op_list"
    and "(oid, Some ref) \<in> set op_list"
  shows "ref < oid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
using assms insert_ops_ref_older split_list_first
[PROOF STATE]
proof (prove)
using this:
insert_ops op_list
(oid, Some ref) \<in> set op_list
insert_ops (?pre @ [(?oid, Some ?ref)] @ ?suf) \<Longrightarrow> ?ref < ?oid
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys

goal (1 subgoal):
 1. ref < oid
[PROOF STEP]
by fastforce


[STATEMENT]
lemma insert_spec_none [simp]:
  shows "set (insert_spec xs (oid, None)) = set xs \<union> {oid}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert_spec xs (oid, None)) = set xs \<union> {oid}
[PROOF STEP]
by (induction xs, auto simp add: insert_commute sup_commute)


[STATEMENT]
lemma insert_spec_set [simp]:
  assumes "ref \<in> set xs"
  shows "set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ref \<in> set xs

goal (1 subgoal):
 1. set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref \<in> set [] \<Longrightarrow> set (insert_spec [] (oid, Some ref)) = set [] \<union> {oid}
 2. \<And>a xs. \<lbrakk>ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}; ref \<in> set (a # xs)\<rbrakk> \<Longrightarrow> set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
assume "ref \<in> set []"
[PROOF STATE]
proof (state)
this:
ref \<in> set []

goal (2 subgoals):
 1. ref \<in> set [] \<Longrightarrow> set (insert_spec [] (oid, Some ref)) = set [] \<union> {oid}
 2. \<And>a xs. \<lbrakk>ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}; ref \<in> set (a # xs)\<rbrakk> \<Longrightarrow> set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
thus "set (insert_spec [] (oid, Some ref)) = set [] \<union> {oid}"
[PROOF STATE]
proof (prove)
using this:
ref \<in> set []

goal (1 subgoal):
 1. set (insert_spec [] (oid, Some ref)) = set [] \<union> {oid}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (insert_spec [] (oid, Some ref)) = set [] \<union> {oid}

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}; ref \<in> set (a # xs)\<rbrakk> \<Longrightarrow> set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}; ref \<in> set (a # xs)\<rbrakk> \<Longrightarrow> set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
fix a xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}; ref \<in> set (a # xs)\<rbrakk> \<Longrightarrow> set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
assume "ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}"
    and "ref \<in> set (a#xs)"
[PROOF STATE]
proof (state)
this:
ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}
ref \<in> set (a # xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}; ref \<in> set (a # xs)\<rbrakk> \<Longrightarrow> set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
thus "set (insert_spec (a#xs) (oid, Some ref)) = set (a#xs) \<union> {oid}"
[PROOF STATE]
proof (prove)
using this:
ref \<in> set xs \<Longrightarrow> set (insert_spec xs (oid, Some ref)) = set xs \<union> {oid}
ref \<in> set (a # xs)

goal (1 subgoal):
 1. set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}
[PROOF STEP]
by(cases "a = ref", auto simp add: insert_commute sup_commute)
[PROOF STATE]
proof (state)
this:
set (insert_spec (a # xs) (oid, Some ref)) = set (a # xs) \<union> {oid}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_spec_nonex [simp]:
  assumes "ref \<notin> set xs"
  shows "insert_spec xs (oid, Some ref) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec xs (oid, Some ref) = xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ref \<notin> set xs

goal (1 subgoal):
 1. insert_spec xs (oid, Some ref) = xs
[PROOF STEP]
proof(induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ref \<notin> set [] \<Longrightarrow> insert_spec [] (oid, Some ref) = []
 2. \<And>a xs. \<lbrakk>ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs; ref \<notin> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec (a # xs) (oid, Some ref) = a # xs
[PROOF STEP]
show "insert_spec [] (oid, Some ref) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_spec [] (oid, Some ref) = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
insert_spec [] (oid, Some ref) = []

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs; ref \<notin> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec (a # xs) (oid, Some ref) = a # xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs; ref \<notin> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec (a # xs) (oid, Some ref) = a # xs
[PROOF STEP]
fix a xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs; ref \<notin> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec (a # xs) (oid, Some ref) = a # xs
[PROOF STEP]
assume "ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs"
    and "ref \<notin> set (a#xs)"
[PROOF STATE]
proof (state)
this:
ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs
ref \<notin> set (a # xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs; ref \<notin> set (a # xs)\<rbrakk> \<Longrightarrow> insert_spec (a # xs) (oid, Some ref) = a # xs
[PROOF STEP]
thus "insert_spec (a#xs) (oid, Some ref) = a#xs"
[PROOF STATE]
proof (prove)
using this:
ref \<notin> set xs \<Longrightarrow> insert_spec xs (oid, Some ref) = xs
ref \<notin> set (a # xs)

goal (1 subgoal):
 1. insert_spec (a # xs) (oid, Some ref) = a # xs
[PROOF STEP]
by(cases "a = ref", auto simp add: insert_commute sup_commute)
[PROOF STATE]
proof (state)
this:
insert_spec (a # xs) (oid, Some ref) = a # xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_greater_non_memb:
  fixes oid :: "'oid::{linorder}"
  assumes "\<And>x. x \<in> set xs \<Longrightarrow> x < oid"
    and "oid \<in> set xs"
  shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> ?x < oid
oid \<in> set xs

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast