[STATEMENT]
lemma the_cf_rKe_ArrMap_app:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'"
    and "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>"
    and "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_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> :
    lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>"
    and
      "lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F
          ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)"
    and
      "\<lbrakk>
        f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>;
        lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
       \<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> &&& lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>) &&& (\<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[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 (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[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 (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
interpret u: is_cat_limit
    \<alpha> \<open>c \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>lim_Obj c\<lparr>UObj\<rparr>\<close> \<open>lim_Obj c\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : c \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(4))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
interpret u': is_cat_limit
    \<alpha> \<open>c' \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>lim_Obj c'\<lparr>UObj\<rparr>\<close> \<open>lim_Obj c'\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(5))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[PROOF STEP]
have c: "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>" and c': "c' \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> &&& c' \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
c' \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
note the_cf_rKe_ArrMap_app_impl' =
    the_cf_rKe_ArrMap_app_impl[OF assms]
[PROOF STATE]
proof (state)
this:
\<exists>!f. f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f

goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
note the_f = theI'[OF the_cf_rKe_ArrMap_app_impl[OF assms]]
[PROOF STATE]
proof (state)
this:
(THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x) : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x)

goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
note the_f_is_arr = the_f[THEN conjunct1]
    and the_f_commutes = the_f[THEN conjunct2]
[PROOF STATE]
proof (state)
this:
(THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x) : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x)

goal (3 subgoals):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
 2. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 3. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
from assms(3) the_f_is_arr
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
(THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x) : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
[PROOF STEP]
show
    "the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> :
      lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
(THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x) : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>

goal (1 subgoal):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: the_cf_rKe_ArrMap_app' cs_intro: cat_cs_intros
      )
[PROOF STATE]
proof (state)
this:
the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>

goal (2 subgoals):
 1. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 2. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>

goal (2 subgoals):
 1. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
 2. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
from assms(3) the_f_commutes
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x)
[PROOF STEP]
show
    "lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F
        ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (THE x. x : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr> \<and> lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> x)

goal (1 subgoal):
 1. lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: the_cf_rKe_ArrMap_app' cs_intro: cat_cs_intros
      )
[PROOF STATE]
proof (state)
this:
lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)

goal (1 subgoal):
 1. \<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)
[PROOF STEP]
show "f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>"
    if "f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>"
      and "lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f"
[PROOF STATE]
proof (prove)
using this:
the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>)

goal (1 subgoal):
 1. f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
