[STATEMENT]
lemma cf_adjunction_if_lKe_preserves:
  \<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}.\<close>
  assumes "\<eta> : cf_id \
 \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<GG> : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C (\<GG> : \
 \<mapsto>\<mapsto>\<^sub>C \<CC>)"
  shows "cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<eta>: is_cat_lKe_preserves \<alpha> \
 \<CC> \
 \<CC> \<GG> \<open>cf_id \
\<close> \<FF> \<GG> \<eta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : dghm_id \
 \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<GG> : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C \<CC>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
from \<eta>.cat_lKe_preserves
[PROOF STATE]
proof (chain)
picking this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \
 \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>C\<^sub>F \<GG> : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<CC>
[PROOF STEP]
interpret \<GG>\<eta>:
    is_cat_lKe \<alpha> \
 \<CC> \<CC> \<GG> \<GG> \<open>\<GG> \<circ>\<^sub>C\<^sub>F \<FF>\<close> \<open>\<GG> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>\<close>
[PROOF STATE]
proof (prove)
using this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \
 \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>C\<^sub>F \<GG> : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<CC>

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta> : \<GG> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>C\<^sub>F \<GG> : \
 \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<CC>
[PROOF STEP]
by (cs_prems cs_shallow cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
from
    \<GG>\<eta>.cat_lKe_unique
      [
        OF \<eta>.AG.HomCod.cat_cf_id_is_functor,
        unfolded \<eta>.AG.cf_cf_comp_cf_id_left,
        OF \<eta>.AG.cf_ntcf_id_is_ntcf
      ]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!\<sigma>. \<sigma> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC> \<and> ntcf_id \<GG> = \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>)
[PROOF STEP]
obtain \<epsilon> where \<epsilon>: "\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<FF> \<mapsto>\<^sub>C\<^sub>F cf_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and ntcf_id_\<GG>_def: "ntcf_id \<GG> = \<epsilon> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<exists>!\<sigma>. \<sigma> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC> \<and> ntcf_id \<GG> = \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>)

goal (1 subgoal):
 1. (\<And>\<epsilon>. \<lbrakk>\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>; ntcf_id \<GG> = \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
ntcf_id \<GG> = \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>)

goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<epsilon>: is_ntcf \<alpha> \<CC> \<CC> \<open>\<GG> \<circ>\<^sub>C\<^sub>F \<FF>\<close> \<open>cf_id \<CC>\<close> \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule \<epsilon>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(rule counit_unit_is_cf_adjunction)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. ?\<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
 8. ?\<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) = ntcf_id \<GG>
[PROOF STEP]
show [cat_cs_simps]: "\<epsilon> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>) = ntcf_id \<GG>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) = ntcf_id \<GG>
[PROOF STEP]
by (rule ntcf_id_\<GG>_def[symmetric])
[PROOF STATE]
proof (state)
this:
\<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) = ntcf_id \<GG>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
have \<eta>_def: "\<eta> = (ntcf_id \<FF> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> = ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps ntcf_id_cf_comp[symmetric]
            cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<eta> = ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
note [cat_cs_simps] = this[symmetric]
[PROOF STATE]
proof (state)
this:
ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
let ?\<FF>\<epsilon>\<GG> = \<open>\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<epsilon> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG>\<close>
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
let ?\<eta>\<FF>\<GG> = \<open>\<eta> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG>\<close>
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
let ?\<FF>\<GG>\<eta> = \<open>\<FF> \<circ>\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>\<close>
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
have "(?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<eta>\<FF>\<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta> = (?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<FF>\<GG>\<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>
[PROOF STEP]
proof(rule ntcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (((?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<eta>\<FF>\<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>) = \
\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>) = \
\<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> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>) = \
\<lparr>Obj\<rparr>

goal (7 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (((?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<FF>\<GG>\<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>) = \
\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>) = \
\<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> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>) = \
\<lparr>Obj\<rparr>

goal (7 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
note is_ntcf.ntcf_Comp_commute[cat_cs_simps del]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<NN> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>; ?f : ?a \<mapsto>\<^bsub>?\<AA>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?\<NN>\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>?\<BB>\<^esub> ?\<FF>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = ?\<GG>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>?\<BB>\<^esub> ?\<NN>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>

goal (7 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
note category.cat_Comp_assoc[cat_cs_simps del]
[PROOF STATE]
proof (state)
this:
\<lbrakk>category ?\<alpha> ?\<CC>; ?h : ?c \<mapsto>\<^bsub>?\<CC>\<^esub> ?d; ?g : ?b \<mapsto>\<^bsub>?\<CC>\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>?\<CC>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?h \<circ>\<^sub>A\<^bsub>?\<CC>\<^esub> ?g \<circ>\<^sub>A\<^bsub>?\<CC>\<^esub> ?f = ?h \<circ>\<^sub>A\<^bsub>?\<CC>\<^esub> (?g \<circ>\<^sub>A\<^bsub>?\<CC>\<^esub> ?f)

goal (7 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show
        "((?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<eta>\<FF>\<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> =
          ((?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<FF>\<GG>\<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 3. \
\<lparr>Obj\<rparr> = \
\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr> \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 3. \
\<lparr>Obj\<rparr> = \
\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr> \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 3. \
\<lparr>Obj\<rparr> = \
\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr> \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr>
[PROOF STEP]
show
          "((?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<eta>\<FF>\<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
            ((?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<FF>\<GG>\<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \
\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
            (
              cs_concl
                cs_simp: cat_cs_simps \<eta>.ntcf_lKe.ntcf_Comp_commute[symmetric]
                cs_intro: cat_cs_intros
            )
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>)
 3. \
\<lparr>Obj\<rparr> = \
\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr> = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>)\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
have "\<dots> = (ntcf_id \<FF> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp:
              cat_cs_simps
              cf_comp_cf_ntcf_comp_assoc
              cf_ntcf_comp_ntcf_cf_comp_assoc
              cf_ntcf_comp_ntcf_vcomp[symmetric]
            cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
have "\<dots> = \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
ntcf_id \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>
[PROOF STEP]
have "(?\<FF>\<epsilon>\<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ?\<eta>\<FF>\<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta> = \<eta>"
[PROOF STATE]
proof (prove)
using this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>
[PROOF STEP]
have \<eta>_def': "\<eta> = (\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<FF>) \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
using this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta> = \<eta>

goal (1 subgoal):
 1. \<eta> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps ntcf_vcomp_ntcf_cf_comp[symmetric]
            cs_intro: cat_cs_intros
        )+
[PROOF STATE]
proof (state)
this:
\<eta> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
have \<FF>\<epsilon>\<eta>\<FF>: "\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<FF>) : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
from \<eta>.cat_lKe_unique[OF \<eta>.Lan.is_functor_axioms \<eta>.ntcf_lKe.is_ntcf_axioms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
 \<and> \<eta> = \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>
[PROOF STEP]
obtain \<sigma> where
      "\<lbrakk> \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
; \<eta> = \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta> \<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>"
      for \<sigma>'
[PROOF STATE]
proof (prove)
using this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
 \<and> \<eta> = \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>

goal (1 subgoal):
 1. (\<And>\<sigma>. (\<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
; \<eta> = \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
; \<eta> = ?\<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<eta>\<rbrakk> \<Longrightarrow> ?\<sigma>' = \<sigma>

goal (7 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 7. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
from this[OF \<eta>.Lan.cf_ntcf_id_is_ntcf \<eta>_def] this[OF \<FF>\<epsilon>\<eta>\<FF> \<eta>_def']
[PROOF STATE]
proof (chain)
picking this:
ntcf_id \<FF> = \<sigma>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = \<sigma>
[PROOF STEP]
show
      "\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<FF>) = ntcf_id \<FF>"
[PROOF STATE]
proof (prove)
using this:
ntcf_id \<FF> = \<sigma>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = \<sigma>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<eta> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = ntcf_id \<FF>

goal (6 subgoals):
 1. category \<alpha> \

 2. category \<alpha> \<CC>
 3. \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

 6. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>C\<^sub>F dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
qed (cs_concl cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
cf_adjunction_of_unit \<alpha> \<GG> \<FF> \<eta> : \<GG> \<rightleftharpoons>\<^sub>C\<^sub>F \<FF> : \
 \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cf_adjunction_if_rKe_preserves:
  assumes "\<epsilon> : \<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 (\<GG> : \
 \<mapsto>\<mapsto>\<^sub>C \<CC>)"
  shows "cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
interpret \<epsilon>: is_cat_rKe_preserves \<alpha> \
 \<CC> \
 \<CC> \<GG> \<open>cf_id \
\<close> \<FF> \<GG> \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<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 \<GG> : \
 \<mapsto>\<mapsto>\<^sub>C \<CC>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
have "op_cf (cf_id \
) = cf_id (op_cat \
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cf (dghm_id \
) = dghm_id (op_cat \
)
[PROOF STEP]
unfolding cat_op_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id (op_cat \
) = dghm_id (op_cat \
)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_cf (dghm_id \
) = dghm_id (op_cat \
)

goal (1 subgoal):
 1. cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by
      (
        rule is_cf_adjunction.is_cf_adjunction_op
          [
            OF cf_adjunction_if_lKe_preserves[
              OF \<epsilon>.is_cat_rKe_preserves_op[unfolded op_cf_cf_id]
              ],
            folded cf_adjunction_of_counit_def,
            unfolded cat_op_simps
          ]
      )
[PROOF STATE]
proof (state)
this:
cf_adjunction_of_counit \<alpha> \<FF> \<GG> \<epsilon> : \<FF> \<rightleftharpoons>\<^sub>C\<^sub>F \<GG> : \<CC> \<rightleftharpoons>\<rightleftharpoons>\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coerce_lifted_abs [simp]: "coerce\<cdot>(lifted_abs\<cdot>x) = lifted_abs\<cdot>(coerce\<cdot>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('b\<cdot>lifted, 'a\<cdot>lifted)\<cdot>(lifted_abs\<cdot>x) = lifted_abs\<cdot>(COERCE('b\<^sub>\<bottom>, 'a\<^sub>\<bottom>)\<cdot>x)
[PROOF STEP]
apply (simp add: lifted_abs_def coerce_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRJ('a\<cdot>lifted)\<cdot>(EMB('b\<cdot>lifted)\<cdot>(PRJ('b\<cdot>lifted)\<cdot>(EMB('b\<^sub>\<bottom>)\<cdot>x))) = PRJ('a\<cdot>lifted)\<cdot>(EMB('a\<^sub>\<bottom>)\<cdot>(PRJ('a\<^sub>\<bottom>)\<cdot>(EMB('b\<^sub>\<bottom>)\<cdot>x)))
[PROOF STEP]
apply (simp add: emb_prj_emb prj_emb_prj DEFL_eq_lifted)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coerce_Lifted [simp]: "coerce\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(coerce\<cdot>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('b\<cdot>lifted, 'a\<cdot>lifted)\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(COERCE('b, 'a)\<cdot>x)
[PROOF STEP]
unfolding Lifted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE('b\<cdot>lifted, 'a\<cdot>lifted)\<cdot>((\<Lambda> a. lifted_abs\<cdot>(up\<cdot>a))\<cdot>x) = (\<Lambda> a. lifted_abs\<cdot>(up\<cdot>a))\<cdot>(COERCE('b, 'a)\<cdot>x)
[PROOF STEP]
by simp


[STATEMENT]
lemma fmapU_lifted_simps [simp]:
  "fmapU\<cdot>f\<cdot>(\<bottom>::udom\<cdot>lifted) = \<bottom>"
  "fmapU\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmapU\<cdot>f\<cdot>\<bottom> = \<bottom> &&& fmapU\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)
[PROOF STEP]
unfolding fmapU_lifted_def lifted_map_def fix_const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> a. lifted_abs oo u_map\<cdot>a oo lifted_rep)\<cdot>f\<cdot>\<bottom> = \<bottom> &&& (\<Lambda> a. lifted_abs oo u_map\<cdot>a oo lifted_rep)\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> a. lifted_abs oo u_map\<cdot>a oo lifted_rep)\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)
[PROOF STEP]
apply (simp add: Lifted_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bindU_lifted_strict [simp]: "bindU\<cdot>\<bottom>\<cdot>k = (\<bottom>::udom\<cdot>lifted)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bindU\<cdot>\<bottom>\<cdot>k = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma fmap_lifted_simps [simp]:
  "fmap\<cdot>f\<cdot>(\<bottom>::'a\<cdot>lifted) = \<bottom>"
  "fmap\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> = \<bottom> &&& fmap\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)
[PROOF STEP]
unfolding fmap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>lifted \<rightarrow> udom\<cdot>lifted, ('a \<rightarrow> 'b) \<rightarrow> 'a\<cdot>lifted \<rightarrow> 'b\<cdot>lifted)\<cdot>fmapU\<cdot>f\<cdot>\<bottom> = \<bottom> &&& COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>lifted \<rightarrow> udom\<cdot>lifted, ('a \<rightarrow> 'b) \<rightarrow> 'a\<cdot>lifted \<rightarrow> 'b\<cdot>lifted)\<cdot>fmapU\<cdot>f\<cdot>(Lifted\<cdot>x) = Lifted\<cdot>(f\<cdot>x)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma bind_lifted_simps [simp]:
  "bind\<cdot>(\<bottom>::'a\<cdot>lifted)\<cdot>f = \<bottom>"
  "bind\<cdot>(Lifted\<cdot>x)\<cdot>f = f\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bottom> \<bind> f = \<bottom> &&& Lifted\<cdot>x \<bind> f = f\<cdot>x
[PROOF STEP]
unfolding bind_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE(udom\<cdot>lifted \<rightarrow> (udom \<rightarrow> udom\<cdot>lifted) \<rightarrow> udom\<cdot>lifted, 'a\<cdot>lifted \<rightarrow> ('a \<rightarrow> 'b\<cdot>lifted) \<rightarrow> 'b\<cdot>lifted)\<cdot>bindU\<cdot>\<bottom>\<cdot>f = \<bottom> &&& COERCE(udom\<cdot>lifted \<rightarrow> (udom \<rightarrow> udom\<cdot>lifted) \<rightarrow> udom\<cdot>lifted, 'a\<cdot>lifted \<rightarrow> ('a \<rightarrow> 'b\<cdot>lifted) \<rightarrow> 'b\<cdot>lifted)\<cdot>bindU\<cdot>(Lifted\<cdot>x)\<cdot>f = f\<cdot>x
[PROOF STEP]
by simp_all


[STATEMENT]
lemma return_lifted_def: "return = Lifted"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return = Lifted
[PROOF STEP]
unfolding return_def returnU_lifted_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE(udom \<rightarrow> udom\<cdot>lifted, 'a \<rightarrow> 'a\<cdot>lifted)\<cdot>Lifted = Lifted
[PROOF STEP]
by (simp add: coerce_cfun cfcomp1 eta_cfun)


[STATEMENT]
lemma join_lifted_simps [simp]:
  "join\<cdot>(\<bottom>::'a\<cdot>lifted\<cdot>lifted) = \<bottom>"
  "join\<cdot>(Lifted\<cdot>xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join\<cdot>\<bottom> = \<bottom> &&& join\<cdot>(Lifted\<cdot>xs) = xs
[PROOF STEP]
unfolding join_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> m. m \<bind> (\<Lambda> x. x))\<cdot>\<bottom> = \<bottom> &&& (\<Lambda> m. m \<bind> (\<Lambda> x. x))\<cdot>(Lifted\<cdot>xs) = xs
[PROOF STEP]
by simp_all


[STATEMENT]
lemma is_document_ptr_ref [simp]: "is_document_ptr (document_ptr.Ref n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_document_ptr (document_ptr.Ref n)
[PROOF STEP]
by(simp add: is_document_ptr\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma cast_document_ptr_not_node_ptr [simp]:
  "cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr \<noteq> cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr"
  "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr \<noteq> cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast document_ptr \<noteq> cast node_ptr &&& cast node_ptr \<noteq> cast document_ptr
[PROOF STEP]
unfolding cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr.Ext (Inr (Inl document_ptr)) \<noteq> object_ptr.Ext (Inl node_ptr) &&& object_ptr.Ext (Inl node_ptr) \<noteq> object_ptr.Ext (Inr (Inl document_ptr))
[PROOF STEP]
by auto


[STATEMENT]
lemma document_ptr_no_node_ptr_cast [simp]:
  "\<not> is_document_ptr_kind (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_document_ptr_kind (cast node_ptr)
[PROOF STEP]
by(simp add: cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_document_ptr_kind_def)


[STATEMENT]
lemma node_ptr_no_document_ptr_cast [simp]:
  "\<not> is_node_ptr_kind (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_node_ptr_kind (cast document_ptr)
[PROOF STEP]
using is_node_ptr_kind_obtains
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_node_ptr_kind ?ptr; \<And>node_ptr. cast ?ptr = Some node_ptr \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<not> is_node_ptr_kind (cast document_ptr)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma document_ptr_document_ptr_cast [simp]:
  "is_document_ptr_kind (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_document_ptr_kind (cast document_ptr)
[PROOF STEP]
by (simp add: cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_document_ptr_kind_def)


[STATEMENT]
lemma document_ptr_casts_commute [simp]:
  "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = Some document_ptr \<longleftrightarrow> cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr = ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast ptr = Some document_ptr) = (cast document_ptr = ptr)
[PROOF STEP]
unfolding cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case ptr of object_ptr.Ext (Inl xa) \<Rightarrow> Map.empty xa | object_ptr.Ext (Inr (Inl x)) \<Rightarrow> Some x | object_ptr.Ext (Inr (Inr x)) \<Rightarrow> Map.empty x) = Some document_ptr) = (object_ptr.Ext (Inr (Inl document_ptr)) = ptr)
[PROOF STEP]
by(auto split: object_ptr.splits sum.splits)


[STATEMENT]
lemma document_ptr_casts_commute2 [simp]:
  "(cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr) = Some document_ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (cast document_ptr) = Some document_ptr
[PROOF STEP]
by simp


[STATEMENT]
lemma document_ptr_casts_commute3 [simp]:
  assumes "is_document_ptr_kind ptr"
  shows "cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (the (cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr)) = ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (the (cast ptr)) = ptr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_document_ptr_kind ptr

goal (1 subgoal):
 1. cast (the (cast ptr)) = ptr
[PROOF STEP]
by(auto simp add: is_document_ptr_kind_def cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
      split: object_ptr.splits sum.splits)


[STATEMENT]
lemma is_document_ptr_kind_obtains:
  assumes "is_document_ptr_kind ptr"
  obtains document_ptr where "ptr = cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>document_ptr. ptr = cast document_ptr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms is_document_ptr_kind_def
[PROOF STATE]
proof (prove)
using this:
is_document_ptr_kind ptr
is_document_ptr_kind ?ptr = (case cast ?ptr of None \<Rightarrow> False | Some x \<Rightarrow> True)

goal (1 subgoal):
 1. (\<And>document_ptr. ptr = cast document_ptr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis case_optionE document_ptr_casts_commute)


[STATEMENT]
lemma is_document_ptr_kind_none:
  assumes "\<not>is_document_ptr_kind ptr"
  shows "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast ptr = None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> is_document_ptr_kind ptr

goal (1 subgoal):
 1. cast ptr = None
[PROOF STEP]
unfolding is_document_ptr_kind_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
[PROOF STATE]
proof (prove)
using this:
\<not> (case case ptr of object_ptr.Ext (Inl xa) \<Rightarrow> Map.empty xa | object_ptr.Ext (Inr (Inl x)) \<Rightarrow> Some x | object_ptr.Ext (Inr (Inr x)) \<Rightarrow> Map.empty x of None \<Rightarrow> False | Some x \<Rightarrow> True)

goal (1 subgoal):
 1. (case ptr of object_ptr.Ext (Inl xa) \<Rightarrow> Map.empty xa | object_ptr.Ext (Inr (Inl x)) \<Rightarrow> Some x | object_ptr.Ext (Inr (Inr x)) \<Rightarrow> Map.empty x) = None
[PROOF STEP]
by (auto split: object_ptr.splits sum.splits)


[STATEMENT]
lemma cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject [simp]:
  "cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r x = cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast x = cast y) = (x = y)
[PROOF STEP]
by(simp add: cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_ext_none [simp]:
  "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None
[PROOF STEP]
by(simp add: cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma is_document_ptr_kind_not_element_ptr_kind [dest]:
  "is_document_ptr_kind ptr \<Longrightarrow> \<not> is_element_ptr_kind ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_document_ptr_kind ptr \<Longrightarrow> \<not> (case cast ptr of None \<Rightarrow> False | Some node_ptr \<Rightarrow> is_element_ptr_kind node_ptr)
[PROOF STEP]
by(auto simp add:  split: option.splits)


[STATEMENT]
lemma distinct_vertices13[simp]: "vertex_1 \<noteq> vertex_3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex_1 \<noteq> vertex_3
[PROOF STEP]
using distinct_vertices
[PROOF STATE]
proof (prove)
using this:
distinct [vertex_1, vertex_2, vertex_3]

goal (1 subgoal):
 1. vertex_1 \<noteq> vertex_3
[PROOF STEP]
by(simp)


[STATEMENT]
lemma distinct_vertices23[simp]: "vertex_2 \<noteq> vertex_3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex_2 \<noteq> vertex_3
[PROOF STEP]
using distinct_vertices
[PROOF STATE]
proof (prove)
using this:
distinct [vertex_1, vertex_2, vertex_3]

goal (1 subgoal):
 1. vertex_2 \<noteq> vertex_3
[PROOF STEP]
by(simp)


[STATEMENT]
lemma Puniform_in:
  "x \<in> S \<Longrightarrow> Puniform S x = 1 / card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> Puniform S x = 1 / real (card S)
[PROOF STEP]
by(simp add:Puniform_def)


[STATEMENT]
lemma Puniform_out:
  "x \<notin> S \<Longrightarrow> Puniform S x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> S \<Longrightarrow> Puniform S x = 0
[PROOF STEP]
by(simp add:Puniform_def)


[STATEMENT]
lemma supp_Puniform:
  "finite S \<Longrightarrow> supp (Puniform S) = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> supp (Puniform S) = S
[PROOF STEP]
by(auto simp:Puniform_def supp_def)


[STATEMENT]
lemma mu_id: "(\<mu> X \<bullet> X) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> X \<bullet> X) = true
[PROOF STEP]
by (simp add: antisym gfp_upperbound)


[STATEMENT]
lemma mu_const: "(\<mu> X \<bullet> P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> X \<bullet> P) = P
[PROOF STEP]
by (simp add: gfp_const)


[STATEMENT]
lemma nu_id: "(\<nu> X \<bullet> X) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> X \<bullet> X) = false
[PROOF STEP]
by (meson lfp_lowerbound utp_pred_laws.bot.extremum_unique)


[STATEMENT]
lemma nu_const: "(\<nu> X \<bullet> P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> X \<bullet> P) = P
[PROOF STEP]
by (simp add: lfp_const)


[STATEMENT]
lemma mu_refine_intro:
  assumes "(C \<Rightarrow> S) \<sqsubseteq> F(C \<Rightarrow> S)" "(C \<and> \<mu> F) = (C \<and> \<nu> F)"
  shows "(C \<Rightarrow> S) \<sqsubseteq> \<mu> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C \<Rightarrow> S) \<sqsubseteq> \<mu> F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (C \<Rightarrow> S) \<sqsubseteq> \<mu> F
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(C \<Rightarrow> S) \<sqsubseteq> F (C \<Rightarrow> S)
(C \<and> \<mu> F) = (C \<and> \<nu> F)
[PROOF STEP]
have "(C \<Rightarrow> S) \<sqsubseteq> \<nu> F"
[PROOF STATE]
proof (prove)
using this:
(C \<Rightarrow> S) \<sqsubseteq> F (C \<Rightarrow> S)
(C \<and> \<mu> F) = (C \<and> \<nu> F)

goal (1 subgoal):
 1. (C \<Rightarrow> S) \<sqsubseteq> \<nu> F
[PROOF STEP]
by (simp add: lfp_lowerbound)
[PROOF STATE]
proof (state)
this:
(C \<Rightarrow> S) \<sqsubseteq> \<nu> F

goal (1 subgoal):
 1. (C \<Rightarrow> S) \<sqsubseteq> \<mu> F
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
(C \<Rightarrow> S) \<sqsubseteq> F (C \<Rightarrow> S)
(C \<and> \<mu> F) = (C \<and> \<nu> F)
(C \<Rightarrow> S) \<sqsubseteq> \<nu> F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(C \<Rightarrow> S) \<sqsubseteq> F (C \<Rightarrow> S)
(C \<and> \<mu> F) = (C \<and> \<nu> F)
(C \<Rightarrow> S) \<sqsubseteq> \<nu> F

goal (1 subgoal):
 1. (C \<Rightarrow> S) \<sqsubseteq> \<mu> F
[PROOF STEP]
by (pred_auto)
[PROOF STATE]
proof (state)
this:
(C \<Rightarrow> S) \<sqsubseteq> \<mu> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain0 [simp]: "chain Y \<Longrightarrow> Y 0 = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain Y \<Longrightarrow> Y 0 = false
[PROOF STEP]
by (simp add:chain_def)


[STATEMENT]
lemma chainI:
  assumes "Y 0 = false" "\<And> i. Y (Suc i) \<sqsubseteq> Y i"
  shows "chain Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain Y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Y 0 = false
Y (Suc ?i) \<sqsubseteq> Y ?i

goal (1 subgoal):
 1. chain Y
[PROOF STEP]
by (auto simp add: chain_def)


[STATEMENT]
lemma chainE:
  assumes "chain Y" "\<And> i. \<lbrakk> Y 0 = false; Y (Suc i) \<sqsubseteq> Y i \<rbrakk> \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain Y
\<lbrakk>Y 0 = false; Y (Suc ?i) \<sqsubseteq> Y ?i\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (simp add: chain_def)


[STATEMENT]
lemma L274:
  assumes "\<forall> n. ((E n \<and>\<^sub>p X) = (E n \<and> Y))"
  shows "(\<Sqinter> (range E) \<and> X) = (\<Sqinter> (range E) \<and> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Or>range E \<and> X) = (\<Or>range E \<and> Y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (E n \<and> X) = (E n \<and> Y)

goal (1 subgoal):
 1. (\<Or>range E \<and> X) = (\<Or>range E \<and> Y)
[PROOF STEP]
by (pred_auto)


[STATEMENT]
lemma constrI:
  assumes "chain E" "\<And> X n. ((F(X) \<and> E(n + 1)) = (F(X \<and> E(n)) \<and> E (n + 1)))"
  shows "constr F E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. constr F E
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain E
(F ?X \<and> E (?n + 1)) = (F (?X \<and> E ?n) \<and> E (?n + 1))

goal (1 subgoal):
 1. constr F E
[PROOF STEP]
by (auto simp add: constr_def)