[STATEMENT]
lemma cat_limit_is_rKe:
  \<comment>\<open>The statement of the theorem is similar to the statement of a part of
    Theorem 1 in Chapter X-7 in \cite{mac_lane_categories_2010}
    or Proposition 6.5.1 in \cite{riehl_category_2016}.\<close>
  assumes "\<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>"
    and "\<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<epsilon>: is_cat_limit \<alpha> \<BB> \<AA> \<TT> \<open>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<close> \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<BB> \<open>cat_1 \<aa> \<ff>\<close> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<GG>: is_functor \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
proof(rule is_cat_rKeI')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
note \<KK>_def = cf_const_if_HomCod_is_cat_1[OF assms(2)]
[PROOF STATE]
proof (state)
this:
\<KK> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)

goal (4 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
note \<GG>_def = cf_const_if_HomDom_is_cat_1[OF assms(3)]
[PROOF STATE]
proof (state)
this:
\<GG> = dghm_const (cat_1 \<aa> \<ff>) \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)

goal (4 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
have \<GG>\<KK>_def: "\<GG> \<circ>\<^sub>C\<^sub>F \<KK> = cf_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
by (subst \<KK>_def, use nothing in \<open>subst \<GG>_def\<close>)
        (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)

goal (4 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 4. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
show "\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps \<GG>\<KK>_def cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
fix \<GG>' \<epsilon>'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
assume prems:
      "\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
      "\<epsilon>' : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (state)
this:
\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret is_functor \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<GG>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
note \<GG>'_def = cf_const_if_HomDom_is_cat_1[OF prems(1)]
[PROOF STATE]
proof (state)
this:
\<GG>' = dghm_const (cat_1 \<aa> \<ff>) \<AA> (\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)

goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have \<epsilon>':
      "\<epsilon>' : cf_const \<BB> \<AA> (\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<epsilon>' : dghm_const \<BB> \<AA> (\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
unfolding \<KK>_def
[PROOF STATE]
proof (prove)
using this:
\<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<epsilon>' : dghm_const \<BB> \<AA> (\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (subst (asm) \<GG>'_def)
        (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<epsilon>' : dghm_const \<BB> \<AA> (\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have "\<epsilon>' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<epsilon>' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (intro is_cat_coneI \<epsilon>') (cs_concl cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<epsilon>' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
from \<epsilon>.cat_lim_ua_fo[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!f'. f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
obtain f'
      where f': "f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>"
        and \<epsilon>_def: "\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'"
        and unique_f':
          "\<lbrakk>
            f'' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>;
            \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f''
          \<rbrakk> \<Longrightarrow> f'' = f'"
        for f''
[PROOF STATE]
proof (prove)
using this:
\<exists>!f'. f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'; \<And>f''. \<lbrakk>f'' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f''\<rbrakk> \<Longrightarrow> f'' = f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
\<lbrakk>?f'' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?f''\<rbrakk> \<Longrightarrow> ?f'' = f'

goal (3 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
show "\<exists>!\<sigma>.
      \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
proof(intro ex1I conjI; (elim conjE)?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (?a1 \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
 3. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ?a1
[PROOF STEP]
from f'
[PROOF STATE]
proof (chain)
picking this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
show
        "ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (subst \<GG>'_def, use nothing in \<open>subst \<GG>_def\<close>)
          (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (2 subgoals):
 1. \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
 2. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
with f'
[PROOF STATE]
proof (chain)
picking this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (prove)
using this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps \<epsilon>_def \<KK>_def cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
assume prems:
        "\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
        "\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (state)
this:
\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
interpret \<sigma>: is_ntcf \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<GG>' \<GG> \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
have "\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
have "\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> (\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> (\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>)
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: cat_cs_simps prems(2) \<KK>_def cs_intro: cat_cs_intros
          )
[PROOF STATE]
proof (state)
this:
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> (\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>)

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> (\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>)
[PROOF STEP]
have \<sigma>\<aa>: "\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> = f'"
[PROOF STATE]
proof (prove)
using this:
\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> (\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>)

goal (1 subgoal):
 1. \<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> = f'
[PROOF STEP]
by (rule unique_f')
[PROOF STATE]
proof (state)
this:
\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> = f'

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
show "\<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
proof(rule ntcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<sigma> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. \<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from f'
[PROOF STATE]
proof (chain)
picking this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
show
          "ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (subst \<GG>'_def, use nothing in \<open>subst \<GG>_def\<close>)
            (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (6 subgoals):
 1. \<sigma> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>
 3. ?\<FF> = \<GG>'
 4. ?\<GG> = \<GG>
 5. ?\<AA> = cat_1 \<aa> \<ff>
 6. ?\<BB> = \<AA>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (\<sigma>\<lparr>NTMap\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<sigma>\<lparr>NTMap\<rparr>) = cat_1 \<aa> \<ff>\<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> (\<sigma>\<lparr>NTMap\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<sigma> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>
 3. ?\<FF> = \<GG>'
 4. ?\<GG> = \<GG>
 5. ?\<AA> = cat_1 \<aa> \<ff>
 6. ?\<BB> = \<AA>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>) = cat_1 \<aa> \<ff>\<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> (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<sigma> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>
 3. ?\<FF> = \<GG>'
 4. ?\<GG> = \<GG>
 5. ?\<AA> = cat_1 \<aa> \<ff>
 6. ?\<BB> = \<AA>
[PROOF STEP]
show "\<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<sigma>\<lparr>NTMap\<rparr>)
 2. vsv (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>)
 3. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> \<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<sigma>\<lparr>NTMap\<rparr>)
 2. vsv (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>)
 3. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> \<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv (\<sigma>\<lparr>NTMap\<rparr>)
 2. vsv (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>)
 3. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> \<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
[PROOF STEP]
have a_def: "a = \<aa>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a = \<aa>
[PROOF STEP]
unfolding cat_1_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>}

goal (1 subgoal):
 1. a = \<aa>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = \<aa>

goal (4 subgoals):
 1. vsv (\<sigma>\<lparr>NTMap\<rparr>)
 2. vsv (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>)
 3. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> \<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from f'
[PROOF STATE]
proof (chain)
picking this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
show "\<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. \<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding a_def \<sigma>\<aa>
[PROOF STATE]
proof (prove)
using this:
f' : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. f' = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<sigma>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (\<sigma>\<lparr>NTMap\<rparr>)
 2. vsv (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>)
 3. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (auto intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<sigma>\<lparr>NTMap\<rparr> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'\<lparr>NTMap\<rparr>

goal (5 subgoals):
 1. \<sigma> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. ?\<FF> = \<GG>'
 3. ?\<GG> = \<GG>
 4. ?\<AA> = cat_1 \<aa> \<ff>
 5. ?\<BB> = \<AA>
[PROOF STEP]
qed (simp_all add: prems)
[PROOF STATE]
proof (state)
this:
\<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (2 subgoals):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
 2. \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
qed (auto simp: assms)
[PROOF STATE]
proof (state)
this:
\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_colimit_is_lKe:
  assumes "\<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>"
    and "\<FF> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<eta>: is_cat_colimit \<alpha> \<BB> \<AA> \<TT> \<open>\<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<close> \<eta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<BB> \<open>cat_1 \<aa> \<ff>\<close> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
from cat_1_components(1)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}
[PROOF STEP]
have \<aa>: "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}

goal (1 subgoal):
 1. \<aa> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<KK>.HomCod.cat_in_Obj_in_Vset)
[PROOF STATE]
proof (state)
this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
from cat_1_components(2)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}
[PROOF STEP]
have \<ff>: "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}

goal (1 subgoal):
 1. \<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<KK>.HomCod.cat_in_Arr_in_Vset)
[PROOF STATE]
proof (state)
this:
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
have \<FF>\<aa>: "\<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> = op_cf \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> = op_cf \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
unfolding cat_op_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> = op_cf \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
note cat_1_op = \<eta>.cat_1_op[OF \<aa> \<ff>]
[PROOF STATE]
proof (state)
this:
op_cat (cat_1 \<aa> \<ff>) = cat_1 \<aa> \<ff>

goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
by
      (
        rule is_cat_rKe.is_cat_lKe_op
          [
            OF cat_limit_is_rKe
              [
                OF
                  \<eta>.is_cat_limit_op[unfolded \<FF>\<aa>]
                  \<KK>.is_functor_op[unfolded cat_1_op]
                  \<FF>.is_functor_op[unfolded cat_1_op]
              ],
            unfolded cat_op_simps cat_1_op
          ]
      )
[PROOF STATE]
proof (state)
this:
\<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cf_adjunction) cf_adjunction_counit_is_rKe:
  \<comment>\<open>The statement of the theorem is similar to the statement of a part of
    Theorem 2 in Chapter X-7 in \cite{mac_lane_categories_2010}
    or Proposition 6.5.2 in \cite{riehl_category_2016}.
    The proof follows (approximately) the proof in \cite{riehl_category_2016}.\<close>
  shows "\<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> cf_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
define \<beta> where "\<beta> = \<alpha> + \<omega>"
[PROOF STATE]
proof (state)
this:
\<beta> = \<alpha> + \<omega>

goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
have \<beta>: "\<Z> \<beta>" and \<alpha>\<beta>: "\<alpha> \<in>\<^sub>\<circ> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta> &&& \<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
by (simp_all add: \<beta>_def \<Z>_Limit_\<alpha>\<omega> \<Z>_\<omega>_\<alpha>\<omega> \<Z>_def \<Z>_\<alpha>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
using this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
note exp_adj = cf_adj_exp_cf_cat_exp_cf_cat[OF \<beta> \<alpha>\<beta> R.category_axioms]
[PROOF STATE]
proof (state)
this:
cf_adjunction_of_unit \<beta> (exp_cat_cf \<alpha> \
 \<GG>) (exp_cat_cf \<alpha> \
 \<FF>) (exp_cat_ntcf \<alpha> \
 (\<eta>\<^sub>C \<Phi>)) : exp_cat_cf \<alpha> \
 \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F exp_cat_cf \<alpha> \
 \<FF> : cat_FUNCT \<alpha> \<CC> \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \
 \

goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\<eta> = \<open>\<eta>\<^sub>C \<Phi>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\<epsilon> = \<open>\<epsilon>\<^sub>C \<Phi>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\
\<eta> = \<open>exp_cat_ntcf \<alpha> \
 ?\<eta>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\
\<FF> = \<open>exp_cat_cf \<alpha> \
 \<FF>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\
\<GG> = \<open>exp_cat_cf \<alpha> \
 \<GG>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\
\
 = \<open>cat_FUNCT \<alpha> \
 \
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?\<CC>\
 = \<open>cat_FUNCT \<alpha> \<CC> \
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
let ?adj_\
\<eta> = \<open>cf_adjunction_of_unit \<beta> ?\
\<GG> ?\
\<FF> ?\
\<eta>\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
interpret \
\<eta>: is_cf_adjunction \<beta> ?\<CC>\
 ?\
\
 ?\
\<GG> ?\
\<FF> ?adj_\
\<eta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<beta> (exp_cat_cf \<alpha> \
 \<GG>) (exp_cat_cf \<alpha> \
 \<FF>) (exp_cat_ntcf \<alpha> \
 (\<eta>\<^sub>C \<Phi>)) : exp_cat_cf \<alpha> \
 \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F exp_cat_cf \<alpha> \
 \<FF> : cat_FUNCT \<alpha> \<CC> \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \
 \

[PROOF STEP]
by (rule exp_adj)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
proof(intro is_cat_rKeI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
have id_\
: "cf_map (cf_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_map (dghm_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_FUNCT_components(1)
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
[PROOF STATE]
proof (state)
this:
cf_map (dghm_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cf_map (dghm_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>
[PROOF STEP]
have exp_id_\
:
      "exp_cat_cf \<alpha> \
 \<FF>\<lparr>ObjMap\<rparr>\<lparr>cf_map (cf_id \
)\<rparr> = cf_map \<FF>"
[PROOF STATE]
proof (prove)
using this:
cf_map (dghm_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. exp_cat_cf \<alpha> \
 \<FF>\<lparr>ObjMap\<rparr>\<lparr>cf_map (dghm_id \
)\<rparr> = cf_map \<FF>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
exp_cat_cf \<alpha> \
 \<FF>\<lparr>ObjMap\<rparr>\<lparr>cf_map (dghm_id \
)\<rparr> = cf_map \<FF>

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
have \<FF>: "cf_map \<FF> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \
\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_map \<FF> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \
\<lparr>Obj\<rparr>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_FUNCT_components(1)
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
[PROOF STATE]
proof (state)
this:
cf_map \<FF> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \
\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
have \<epsilon>: "ntcf_arrow (\<epsilon>\<^sub>C \<Phi>) \<in>\<^sub>\<circ> ntcf_arrows \<alpha> \
 \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_arrow (\<epsilon>\<^sub>C \<Phi>) \<in>\<^sub>\<circ> ntcf_arrows \<alpha> \
 \

[PROOF STEP]
by (cs_concl cs_intro: cat_FUNCT_cs_intros adj_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_arrow (\<epsilon>\<^sub>C \<Phi>) \<in>\<^sub>\<circ> ntcf_arrows \<alpha> \
 \

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
have \
\
: "category \<beta> (cat_FUNCT \<alpha> \
 \
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<beta> (cat_FUNCT \<alpha> \
 \
)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
category \<beta> (cat_FUNCT \<alpha> \
 \
)

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
have \<CC>\
: "category \<beta> (cat_FUNCT \<alpha> \<CC> \
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<beta> (cat_FUNCT \<alpha> \<CC> \
)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
category \<beta> (cat_FUNCT \<alpha> \<CC> \
)

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
from
      \<epsilon> \<FF> \<alpha>\<beta> id_\

      \
\
 \<CC>\
 LR.is_functor_axioms RL.is_functor_axioms R.cat_cf_id_is_functor
      NT.is_iso_ntcf_axioms
[PROOF STATE]
proof (chain)
picking this:
ntcf_arrow (\<epsilon>\<^sub>C \<Phi>) \<in>\<^sub>\<circ> ntcf_arrows \<alpha> \
 \

cf_map \<FF> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \
\<lparr>Obj\<rparr>
\<alpha> \<in>\<^sub>\<circ> \<beta>
cf_map (dghm_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>
category \<beta> (cat_FUNCT \<alpha> \
 \
)
category \<beta> (cat_FUNCT \<alpha> \<CC> \
)
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<Phi>\<lparr>AdjNT\<rparr> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\
(\<FF>-,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<GG>-) : op_cat \<CC> \<times>\<^sub>C \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
have \<epsilon>_id_\
: "\<epsilon>\<^sub>C ?adj_\
\<eta>\<lparr>NTMap\<rparr>\<lparr>cf_map (cf_id \
)\<rparr> = ntcf_arrow ?\<epsilon>"
[PROOF STATE]
proof (prove)
using this:
ntcf_arrow (\<epsilon>\<^sub>C \<Phi>) \<in>\<^sub>\<circ> ntcf_arrows \<alpha> \
 \

cf_map \<FF> \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \
\<lparr>Obj\<rparr>
\<alpha> \<in>\<^sub>\<circ> \<beta>
cf_map (dghm_id \
) \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \
 \
\<lparr>Obj\<rparr>
category \<beta> (cat_FUNCT \<alpha> \
 \
)
category \<beta> (cat_FUNCT \<alpha> \<CC> \
)
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<Phi>\<lparr>AdjNT\<rparr> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\
(\<FF>-,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(-,\<GG>-) : op_cat \<CC> \<times>\<^sub>C \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. \<epsilon>\<^sub>C (cf_adjunction_of_unit \<beta> (exp_cat_cf \<alpha> \
 \<GG>) (exp_cat_cf \<alpha> \
 \<FF>) (exp_cat_ntcf \<alpha> \
 (\<eta>\<^sub>C \<Phi>)))\<lparr>NTMap\<rparr>\<lparr>cf_map (dghm_id \
)\<rparr> = ntcf_arrow (\<epsilon>\<^sub>C \<Phi>)
[PROOF STEP]
by (*slow*)
        (
          cs_concl
            cs_simp:
              cat_Set_the_inverse[symmetric]
              cat_op_simps
              cat_cs_simps
              cat_FUNCT_cs_simps
              adj_cs_simps
            cs_intro:
              \
\<eta>.NT.iso_ntcf_is_iso_arr''
              cat_op_intros
              adj_cs_intros
              cat_cs_intros
              cat_FUNCT_cs_intros
              cat_prod_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<epsilon>\<^sub>C (cf_adjunction_of_unit \<beta> (exp_cat_cf \<alpha> \
 \<GG>) (exp_cat_cf \<alpha> \
 \<FF>) (exp_cat_ntcf \<alpha> \
 (\<eta>\<^sub>C \<Phi>)))\<lparr>NTMap\<rparr>\<lparr>cf_map (dghm_id \
)\<rparr> = ntcf_arrow (\<epsilon>\<^sub>C \<Phi>)

goal (4 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 4. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
show "universal_arrow_fo ?\
\<GG> (cf_map (cf_id \
)) (cf_map \<FF>) (ntcf_arrow ?\<epsilon>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))
[PROOF STEP]
by
        (
          rule is_cf_adjunction.cf_adjunction_counit_component_is_ua_fo[
            OF exp_adj id_\
, unfolded exp_id_\
 \<epsilon>_id_\

            ]
        )
[PROOF STATE]
proof (state)
this:
universal_arrow_fo (exp_cat_cf \<alpha> \
 \<GG>) (cf_map (dghm_id \
)) (cf_map \<FF>) (ntcf_arrow (\<epsilon>\<^sub>C \<Phi>))

goal (3 subgoals):
 1. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 2. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. \<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<mapsto>\<^sub>C\<^sub>F dghm_id \
 : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
qed (cs_concl cs_intro: cat_cs_intros adj_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<epsilon>\<^sub>C \<Phi> : \<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> dghm_id \
 : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cf_adjunction) cf_adjunction_unit_is_lKe:
  shows "\<eta>\<^sub>C \<Phi> : cf_id \<CC> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG> \<circ>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<^sub>C \<DD> \<mapsto>\<^sub>C \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta>\<^sub>C \<Phi> : dghm_id \<CC> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG> \<circ>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<^sub>C \<DD> \<mapsto>\<^sub>C \<CC>
[PROOF STEP]
by
    (
      rule is_cat_rKe.is_cat_lKe_op
        [
          OF is_cf_adjunction.cf_adjunction_counit_is_rKe
            [
              OF is_cf_adjunction_op,
              folded op_ntcf_cf_adjunction_unit op_cf_cf_id
            ],
          unfolded
            cat_op_simps ntcf_op_ntcf_op_ntcf[OF cf_adjunction_unit_is_ntcf]
        ]
    )