[PROOF STEP]
by (metis that the_cf_rKe_ArrMap_app_impl')
[PROOF STATE]
proof (state)
this:
\<lbrakk>f : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>; lim_Obj c\<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 c'\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f\<rbrakk> \<Longrightarrow> f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_cf_rKe_ArrMap_is_arr'[cat_Kan_cs_intros]:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'"
    and "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>"
    and "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>"
    and "a = lim_Obj c\<lparr>UObj\<rparr>"
    and "b = lim_Obj c'\<lparr>UObj\<rparr>"
  shows "the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
unfolding assms(6,7)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> : lim_Obj c\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj c'\<lparr>UObj\<rparr>
[PROOF STEP]
by (rule the_cf_rKe_ArrMap_app[OF assms(1-5)])


[STATEMENT]
lemma lim_Obj_the_cf_rKe_commute:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "lim_Obj a\<lparr>UArr\<rparr> :
      lim_Obj a\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>C\<^sub>F a \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : a \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "lim_Obj b\<lparr>UArr\<rparr> :
      lim_Obj b\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>C\<^sub>F b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : b \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
    and "[a', b', f']\<^sub>\<circ> \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
  shows
    "lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> =
      lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub>
        the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[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. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[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. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
note f = \<KK>.HomCod.cat_is_arrD[OF assms(5)]
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<CC>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
\<CC>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b

goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
interpret lim_a: is_cat_limit
    \<alpha> \<open>a \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F a \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>lim_Obj a\<lparr>UObj\<rparr>\<close> \<open>lim_Obj a\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr> : lim_Obj a\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M a \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : a \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
interpret lim_b: is_cat_limit
    \<alpha> \<open>b \<down>\<^sub>C\<^sub>F \<KK>\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>\<close> \<open>lim_Obj b\<lparr>UObj\<rparr>\<close> \<open>lim_Obj b\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj b\<lparr>UArr\<rparr> : lim_Obj b\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : b \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(4))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
note f_app = the_cf_rKe_ArrMap_app[
      where lim_Obj=lim_Obj, OF assms(1,2,5,3,4)
      ]
[PROOF STATE]
proof (state)
this:
the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : lim_Obj a\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj b\<lparr>UObj\<rparr>
lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
\<lbrakk>?f : lim_Obj a\<lparr>UObj\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> lim_Obj b\<lparr>UObj\<rparr>; lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> ?f\<rbrakk> \<Longrightarrow> ?f = the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
from f_app(2)
[PROOF STATE]
proof (chain)
picking this:
lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
[PROOF STEP]
have lim_a_f\<KK>_NTMap_app:
    "(lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>NTMap\<rparr>\<lparr>A\<rparr> =
      (
        lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F
        ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
      )\<lparr>NTMap\<rparr>\<lparr>A\<rparr>"
    if \<open>A \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>\<close> for A
[PROOF STATE]
proof (prove)
using this:
lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)

goal (1 subgoal):
 1. (lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>NTMap\<rparr>\<lparr>A\<rparr> = (lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>))\<lparr>NTMap\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?A \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>NTMap\<rparr>\<lparr>?A\<rparr> = (lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>))\<lparr>NTMap\<rparr>\<lparr>?A\<rparr>

goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
show
    "lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> =
      lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub>
        the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
from assms(5,6)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[a', b', f']\<^sub>\<circ> \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
have a'_def: "a' = 0"
      and b': "b' \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
      and f': "f' : b \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[a', b', f']\<^sub>\<circ> \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a' = []\<^sub>\<circ> &&& b' \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> &&& f' : b \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a' = []\<^sub>\<circ>
b' \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
f' : b \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>

goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
show
      "lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> =
        lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr>\<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub>
          the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
using lim_a_f\<KK>_NTMap_app[OF assms(6)] f' assms(3-6)
[PROOF STATE]
proof (prove)
using this:
(lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> = (lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>))\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet>
f' : b \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
lim_Obj a\<lparr>UArr\<rparr> : lim_Obj a\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M a \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : a \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
lim_Obj b\<lparr>UArr\<rparr> : lim_Obj b\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : b \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[a', b', f']\<^sub>\<circ> \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
unfolding a'_def
[PROOF STATE]
proof (prove)
using this:
(lim_Obj a\<lparr>UArr\<rparr> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M f \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b', f'\<rparr>\<^sub>\<bullet> = (lim_Obj b\<lparr>UArr\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (b \<down>\<^sub>C\<^sub>F \<KK>) \<AA> (the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>))\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b', f'\<rparr>\<^sub>\<bullet>
f' : b \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
lim_Obj a\<lparr>UArr\<rparr> : lim_Obj a\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M a \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : a \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
lim_Obj b\<lparr>UArr\<rparr> : lim_Obj b\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M b \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : b \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[[]\<^sub>\<circ>, b', f']\<^sub>\<circ> \<in>\<^sub>\<circ> b \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>[]\<^sub>\<circ>, b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
by
        (
          cs_prems
            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:
lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lim_Obj a\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f' \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f\<rparr>\<^sub>\<bullet> = lim_Obj b\<lparr>UArr\<rparr>\<lparr>NTMap\<rparr> \<lparr>a', b', f'\<rparr>\<^sub>\<bullet> \<circ>\<^sub>A\<^bsub>\<AA>\<^esub> the_cf_rKe \<alpha> \<TT> \<KK> lim_Obj\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed