[STATEMENT]
lemma the_cf_rKe_ArrMap_app_impl:
  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 "u : r <\<^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 "u' : r' <\<^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 "\<exists>!f.
    f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and>
    u \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[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. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[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. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[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> r u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u : r <\<^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 (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[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> r' u'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' : r' <\<^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 (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[PROOF STEP]
have const_r_def:
    "cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r = cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) = dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>
[PROOF STEP]
proof(rule cf_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 4. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show const_r: "cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (5 subgoals):
 1. dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 3. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 4. c' \<down>\<^sub>C\<^sub>F \<KK> = ?\<CC>
 5. \<AA> = ?\

[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[PROOF STEP]
show const_r_g\<KK>:
      "cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros cat_comma_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (4 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
have ObjMap_dom_lhs: "\<D>\<^sub>\<circ> (cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[PROOF STEP]
have ObjMap_dom_rhs:
      "\<D>\<^sub>\<circ> ((cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
have ArrMap_dom_lhs: "\<D>\<^sub>\<circ> (cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[PROOF STEP]
have ArrMap_dom_rhs:
      "\<D>\<^sub>\<circ> ((cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
show
      "cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ObjMap\<rparr> =
        (cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>)
 2. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>)
 2. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>)
 2. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from prems assms
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
obtain b f
        where A_def: "A = [0, b, f]\<^sub>\<circ>"
          and b: "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
          and f: "f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. (\<And>b f. \<lbrakk>A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (4 subgoals):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>)
 2. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms(1,3) prems f b
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show
        "cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ObjMap\<rparr>\<lparr>A\<rparr> =
          (cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[[]\<^sub>\<circ>, b, f]\<^sub>\<circ> \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, f\<rparr>\<^sub>\<bullet> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, f\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: cat_cs_simps cat_comma_cs_simps
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>

goal (3 subgoals):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr>)
 2. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
qed
      (
        use assms(3) in
          \<open>cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros\<close>
      )+
[PROOF STATE]
proof (state)
this:
dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ObjMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 2. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 3. \<AA> = \<AA>
[PROOF STEP]
show
      "cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ArrMap\<rparr> =
        (cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>)
 2. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "vsv (cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
vsv (dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>)

goal (3 subgoals):
 1. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
 2. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 3. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[PROOF STEP]
show "vsv ((cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
[PROOF STATE]
proof (state)
this:
vsv ((dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain A B where F: "F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>A B. F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: is_arrI)
[PROOF STATE]
proof (state)
this:
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B
[PROOF STEP]
obtain b f b' f' h'
        where F_def: "F = [[0, b, f]\<^sub>\<circ>, [0, b', f']\<^sub>\<circ>, [0, h']\<^sub>\<circ>]\<^sub>\<circ>"
          and A_def: "A = [0, b, f]\<^sub>\<circ>"
          and B_def: "B = [0, b', f']\<^sub>\<circ>"
          and h': "h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'"
          and f: "f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
          and f': "f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>"
          and f'_def: "\<KK>\<lparr>ArrMap\<rparr>\<lparr>h'\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = f'"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B

goal (1 subgoal):
 1. (\<And>b f b' f' h'. \<lbrakk>F = [[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ>; A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>; B = [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>; h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'; f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>; f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>; \<KK>\<lparr>ArrMap\<rparr>\<lparr>h'\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = [[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ>
A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>
B = [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
\<KK>\<lparr>ArrMap\<rparr>\<lparr>h'\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = f'

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from prems assms(3) F g' h' f f'
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B
\<lbrakk>?\<KK> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<CC>; ?\<TT> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<AA>; ?g : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?c'\<rbrakk> \<Longrightarrow> ?g \<in>\<^sub>\<circ> ?\<CC>\<lparr>Arr\<rparr>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
[PROOF STEP]
show
        "cf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r\<lparr>ArrMap\<rparr>\<lparr>F\<rparr> =
          (cf_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr>"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B
\<lbrakk>?\<KK> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<CC>; ?\<TT> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<AA>; ?g : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?c'\<rbrakk> \<Longrightarrow> ?g \<in>\<^sub>\<circ> ?\<CC>\<lparr>Arr\<rparr>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>

goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr>
[PROOF STEP]
unfolding F_def A_def B_def
[PROOF STATE]
proof (prove)
using this:
[[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ> \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ> : [[]\<^sub>\<circ>, b, f]\<^sub>\<circ> \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>
\<lbrakk>?\<KK> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<CC>; ?\<TT> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<AA>; ?g : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?c'\<rbrakk> \<Longrightarrow> ?g \<in>\<^sub>\<circ> ?\<CC>\<lparr>Arr\<rparr>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>

goal (1 subgoal):
 1. dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>\<rparr>\<^sub>\<bullet> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by (*slow*)
          (
            cs_concl
              cs_simp: cat_comma_cs_simps cat_cs_simps f'_def[symmetric]
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr>

goal (1 subgoal):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>)\<lparr>ArrMap\<rparr> = (dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 2. \<AA> = \<AA>
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
dghm_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) = dghm_const (c \<down>\<^sub>C\<^sub>F \<KK>) \<AA> r (\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>

goal (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[PROOF STEP]
have \<TT>c'\<KK>: "\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> = \<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> = \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>
[PROOF STEP]
proof(rule cf_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 4. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "\<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>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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 (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<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>

goal (5 subgoals):
 1. \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 3. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 4. c' \<down>\<^sub>C\<^sub>F \<KK> = ?\<CC>
 5. \<AA> = ?\

[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
show " \<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_comma_cs_intros cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : c' \<down>\<^sub>C\<^sub>F \<KK> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (4 subgoals):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
have ObjMap_dom_lhs: "\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
have ObjMap_dom_rhs:
      "\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_comma_cs_intros cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
 2. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 3. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 4. \<AA> = \<AA>
[PROOF STEP]
show "(\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 2. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
show "vsv ((\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)

goal (3 subgoals):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
 2. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 3. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
show "vsv ((\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_comma_cs_intros)
[PROOF STATE]
proof (state)
this:
vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>)

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms(3) prems
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
obtain b f
        where A_def: "A = [0, b, f]\<^sub>\<circ>"
          and b: "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
          and f: "f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>b f. \<lbrakk>A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from prems assms b f
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
show
        "(\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr> =
          (\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
[[]\<^sub>\<circ>, b, f]\<^sub>\<circ> \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, f\<rparr>\<^sub>\<bullet> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> \<lparr>[]\<^sub>\<circ>, b, f\<rparr>\<^sub>\<bullet>
[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:
(\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>

goal (1 subgoal):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Obj\<rparr>
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 2. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 3. \<AA> = \<AA>
[PROOF STEP]
have ArrMap_dom_lhs: "\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (3 subgoals):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 2. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 3. \<AA> = \<AA>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
have ArrMap_dom_rhs:
      "\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps
            cs_intro: cat_comma_cs_intros cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>) = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (3 subgoals):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
 2. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 3. \<AA> = \<AA>
[PROOF STEP]
show "(\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
 2. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
 3. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
show "vsv ((\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_comma_cs_simps
              cs_intro: cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)

goal (3 subgoals):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
 2. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 3. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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]
show "vsv ((\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
u : r <\<^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>
u' : r' <\<^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>

goal (1 subgoal):
 1. vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cs_intro: cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
vsv ((\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>)

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix F
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain A B where F: "F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>A B. F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding cat_comma_cs_simps
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>A B. F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: is_arrI)
[PROOF STATE]
proof (state)
this:
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B
[PROOF STEP]
obtain b f b' f' h'
        where F_def: "F = [[0, b, f]\<^sub>\<circ>, [0, b', f']\<^sub>\<circ>, [0, h']\<^sub>\<circ>]\<^sub>\<circ>"
          and A_def: "A = [0, b, f]\<^sub>\<circ>"
          and B_def: "B = [0, b', f']\<^sub>\<circ>"
          and h': "h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'"
          and f: "f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
          and f': "f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>"
          and f'_def: "\<KK>\<lparr>ArrMap\<rparr>\<lparr>h'\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = f'"
[PROOF STATE]
proof (prove)
using this:
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B

goal (1 subgoal):
 1. (\<And>b f b' f' h'. \<lbrakk>F = [[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ>; A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>; B = [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>; h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'; f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>; f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>; \<KK>\<lparr>ArrMap\<rparr>\<lparr>h'\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F = [[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ>
A = [[]\<^sub>\<circ>, b, f]\<^sub>\<circ>
B = [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
\<KK>\<lparr>ArrMap\<rparr>\<lparr>h'\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> f = f'

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
 2. \<And>a. a \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> \<Longrightarrow> (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from prems assms(3) F g' h' f f'
[PROOF STATE]
proof (chain)
picking this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B
\<lbrakk>?\<KK> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<CC>; ?\<TT> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<AA>; ?g : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?c'\<rbrakk> \<Longrightarrow> ?g \<in>\<^sub>\<circ> ?\<CC>\<lparr>Arr\<rparr>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>
[PROOF STEP]
show
        "(\<TT> \<circ>\<^sub>C\<^sub>F c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr> =
          (\<TT> \<circ>\<^sub>C\<^sub>F c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr>"
[PROOF STATE]
proof (prove)
using this:
F \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
F : A \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> B
\<lbrakk>?\<KK> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<CC>; ?\<TT> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<AA>; ?g : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?c'\<rbrakk> \<Longrightarrow> ?g \<in>\<^sub>\<circ> ?\<CC>\<lparr>Arr\<rparr>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>

goal (1 subgoal):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr>
[PROOF STEP]
unfolding F_def A_def B_def
[PROOF STATE]
proof (prove)
using this:
[[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ> \<in>\<^sub>\<circ> c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>]\<^sub>\<circ> : [[]\<^sub>\<circ>, b, f]\<^sub>\<circ> \<mapsto>\<^bsub>c' \<down>\<^sub>C\<^sub>F \<KK>\<^esub> [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>
\<lbrakk>?\<KK> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<CC>; ?\<TT> : ?\<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<AA>; ?g : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?c'\<rbrakk> \<Longrightarrow> ?g \<in>\<^sub>\<circ> ?\<CC>\<lparr>Arr\<rparr>
h' : b \<mapsto>\<^bsub>\<BB>\<^esub> b'
f : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
f' : c' \<mapsto>\<^bsub>\<CC>\<^esub> \<KK>\<lparr>ObjMap\<rparr>\<lparr>b'\<rparr>

goal (1 subgoal):
 1. (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>\<rparr>\<^sub>\<bullet> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> \<lparr>[[]\<^sub>\<circ>, b, f]\<^sub>\<circ>, [[]\<^sub>\<circ>, b', f']\<^sub>\<circ>, [[]\<^sub>\<circ>, h']\<^sub>\<circ>\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by (*slow*)
          (
            cs_concl
              cs_simp: cat_comma_cs_simps cat_cs_simps f'_def[symmetric]
              cs_intro: cat_lim_cs_intros cat_cs_intros cat_comma_cs_intros
          )
[PROOF STATE]
proof (state)
this:
(\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>\<lparr>F\<rparr>

goal (1 subgoal):
 1. c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr> = c' \<down>\<^sub>C\<^sub>F \<KK>\<lparr>Arr\<rparr>
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr> = (\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>)\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. c' \<down>\<^sub>C\<^sub>F \<KK> = c' \<down>\<^sub>C\<^sub>F \<KK>
 2. \<AA> = \<AA>
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
\<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c' \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> = \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK>

goal (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[PROOF STEP]
from assms(1-3)
[PROOF STATE]
proof (chain)
picking this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'
[PROOF STEP]
have
    "u \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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>"
[PROOF STATE]
proof (prove)
using this:
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
g : c \<mapsto>\<^bsub>\<CC>\<^esub> c'

goal (1 subgoal):
 1. u \<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> : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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 (intro is_cat_coneI)
      (
        cs_concl
          cs_intro: cat_cs_intros cat_comma_cs_intros cat_lim_cs_intros
          cs_simp: const_r_def \<TT>c'\<KK>
      )+
[PROOF STATE]
proof (state)
this:
u \<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> : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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>

goal (1 subgoal):
 1. \<exists>!f. f : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f
[PROOF STEP]
with u'.cat_lim_ua_fo
[PROOF STATE]
proof (chain)
picking this:
?u' : ?r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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> \<Longrightarrow> \<exists>!f'. f' : ?r' \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> ?u' = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f'
u \<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> : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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]
show
    "\<exists>!G.
      G : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and>
      u \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F g \<^sub>A\<down>\<^sub>C\<^sub>F \<KK> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> G"
[PROOF STATE]
proof (prove)
using this:
?u' : ?r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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> \<Longrightarrow> \<exists>!f'. f' : ?r' \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> ?u' = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> f'
u \<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> : r <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<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>

goal (1 subgoal):
 1. \<exists>!G. G : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> G
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>!G. G : r \<mapsto>\<^bsub>\<AA>\<^esub> r' \<and> u \<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> = u' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const (c' \<down>\<^sub>C\<^sub>F \<KK>) \<AA> G

goal:
No subgoals!
[PROOF STEP]
qed