[STATEMENT]
lemma (in is_functor) cf_umap_of_cf_hom_commute: 
  assumes "category \<alpha> \<AA>"
    and "category \<alpha> \<BB>"
    and "c \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
    and "r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>"
    and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
  shows 
    "umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> =
      cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a"
  (is \<open>?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf = ?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
from is_functor_axioms category_cat_Set assms(1,2,4-6)
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have b_rf: 
    "?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by 
      (
        cs_concl cs_shallow 
          cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
      )
[PROOF STATE]
proof (state)
this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
from is_functor_axioms category_cat_Set assms(1,2,4-6)
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have cf_a: 
    "?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a
[PROOF STEP]
proof(rule arr_Set_eqI[of \<alpha>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arr_Set \<alpha> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)
 2. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 4. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 5. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from b_rf
[PROOF STATE]
proof (chain)
picking this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
show arr_Set_b_rf: "arr_Set \<alpha> (?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)"
[PROOF STATE]
proof (prove)
using this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. arr_Set \<alpha> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)
[PROOF STEP]
by (auto dest: cat_Set_is_arrD(1))
[PROOF STATE]
proof (state)
this:
arr_Set \<alpha> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)

goal (4 subgoals):
 1. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 4. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from b_rf
[PROOF STATE]
proof (chain)
picking this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
have dom_lhs: 
      "\<D>\<^sub>\<circ> ((?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a"
[PROOF STATE]
proof (prove)
using this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a

goal (4 subgoals):
 1. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 4. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from cf_a
[PROOF STATE]
proof (chain)
picking this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
show arr_Set_cf_a: "arr_Set \<alpha> (?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)"
[PROOF STATE]
proof (prove)
using this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)
[PROOF STEP]
by (auto dest: cat_Set_is_arrD(1))
[PROOF STATE]
proof (state)
this:
arr_Set \<alpha> (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)

goal (3 subgoals):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
from cf_a
[PROOF STATE]
proof (chain)
picking this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
have dom_rhs: 
      "\<D>\<^sub>\<circ> ((?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a"
[PROOF STATE]
proof (prove)
using this:
cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a : Hom \<AA> r a \<mapsto>\<^bsub>cat_Set \<alpha>\<^esub> Hom \<BB> c (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>) = Hom \<AA> r a

goal (3 subgoals):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 3. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
show "(?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)\<lparr>ArrVal\<rparr> = (?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
 4. \<And>aa. aa : r \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
 4. \<And>aa. aa : r \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
assume "q : r \<mapsto>\<^bsub>\<AA>\<^esub> a"
[PROOF STATE]
proof (state)
this:
q : r \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (4 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
 4. \<And>aa. aa : r \<mapsto>\<^bsub>\<AA>\<^esub> a \<Longrightarrow> (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>aa\<rparr>
[PROOF STEP]
with is_functor_axioms category_cat_Set assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
c \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
q : r \<mapsto>\<^bsub>\<AA>\<^esub> a
[PROOF STEP]
show 
        "(?uof_b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?rf)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr> =
          (?cf \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> ?uof_a)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
category \<alpha> (cat_Set \<alpha>)
category \<alpha> \<AA>
category \<alpha> \<BB>
c \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
r \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
u : c \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
q : r \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (1 subgoal):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
         )
[PROOF STATE]
proof (state)
this:
(umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>\<lparr>q\<rparr>

goal (3 subgoals):
 1. vsv ((umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr>)
 2. vsv ((cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>)
 3. Hom \<AA> r a = Hom \<AA> r a
[PROOF STEP]
qed (use arr_Set_b_rf arr_Set_cf_a in auto)
[PROOF STATE]
proof (state)
this:
(umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrVal\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrDom\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrDom\<rparr>
 2. (umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ>)\<lparr>ArrCod\<rparr> = (cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a)\<lparr>ArrCod\<rparr>
[PROOF STEP]
qed (use b_rf cf_a in \<open>cs_concl cs_shallow cs_simp: cat_cs_simps\<close>)+
[PROOF STATE]
proof (state)
this:
umap_of \<FF> c r u b \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> cf_hom \<AA> [\<AA>\<lparr>CId\<rparr>\<lparr>r\<rparr>, f]\<^sub>\<circ> = cf_hom \<BB> [\<BB>\<lparr>CId\<rparr>\<lparr>c\<rparr>, \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<circ>\<^sub>A\<^bsub>cat_Set \<alpha>\<^esub> umap_of \<FF> c r u a

goal:
No subgoals!
[PROOF STEP]
qed