[STATEMENT]
lemma the_cf_lKe_is_functor:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<And>c. c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> lim_Obj c\<lparr>UArr\<rparr> :
      \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
assume prems: "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from assms(3)[OF this]
[PROOF STATE]
proof (chain)
picking this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have lim_Obj_UArr: "lim_Obj c\<lparr>UArr\<rparr> :
      \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret lim_Obj_c: 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> \<open>lim_Obj c\<lparr>UObj\<rparr>\<close> \<open>lim_Obj c\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
using this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
note op_ua_UArr_is_cat_limit'[
      where lim_Obj=lim_Obj, OF assms(1,2) prems lim_Obj_UArr
      ]
[PROOF STATE]
proof (state)
this:
op_ua lim_Obj \<KK> c\<lparr>UArr\<rparr> : lim_Obj c\<lparr>UObj\<rparr> <\<^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 (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?c2 \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> op_ua lim_Obj \<KK> ?c2\<lparr>UArr\<rparr> : lim_Obj ?c2\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?c2 \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : ?c2 \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
note the_cf_rKe_is_functor = the_cf_rKe_is_functor
    [
      OF \<KK>.is_functor_op \<TT>.is_functor_op,
      unfolded cat_op_simps,
      where lim_Obj=\<open>op_ua lim_Obj \<KK>\<close>,
      unfolded cat_op_simps,
      OF this,
      simplified,
      folded the_cf_lKe_def
    ]
[PROOF STATE]
proof (state)
this:
the_cf_rKe \<alpha> (op_cf \<TT>) (op_cf \<KK>) (op_ua lim_Obj \<KK>) : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
      (
        rule is_functor.is_functor_op
          [
            OF the_cf_rKe_is_functor,
            folded the_cf_lKe_def,
            unfolded cat_op_simps
          ]
      )
[PROOF STATE]
proof (state)
this:
the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_ntcf_rKe_is_ntcf:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<And>c. c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> lim_Obj c\<lparr>UArr\<rparr> :
      lim_Obj c\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : c \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj :
    the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
let ?UObj = \<open>\<lambda>a. lim_Obj a\<lparr>UObj\<rparr>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
let ?UArr = \<open>\<lambda>a. lim_Obj a\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
let ?const_comma = \<open>\<lambda>a b. cf_const (a \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (?UObj b)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
let ?the_cf_rKe = \<open>the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
let ?the_ntcf_rKe = \<open>the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret cf_rKe: is_functor \<alpha> \<CC> \<AA> \<open>?the_cf_rKe\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule the_cf_rKe_is_functor[OF assms, simplified])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(rule is_ntcfI')
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj)
 3. vcard (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj) = 5\<^sub>\<nat>
 4. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 5. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 6. 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>
 7. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT>
 8. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<BB>
 9. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<AA>
 10. vsv (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>)
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence ?the_ntcf_rKe"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj)
[PROOF STEP]
unfolding the_ntcf_rKe_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<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_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>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. vcard (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj) = 5\<^sub>\<nat>
 3. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 5. 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>
 6. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT>
 7. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<BB>
 8. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<AA>
 9. vsv (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>)
 10. \<D>\<^sub>\<circ> (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard ?the_ntcf_rKe = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding the_ntcf_rKe_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<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_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> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj) = 5\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. 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>
 5. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT>
 6. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<BB>
 7. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<AA>
 8. vsv (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>)
 9. \<D>\<^sub>\<circ> (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 10. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
A total of 11 subgoals...
[PROOF STEP]
show "?the_ntcf_rKe\<lparr>NTMap\<rparr>\<lparr>b\<rparr> :
      (?the_cf_rKe \<circ>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
      if "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
let ?\<KK>b = \<open>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
have \<KK>b: "\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
note lim_\<KK>b = assms(3)[OF \<KK>b]
[PROOF STATE]
proof (state)
this:
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
interpret lim_\<KK>b: is_cat_limit
        \<alpha> \<open>?\<KK>b \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F ?\<KK>b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>?UObj ?\<KK>b\<close> \<open>?UArr ?\<KK>b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule lim_\<KK>b)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
from that lim_\<KK>b
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_comma_cs_simps cat_Kan_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros cat_Kan_cs_intros
          )+
[PROOF STATE]
proof (state)
this:
the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> : (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<TT>\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. 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>
 5. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT>
 6. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<BB>
 7. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<AA>
 8. vsv (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>)
 9. \<D>\<^sub>\<circ> (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<BB>\<^esub> b \<Longrightarrow> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show
      "?the_ntcf_rKe\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (?the_cf_rKe \<circ>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
        \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> ?the_ntcf_rKe\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
      if "f : a \<mapsto>\<^bsub>\<BB>\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
let ?\<KK>a = \<open>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<close> and ?\<KK>b = \<open>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<close> and ?\<KK>f = \<open>\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
have \<KK>a: "?\<KK>a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
        and \<KK>b: "?\<KK>b \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
        and \<KK>f: "?\<KK>f : ?\<KK>a \<mapsto>\<^bsub>\<CC>\<^esub> ?\<KK>b"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> &&& \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> &&& \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
note lim_\<KK>a = assms(3)[OF \<KK>a]
        and lim_\<KK>b = assms(3)[OF \<KK>b]
[PROOF STATE]
proof (state)
this:
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
have z_b_\<KK>b: "[0, b, \<CC>\<lparr>CId\<rparr>\<lparr>?\<KK>b\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> ?\<KK>b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. [[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros cat_comma_cs_intros)
[PROOF STATE]
proof (state)
this:
[[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from
        lim_Obj_the_cf_rKe_commute[
          OF assms(1,2) lim_\<KK>a lim_\<KK>b \<KK>f z_b_\<KK>b, symmetric
          ]
        that
[PROOF STATE]
proof (chain)
picking this:
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet>
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
have [cat_Kan_cs_simps]:
        "?UArr ?\<KK>b\<lparr>NTMap\<rparr>\<lparr>0, b, \<CC>\<lparr>CId\<rparr>\<lparr>?\<KK>b\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> ?the_cf_rKe\<lparr>ArrMap\<rparr>\<lparr>?\<KK>f\<rparr> =
          ?UArr ?\<KK>a\<lparr>NTMap\<rparr>\<lparr>0, b, ?\<KK>f\<rparr>\<^sub>\<bullet>"
[PROOF STATE]
proof (prove)
using this:
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet>
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
interpret lim_\<KK>a: is_cat_limit
        \<alpha> \<open>?\<KK>a \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F ?\<KK>a \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>?UObj ?\<KK>a\<close> \<open>?UArr ?\<KK>a\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule lim_\<KK>a)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
interpret lim_\<KK>b: is_cat_limit
        \<alpha> \<open>?\<KK>b \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F ?\<KK>b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>?UObj ?\<KK>b\<close> \<open>?UArr ?\<KK>b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr> : lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule lim_\<KK>b)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
note lim_\<KK>a.cat_cone_Comp_commute[cat_cs_simps del]
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>(\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>\<^esub> ?b \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>?b\<rparr>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
note lim_\<KK>b.cat_cone_Comp_commute[cat_cs_simps del]
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>(\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>\<^esub> ?b \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>?b\<rparr>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
have
        "[[0, a, \<CC>\<lparr>CId\<rparr>\<lparr>?\<KK>a\<rparr>]\<^sub>\<circ>, [0, b, ?\<KK>f]\<^sub>\<circ>, [0, f]\<^sub>\<circ>]\<^sub>\<circ> :
          [0, a, \<CC>\<lparr>CId\<rparr>\<lparr>?\<KK>a\<rparr>]\<^sub>\<circ> \<mapsto>\<^bsub>(?\<KK>a) \<down>\<^sub>C\<^sub>F \<KK>\<^esub> [0, b, ?\<KK>f]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. [[[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, f]\<^sub>\<circ>]\<^sub>\<circ> : [[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ> \<mapsto>\<^bsub>(\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>\<^esub> [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
[[[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, f]\<^sub>\<circ>]\<^sub>\<circ> : [[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ> \<mapsto>\<^bsub>(\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>\<^esub> [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from lim_\<KK>a.ntcf_Comp_commute[OF this, symmetric] that
[PROOF STATE]
proof (chain)
picking this:
(\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, f]\<^sub>\<circ>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> dghm_const ((\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UObj\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UObj\<rparr>\<rparr>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, f]\<^sub>\<circ>\<rparr>\<^sub>\<bullet>
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
have [cat_Kan_cs_simps]:
        "\<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> ?UArr (?\<KK>a)\<lparr>NTMap\<rparr> \<lparr>0, a, \<CC>\<lparr>CId\<rparr>\<lparr>?\<KK>a\<rparr>\<rparr>\<^sub>\<bullet> =
          ?UArr ?\<KK>a\<lparr>NTMap\<rparr>\<lparr>0, b, ?\<KK>f\<rparr>\<^sub>\<bullet>"
[PROOF STATE]
proof (prove)
using this:
(\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, f]\<^sub>\<circ>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> dghm_const ((\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UObj\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UObj\<rparr>\<rparr>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>, [[]\<^sub>\<circ>, f]\<^sub>\<circ>\<rparr>\<^sub>\<bullet>
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by
          (
            cs_prems
              cs_simp: cat_cs_simps cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros cat_1_is_arrI
          )
[PROOF STATE]
proof (state)
this:
\<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, a, \<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>\<rparr>\<^sub>\<bullet> = lim_Obj (\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<^sub>\<bullet>

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
          )
[PROOF STATE]
proof (state)
this:
the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b \<Longrightarrow> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = \<TT>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. 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>
 5. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTCod\<rparr> = \<TT>
 6. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGDom\<rparr> = \<BB>
 7. the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTDGCod\<rparr> = \<AA>
 8. vsv (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>)
 9. \<D>\<^sub>\<circ> (the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>NTMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
qed
    (
      cs_concl
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+
[PROOF STATE]
proof (state)
this:
the_ntcf_rKe \<alpha> \<TT> \<KK> lim_Obj : the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_ntcf_lKe_is_ntcf:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<And>c. c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> lim_Obj c\<lparr>UArr\<rparr> :
      \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj :
    \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<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. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
assume prems: "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from assms(3)[OF this]
[PROOF STATE]
proof (chain)
picking this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have lim_Obj_UArr: "lim_Obj c\<lparr>UArr\<rparr> :
      \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret lim_Obj_c: 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> \<open>lim_Obj c\<lparr>UObj\<rparr>\<close> \<open>lim_Obj c\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
using this:
lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. lim_Obj c\<lparr>UArr\<rparr> : \<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 lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
note op_ua_UArr_is_cat_limit'[
      where lim_Obj=lim_Obj, OF assms(1,2) prems lim_Obj_UArr
      ]
[PROOF STATE]
proof (state)
this:
op_ua lim_Obj \<KK> c\<lparr>UArr\<rparr> : lim_Obj c\<lparr>UObj\<rparr> <\<^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 (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?c2 \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> op_ua lim_Obj \<KK> ?c2\<lparr>UArr\<rparr> : lim_Obj ?c2\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?c2 \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : ?c2 \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
note the_ntcf_rKe_is_ntcf = the_ntcf_rKe_is_ntcf
    [
      OF \<KK>.is_functor_op \<TT>.is_functor_op,
      unfolded cat_op_simps,
      where lim_Obj=\<open>op_ua lim_Obj \<KK>\<close>,
      unfolded cat_op_simps,
      OF this,
      simplified
    ]
[PROOF STATE]
proof (state)
this:
the_ntcf_rKe \<alpha> (op_cf \<TT>) (op_cf \<KK>) (op_ua lim_Obj \<KK>) : the_cf_rKe \<alpha> (op_cf \<TT>) (op_cf \<KK>) (op_ua lim_Obj \<KK>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj :
    \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
      (
        rule is_ntcf.is_ntcf_op
          [
            OF the_ntcf_rKe_is_ntcf,
            unfolded cat_op_simps,
            folded the_cf_lKe_def the_ntcf_lKe_def
          ]
       )
[PROOF STATE]
proof (state)
this:
the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed