[STATEMENT]
lemma op_ua_UArr_is_cat_limit:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
    and "u : \<TT> \<circ>\<^sub>C\<^sub>F \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "op_ntcf u \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F inv_cf (op_cf_obj_comma \<KK> c) :
    r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
note [cf_cs_simps] = is_iso_functor_is_iso_arr(2,3)
[PROOF STATE]
proof (state)
this:
?\<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> inv_dghm ?\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<FF> = dghm_id ?\<AA>
?\<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> ?\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm ?\<FF> = dghm_id ?\<BB>

goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
let ?op_\<KK> = \<open>\<lambda>c. op_cf_obj_comma \<KK> c\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
let ?op_\<KK>c = \<open>?op_\<KK> c\<close>
    and ?op_ua_UArr = \<open>op_ntcf u \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F inv_cf (op_cf_obj_comma \<KK> c)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<BB> \<CC> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
interpret \<TT>: is_functor \<alpha> \<BB> \<AA> \<TT>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
interpret u: is_cat_colimit \<alpha> \<open>\<KK> \<^sub>C\<^sub>F\<down> c\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c\<close> r u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(4))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
from \<KK>.op_cf_cf_obj_comma_proj[OF assms(3)]
[PROOF STATE]
proof (chain)
picking this:
op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf_obj_comma \<KK> c
[PROOF STEP]
have
    "op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>C\<^sub>F inv_cf (?op_\<KK> c) =
      c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>C\<^sub>F (?op_\<KK> c) \<circ>\<^sub>C\<^sub>F inv_cf (?op_\<KK> c)"
[PROOF STATE]
proof (prove)
using this:
op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf_obj_comma \<KK> c

goal (1 subgoal):
 1. op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf_obj_comma \<KK> c \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf_obj_comma \<KK> c \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)

goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
from this assms(3)
[PROOF STATE]
proof (chain)
picking this:
op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf_obj_comma \<KK> c \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
have [cat_comma_cs_simps]:
    "op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>C\<^sub>F inv_cf (?op_\<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>)"
[PROOF STATE]
proof (prove)
using this:
op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf_obj_comma \<KK> c \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>)
[PROOF STEP]
by
      (
        cs_prems
          cs_simp: cat_cs_simps cat_comma_cs_simps cf_cs_simps cat_op_simps
          cs_intro: cf_cs_intros cat_cs_intros cat_comma_cs_intros cat_op_intros
      )
[PROOF STATE]
proof (state)
this:
op_cf (\<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) = c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>)

goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
show "?op_ua_UArr :
    r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
by
      (
        cs_concl
          cs_simp:
            cf_cs_simps cat_cs_simps cat_comma_cs_simps cat_op_simps
            \<KK>.op_cf_cf_obj_comma_proj[symmetric]
          cs_intro:
            cat_cs_intros
            cf_cs_intros
            cat_lim_cs_intros
            cat_comma_cs_intros
            cat_op_intros
      )
[PROOF STATE]
proof (state)
this:
op_ntcf u \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c) : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_cf_rKe_components:
  shows "the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ObjMap\<rparr> =
    (\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>HomCod\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>)"
    and "the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr> =
    (
      \<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>HomCod\<rparr>\<lparr>Arr\<rparr>. THE f.
        f :
          lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>HomCod\<rparr>\<^esub>
          lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and>
        lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> =
          lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F
          ntcf_const ((\<KK>\<lparr>HomCod\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>HomCod\<rparr>) f
    )"
    and "the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>HomDom\<rparr> = \<KK>\<lparr>HomCod\<rparr>"
    and "the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>HomCod\<rparr> = \<TT>\<lparr>HomCod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ObjMap\<rparr> = (\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>HomCod\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>) &&& the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr> = (\<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>HomCod\<rparr>\<lparr>Arr\<rparr>. THE f. f : lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>HomCod\<rparr>\<^esub> lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and> lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj (\<KK>\<lparr>HomCod\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const ((\<KK>\<lparr>HomCod\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>HomCod\<rparr>) f)) &&& the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>HomDom\<rparr> = \<KK>\<lparr>HomCod\<rparr> &&& the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>HomCod\<rparr> = \<TT>\<lparr>HomCod\<rparr>
[PROOF STEP]
unfolding the_cf_rKe_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>, \<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Arr\<rparr>. THE f. f : lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>3\<^sub>\<nat>\<rparr>\<^esub> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const ((\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>3\<^sub>\<nat>\<rparr>) f, \<KK>\<lparr>3\<^sub>\<nat>\<rparr>, \<TT>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>) &&& [\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>, \<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Arr\<rparr>. THE f. f : lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>3\<^sub>\<nat>\<rparr>\<^esub> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const ((\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>3\<^sub>\<nat>\<rparr>) f, \<KK>\<lparr>3\<^sub>\<nat>\<rparr>, \<TT>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Arr\<rparr>. THE f. f : lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>3\<^sub>\<nat>\<rparr>\<^esub> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const ((\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>3\<^sub>\<nat>\<rparr>) f)) &&& [\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>, \<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Arr\<rparr>. THE f. f : lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>3\<^sub>\<nat>\<rparr>\<^esub> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const ((\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>3\<^sub>\<nat>\<rparr>) f, \<KK>\<lparr>3\<^sub>\<nat>\<rparr>, \<TT>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<KK>\<lparr>3\<^sub>\<nat>\<rparr> &&& [\<lambda>c\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>, \<lambda>g\<in>\<^sub>\<circ>\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Arr\<rparr>. THE f. f : lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<TT>\<lparr>3\<^sub>\<nat>\<rparr>\<^esub> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UObj\<rparr> \<and> lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Dom\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj (\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>)\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const ((\<KK>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Cod\<rparr>\<lparr>g\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) (\<TT>\<lparr>3\<^sub>\<nat>\<rparr>) f, \<KK>\<lparr>3\<^sub>\<nat>\<rparr>, \<TT>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<TT>\<lparr>3\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma the_ntcf_rKe_components:
  shows "the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr> =
      (
        \<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>.
          lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>0, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>
      )"
    and "the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDom\<rparr> = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK>"
    and "the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT>"
    and "the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<TT>\<lparr>HomDom\<rparr>"
    and "the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<TT>\<lparr>HomCod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr> = (\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>) &&& the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDom\<rparr> = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) &&& the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT> &&& the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<TT>\<lparr>HomDom\<rparr> &&& the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<TT>\<lparr>HomCod\<rparr>
[PROOF STEP]
unfolding the_ntcf_rKe_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>, the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>, \<TT>, \<TT>\<lparr>HomDom\<rparr>, \<TT>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>) &&& [\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>, the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>, \<TT>, \<TT>\<lparr>HomDom\<rparr>, \<TT>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) &&& [\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>, the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>, \<TT>, \<TT>\<lparr>HomDom\<rparr>, \<TT>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<TT> &&& [\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>, the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>, \<TT>, \<TT>\<lparr>HomDom\<rparr>, \<TT>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<TT>\<lparr>HomDom\<rparr> &&& [\<lambda>c\<in>\<^sub>\<circ>\<TT>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>)\<lparr>UArr\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<lparr>[]\<^sub>\<circ>, c, \<KK>\<lparr>HomCod\<rparr>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>\<rparr>\<^sub>\<bullet>, the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>, \<TT>, \<TT>\<lparr>HomDom\<rparr>, \<TT>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = \<TT>\<lparr>HomCod\<rparr>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma the_cf_rKe_ObjMap_vrange:
  assumes "\<And>c. c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> lim_Obj c\<lparr>UObj\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "\<R>\<^sub>\<circ> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding the_cf_rKe_components'[OF \<KK> \<TT>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>c\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. lim_Obj c\<lparr>UObj\<rparr>) \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (intro vrange_VLambda_vsubset assms)


[STATEMENT]
lemma g': "g \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. g \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto