[STATEMENT]
lemma (in is_dghm) dghm_dghm_comp_dghm_id_left: "dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<FF>"
  \<comment>\<open>See Chapter I-3 in \cite{mac_lane_categories_2010}).\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<FF>
[PROOF STEP]
proof(rule dghm_eqI [of \<alpha> \<AA> \<BB> _ \<AA> \<BB>])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
 4. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \<BB> = \<BB>
[PROOF STEP]
show "(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)

goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (3 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
[PROOF STATE]
proof (state)
this:
(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>

goal (5 subgoals):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 4. \<AA> = \<AA>
 5. \<BB> = \<BB>
[PROOF STEP]
show "(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)

goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr>

goal (3 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
[PROOF STATE]
proof (state)
this:
(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>

goal (4 subgoals):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<AA> = \<AA>
 4. \<BB> = \<BB>
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: cs_intro: dg_cs_intros)+


[STATEMENT]
lemma (in is_dghm) dghm_dghm_comp_dghm_id_right: "\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> = \<FF>"
  \<comment>\<open>See Chapter I-3 in \cite{mac_lane_categories_2010}).\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> = \<FF>
[PROOF STEP]
proof(rule dghm_eqI [of \<alpha> \<AA> \<BB> _ \<AA> \<BB>])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
 4. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>) \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>)" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>)

goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>) \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (3 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>)
 2. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>

goal (5 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 4. \<AA> = \<AA>
 5. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>) \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>)" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>)

goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>) \<Longrightarrow> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr>

goal (3 subgoals):
 1. vsv ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>)
 2. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>

goal (4 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<AA> = \<AA>
 4. \<BB> = \<BB>
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+


[STATEMENT]
lemma dghm_const_components:
  shows "dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr> = vconst_on (\<CC>\<lparr>Obj\<rparr>) a"
    and "dghm_const \<CC> \
 a f\<lparr>ArrMap\<rparr> = vconst_on (\<CC>\<lparr>Arr\<rparr>) f"
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_const \<CC> \
 a f\<lparr>HomDom\<rparr> = \<CC>"
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_const \<CC> \
 a f\<lparr>HomCod\<rparr> = \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr> = vconst_on (\<CC>\<lparr>Obj\<rparr>) a &&& dghm_const \<CC> \
 a f\<lparr>ArrMap\<rparr> = vconst_on (\<CC>\<lparr>Arr\<rparr>) f) &&& dghm_const \<CC> \
 a f\<lparr>HomDom\<rparr> = \<CC> &&& dghm_const \<CC> \
 a f\<lparr>HomCod\<rparr> = \

[PROOF STEP]
unfolding dghm_const_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([vconst_on (\<CC>\<lparr>Obj\<rparr>) a, vconst_on (\<CC>\<lparr>Arr\<rparr>) f, \<CC>, \
]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = vconst_on (\<CC>\<lparr>Obj\<rparr>) a &&& [vconst_on (\<CC>\<lparr>Obj\<rparr>) a, vconst_on (\<CC>\<lparr>Arr\<rparr>) f, \<CC>, \
]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = vconst_on (\<CC>\<lparr>Arr\<rparr>) f) &&& [vconst_on (\<CC>\<lparr>Obj\<rparr>) a, vconst_on (\<CC>\<lparr>Arr\<rparr>) f, \<CC>, \
]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<CC> &&& [vconst_on (\<CC>\<lparr>Obj\<rparr>) a, vconst_on (\<CC>\<lparr>Arr\<rparr>) f, \<CC>, \
]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \

[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma dghm_const_is_dghm:
  assumes "digraph \<alpha> \<CC>" and "digraph \<alpha> \
" and "f : a \<mapsto>\<^bsub>\
\<^esub> a"
  shows "dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
interpret \
: digraph \<alpha> \

[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> \

[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
proof(intro is_dghmI)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dghm_const \<CC> \
 a f)
 3. digraph \<alpha> \<CC>
 4. digraph \<alpha> \

 5. vcard (dghm_const \<CC> \
 a f) = 4\<^sub>\<nat>
 6. dghm_const \<CC> \
 a f\<lparr>HomDom\<rparr> = \<CC>
 7. dghm_const \<CC> \
 a f\<lparr>HomCod\<rparr> = \

 8. vsv (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>)
 9. vsv (dghm_const \<CC> \
 a f\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (dghm_const \<CC> \
 a f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dghm_const \<CC> \
 a f)
[PROOF STEP]
unfolding dghm_const_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [vconst_on (\<CC>\<lparr>Obj\<rparr>) a, vconst_on (\<CC>\<lparr>Arr\<rparr>) f, \<CC>, \
]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (dghm_const \<CC> \
 a f)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> \

 4. vcard (dghm_const \<CC> \
 a f) = 4\<^sub>\<nat>
 5. dghm_const \<CC> \
 a f\<lparr>HomDom\<rparr> = \<CC>
 6. dghm_const \<CC> \
 a f\<lparr>HomCod\<rparr> = \

 7. vsv (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>)
 8. vsv (dghm_const \<CC> \
 a f\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \
\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (dghm_const \<CC> \
 a f) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dghm_const \<CC> \
 a f) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_const_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [vconst_on (\<CC>\<lparr>Obj\<rparr>) a, vconst_on (\<CC>\<lparr>Arr\<rparr>) f, \<CC>, \
]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dghm_const \<CC> \
 a f) = 4\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> \

 4. dghm_const \<CC> \
 a f\<lparr>HomDom\<rparr> = \<CC>
 5. dghm_const \<CC> \
 a f\<lparr>HomCod\<rparr> = \

 6. vsv (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_const \<CC> \
 a f\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (dghm_const \<CC> \
 a f\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \
\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (dghm_const \<CC> \
 a f\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
qed
    (
      use assms in
        \<open>
          cs_concl
            cs_simp: dghm_const_components(1) dg_cs_simps
            cs_intro: V_cs_intros dg_cs_intros
        \<close>
    )+
[PROOF STATE]
proof (state)
this:
dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_const_is_dghm'[dg_cs_intros]:
  assumes "digraph \<alpha> \<CC>"
    and "digraph \<alpha> \
"
    and "f : a \<mapsto>\<^bsub>\
\<^esub> a"
    and "\<AA> = \<CC>"
    and "\<BB> = \
"
  shows "dghm_const \<CC> \
 a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<CC>
digraph \<alpha> \

f : a \<mapsto>\<^bsub>\
\<^esub> a

goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding assms(4,5)
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<CC>
digraph \<alpha> \

f : a \<mapsto>\<^bsub>\
\<^esub> a

goal (1 subgoal):
 1. dghm_const \<CC> \
 a f : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule dghm_const_is_dghm)


[STATEMENT]
lemma (in is_dghm) dghm_dghm_comp_dghm_const[dg_cs_simps]:
  assumes "digraph \<alpha> \<CC>" and "f : a \<mapsto>\<^bsub>\<CC>\<^esub> a"
  shows "dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_const \<AA> \<CC> a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_const \<AA> \<CC> a f
[PROOF STEP]
proof(rule dghm_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_const \<AA> \<CC> a f : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\

 3. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
 4. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
interpret \<CC>: digraph \<alpha> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_const \<AA> \<CC> a f : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\

 3. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
 4. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a
[PROOF STEP]
show "dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a

goal (1 subgoal):
 1. dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. dghm_const \<AA> \<CC> a f : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
 3. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 4. \<AA> = ?\<CC>
 5. \<CC> = ?\

[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a
dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have ObjMap_dom_lhs:
    "\<D>\<^sub>\<circ> ((dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
    and ArrMap_dom_lhs: "\<D>\<^sub>\<circ> ((dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a
dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr> &&& \<D>\<^sub>\<circ> ((dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> ((dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>

goal (5 subgoals):
 1. dghm_const \<AA> \<CC> a f : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
 3. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 4. \<AA> = ?\<CC>
 5. \<CC> = ?\

[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a
[PROOF STEP]
show "dghm_const \<AA> \<CC> a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a

goal (1 subgoal):
 1. dghm_const \<AA> \<CC> a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_const \<AA> \<CC> a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (4 subgoals):
 1. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
 2. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 3. \<AA> = \<AA>
 4. \<CC> = \<CC>
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a
dghm_const \<AA> \<CC> a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have ObjMap_dom_rhs: "\<D>\<^sub>\<circ> (dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
    and ArrMap_dom_rhs: "\<D>\<^sub>\<circ> (dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> a
dghm_const \<AA> \<CC> a f : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr> &&& \<D>\<^sub>\<circ> (dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> (dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
 2. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 3. \<AA> = \<AA>
 4. \<CC> = \<CC>
[PROOF STEP]
show "(dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>
[PROOF STEP]
by (rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
      (
        use assms(2) in
          \<open>cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros\<close>
      )+
[PROOF STATE]
proof (state)
this:
(dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
 2. \<AA> = \<AA>
 3. \<CC> = \<CC>
[PROOF STEP]
show "(dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>
[PROOF STEP]
by (rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
      (
        use assms(2) in
          \<open>cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros\<close>
      )+
[PROOF STATE]
proof (state)
this:
(dghm_const \<BB> \<CC> a f \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_const \<AA> \<CC> a f\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. \<AA> = \<AA>
 2. \<CC> = \<CC>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma (in is_ft_dghm) is_ft_dghm_axioms'[dghm_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>"
  shows "\<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule is_ft_dghm_axioms)


[STATEMENT]
lemma is_ft_dghmI'':
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<And>a b g f.
      \<lbrakk> g : a \<mapsto>\<^bsub>\<AA>\<^esub> b; f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<rbrakk> \<Longrightarrow> g = f"
  shows "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_ft_dghmI assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
interpret \<FF>: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
have dom_def: "\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b) = Hom \<AA> a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b) = Hom \<AA> a b
[PROOF STEP]
by (intro vdomain_vlrestriction_vsubset vsubsetI) (auto simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b) = Hom \<AA> a b

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
show "v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
proof(intro vsv.vsv_valeq_v11I, unfold dom_def dg_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
 2. \<And>x y. \<lbrakk>x : a \<mapsto>\<^bsub>\<AA>\<^esub> b; y : a \<mapsto>\<^bsub>\<AA>\<^esub> b; (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>x\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x : a \<mapsto>\<^bsub>\<AA>\<^esub> b; y : a \<mapsto>\<^bsub>\<AA>\<^esub> b; (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>x\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix g f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x : a \<mapsto>\<^bsub>\<AA>\<^esub> b; y : a \<mapsto>\<^bsub>\<AA>\<^esub> b; (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>x\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume prems:
      "g : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
      "(\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>"
[PROOF STATE]
proof (state)
this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
(\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x : a \<mapsto>\<^bsub>\<AA>\<^esub> b; y : a \<mapsto>\<^bsub>\<AA>\<^esub> b; (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>x\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from prems(3,1,2)
[PROOF STATE]
proof (chain)
picking this:
(\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have \<FF>g_\<FF>f: "\<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
using this:
(\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
by
        (
          cs_prems
            cs_simp: V_cs_simps dg_cs_simps
            cs_intro: V_cs_intros dg_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x : a \<mapsto>\<^bsub>\<AA>\<^esub> b; y : a \<mapsto>\<^bsub>\<AA>\<^esub> b; (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>x\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "g = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
by (rule assms(2)[OF prems(1,2) \<FF>g_\<FF>f])
[PROOF STATE]
proof (state)
this:
g = f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_ft_dghm) ft_dghm_op_dghm_is_ft_dghm:
  "op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by
    (
      rule is_ft_dghmI,
      unfold dg_op_simps,
      cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros
    )
    (auto simp: ft_dghm_v11_on_Hom)


[STATEMENT]
lemma (in is_ft_dghm) ft_dghm_op_dghm_is_ft_dghm'[dg_op_intros]:
  assumes "\<AA>' = op_dg \<AA>" and "\<BB>' = op_dg \<BB>"
  shows "op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule ft_dghm_op_dghm_is_ft_dghm)


[STATEMENT]
lemma dghm_comp_is_ft_dghm[dghm_cs_intros]:
  \<comment>\<open>See Chapter I-3 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret L: is_ft_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret R: is_ft_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have inj:
    "\<lbrakk> a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> ; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)"
    for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have \<GG>_hom_\<BB>:
      "v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>))"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>))
[PROOF STEP]
by (intro L.ft_dghm_v11_on_Hom)
        (cs_concl cs_shallow cs_intro: dg_cs_intros)+
[PROOF STATE]
proof (state)
this:
v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>))

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
have "v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
proof(intro v11_vlrestriction_vsubset[OF \<GG>_hom_\<BB>] vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
assume "g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b"
[PROOF STATE]
proof (state)
this:
g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b
[PROOF STEP]
obtain f where f: "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and g_def: "g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f : a \<mapsto>\<^bsub>\<AA>\<^esub> b; g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show "g \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. g \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: g_def cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
g \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b)

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
show "v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)"
[PROOF STATE]
proof (prove)
using this:
v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b)

goal (1 subgoal):
 1. v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
unfolding dghm_comp_components
[PROOF STATE]
proof (prove)
using this:
v11 (\<GG>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b)

goal (1 subgoal):
 1. v11 ((\<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>) \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
by (intro v11_vlrestriction_vcomp) (auto simp: R.ft_dghm_v11_on_Hom prems)
[PROOF STATE]
proof (state)
this:
v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> ?a ?b)

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> ?a ?b)
[PROOF STEP]
show "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> ?a ?b)

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (intro is_ft_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros) auto
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_ft_dghm) ft_dghm_ArrMap_eqD:
  assumes "g : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and "\<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
  shows "g = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and b: "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b

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

goal (1 subgoal):
 1. g = f
[PROOF STEP]
interpret ArrMap: v11 \<open>\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)
[PROOF STEP]
by (rule ft_dghm_v11_on_Hom[OF a b])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
have dom_def: "\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b) = Hom \<AA> a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b) = Hom \<AA> a b
[PROOF STEP]
by (intro vdomain_vlrestriction_vsubset vsubsetI) (auto simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b) = Hom \<AA> a b

goal (1 subgoal):
 1. g = f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
proof(rule ArrMap.v11_injective[unfolded dom_def dg_cs_simps, OF assms(1,2)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show
      "(\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> b
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: dg_cs_simps assms(3) vsv.vlrestriction_atI
            cs_intro: V_cs_intros dg_cs_intros
        )
[PROOF STATE]
proof (state)
this:
(\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>g\<rparr> = (\<FF>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom \<AA> a b)\<lparr>f\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g = f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_fl_dghm) is_fl_dghm_axioms'[dghm_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>"
  shows "\<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule is_fl_dghm_axioms)


[STATEMENT]
lemma (in is_fl_dghm) fl_dghm_op_dghm_is_fl_dghm:
  "op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by
    (
      rule is_fl_dghmI,
      unfold dg_op_simps,
      cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros
    )
    (auto simp: fl_dghm_surj_on_Hom)


[STATEMENT]
lemma (in is_fl_dghm) fl_dghm_op_dghm_is_fl_dghm'[dg_op_intros]:
  assumes "\<AA>' = op_dg \<AA>" and "\<BB>' = op_dg \<BB>"
  shows "op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule fl_dghm_op_dghm_is_fl_dghm)


[STATEMENT]
lemma dghm_comp_is_fl_dghm[dghm_cs_intros]:
  \<comment>\<open>See Chapter I-3 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret L: is_fl_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret R: is_fl_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have surj:
    "\<lbrakk> a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<rbrakk> \<Longrightarrow>
      (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> (Hom \<AA> a b) =
        Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
    for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
have surj_\<FF>: "\<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by (rule R.fl_dghm_surj_on_Hom[OF prems])
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
from prems L.is_dghm_axioms R.is_dghm_axioms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have comp_Obj:
      "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
      "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> &&& (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>
[PROOF STEP]
by (auto simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
have "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b
[PROOF STEP]
unfolding dghm_comp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>) `\<^sub>\<circ> Hom \<AA> a b = \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b
[PROOF STEP]
by (simp add: vcomp_vimage)
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have
      "\<dots> = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
unfolding surj_\<FF> comp_Obj
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = Hom \<CC> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>) (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>)
[PROOF STEP]
by
        (
          simp add:
            prems(2) L.fl_dghm_surj_on_Hom R.dghm_ObjMap_app_in_HomCod_Obj
        )
[PROOF STATE]
proof (state)
this:
\<GG>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
show "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> (Hom \<AA> a b) =
      Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> ?a ?b = Hom \<CC> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>) ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr>)

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule is_fl_dghmI, cs_concl cs_shallow cs_intro: dg_cs_intros)
      (auto simp: surj)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>u\<^sub>l\<^sub>l\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_ff_dghm) is_ff_dghm_axioms'[dghm_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>"
  shows "\<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule is_ff_dghm_axioms)


[STATEMENT]
lemma (in is_ff_dghm) ff_dghm_op_dghm_is_ff_dghm:
  "op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule is_ff_dghmI) (cs_concl cs_shallow cs_intro: dg_op_intros)+


[STATEMENT]
lemma (in is_ff_dghm) ff_dghm_op_dghm_is_ff_dghm'[dg_op_intros]:
  assumes "\<AA>' = op_dg \<AA>" and "\<BB>' = op_dg \<BB>"
  shows "op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule ff_dghm_op_dghm_is_ff_dghm)


[STATEMENT]
lemma dghm_comp_is_ff_dghm[dghm_cs_intros]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>f\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (intro is_ff_dghmI, elim is_ff_dghmE) (cs_concl cs_intro: dghm_cs_intros)


[STATEMENT]
lemma (in is_iso_dghm) is_iso_dghm_axioms'[dghm_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>"
  shows "\<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule is_iso_dghm_axioms)


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_Arr_HomDom_if_Arr_HomCod[elim]:
  assumes "g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
  obtains f where "f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" and "g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms ArrMap.vrange_atD iso_dghm_ArrMap_vrange
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
?b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<exists>a\<in>elts (\<AA>\<lparr>Arr\<rparr>). \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = ?b
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_ObjMap_eqE[elim]:
  assumes "\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
    and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "a = b \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms ObjMap.v11_eq_iff
[PROOF STATE]
proof (prove)
using this:
\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
a = b \<Longrightarrow> P
\<lbrakk>?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr>) = (?a = ?b)

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_ArrMap_eqE[elim]:
  assumes "\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>"
    and "f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and "f = g \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms ArrMap.v11_eq_iff
[PROOF STATE]
proof (prove)
using this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr>
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f = g \<Longrightarrow> P
\<lbrakk>?a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; ?b \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> (\<FF>\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>?b\<rparr>) = (?a = ?b)

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto


[STATEMENT]
lemma (in is_iso_dghm) is_iso_dghm_op:
  "op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (intro is_iso_dghmI, unfold dg_op_simps)
    (
      cs_concl cs_shallow
        cs_simp: dghm_cs_simps cs_intro: V_cs_intros dg_cs_intros dg_op_intros
    )+


[STATEMENT]
lemma (in is_iso_dghm) is_iso_dghm_op':
  assumes "\<AA>' = op_dg \<AA>" and "\<BB>' = op_dg \<BB>"
  shows "op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule is_iso_dghm_op)


[STATEMENT]
lemma dghm_comp_is_iso_dghm[dghm_cs_intros]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<FF>: is_iso_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<GG>: is_iso_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (intro is_iso_dghmI, unfold dghm_comp_components)
      (
        cs_concl
          cs_simp: V_cs_simps dg_cs_simps dghm_cs_simps
          cs_intro: dg_cs_intros V_cs_intros
      )+
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in digraph) dg_dghm_id_is_iso_dghm: "dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule is_iso_dghmI) (simp_all add: dg_dghm_id_is_dghm dghm_id_components)


[STATEMENT]
lemma (in digraph) dg_dghm_id_is_iso_dghm'[dghm_cs_intros]:
  assumes "\<AA>' = \<CC>" and "\<BB>' = \<CC>"
  shows "dghm_id \<CC> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<CC> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule dg_dghm_id_is_iso_dghm)


[STATEMENT]
lemma inv_dghm_components:
  shows "inv_dghm \<FF>\<lparr>ObjMap\<rparr> = (\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>"
    and "inv_dghm \<FF>\<lparr>ArrMap\<rparr> = (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>"
    and [dghm_cs_simps]: "inv_dghm \<FF>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomCod\<rparr>"
    and [dghm_cs_simps]: "inv_dghm \<FF>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomDom\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv_dghm \<FF>\<lparr>ObjMap\<rparr> = (\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ> &&& inv_dghm \<FF>\<lparr>ArrMap\<rparr> = (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>) &&& inv_dghm \<FF>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomCod\<rparr> &&& inv_dghm \<FF>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomDom\<rparr>
[PROOF STEP]
unfolding inv_dghm_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([(\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>)\<inverse>\<^sub>\<circ>, (\<FF>\<lparr>1\<^sub>\<nat>\<rparr>)\<inverse>\<^sub>\<circ>, \<FF>\<lparr>3\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>)\<inverse>\<^sub>\<circ> &&& [(\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>)\<inverse>\<^sub>\<circ>, (\<FF>\<lparr>1\<^sub>\<nat>\<rparr>)\<inverse>\<^sub>\<circ>, \<FF>\<lparr>3\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<FF>\<lparr>1\<^sub>\<nat>\<rparr>)\<inverse>\<^sub>\<circ>) &&& [(\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>)\<inverse>\<^sub>\<circ>, (\<FF>\<lparr>1\<^sub>\<nat>\<rparr>)\<inverse>\<^sub>\<circ>, \<FF>\<lparr>3\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<FF>\<lparr>3\<^sub>\<nat>\<rparr> &&& [(\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>)\<inverse>\<^sub>\<circ>, (\<FF>\<lparr>1\<^sub>\<nat>\<rparr>)\<inverse>\<^sub>\<circ>, \<FF>\<lparr>3\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<FF>\<lparr>2\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ObjMap_v11[dghm_cs_intros]:
  "v11 (inv_dghm \<FF>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (inv_dghm \<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 ((\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: V_cs_intros)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ObjMap_vdomain[dghm_cs_simps]:
  "\<D>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>) = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dghm_cs_simps V_cs_simps)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ObjMap_app[dghm_cs_simps]:
  assumes "a' = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>" and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a'\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a'\<rparr> = a
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>\<lparr>a'\<rparr> = a
[PROOF STEP]
by (metis assms ObjMap.vconverse_atI ObjMap.vsv_vconverse vsv.vsv_appI)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ObjMap_vrange[dghm_cs_simps]:
  "\<R>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps V_cs_simps)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ArrMap_v11[dghm_cs_intros]:
  "v11 (inv_dghm \<FF>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (inv_dghm \<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 ((\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: V_cs_intros)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ArrMap_vdomain[dghm_cs_simps]:
  "\<D>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dghm_cs_simps V_cs_simps)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ArrMap_app[dghm_cs_simps]:
  assumes "a' = \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>" and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
  shows "inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>a'\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>a'\<rparr> = a
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>\<lparr>a'\<rparr> = a
[PROOF STEP]
by (metis assms ArrMap.vconverse_atI ArrMap.vsv_vconverse vsv.vsv_appI)


[STATEMENT]
lemma (in is_iso_dghm) inv_dghm_ArrMap_vrange[dghm_cs_simps]:
  "\<R>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (inv_dghm \<FF>\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding inv_dghm_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps V_cs_simps)


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_ObjMap_inv_dghm_ObjMap_app[dghm_cs_simps]:
  assumes "a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
  shows "\<FF>\<lparr>ObjMap\<rparr>\<lparr>inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a
[PROOF STEP]
by (cs_concl cs_simp: inv_dghm_components V_cs_simps)


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_ArrMap_inv_dghm_ArrMap_app[dghm_cs_simps]:
  assumes "f : a \<mapsto>\<^bsub>\<BB>\<^esub> b"
  shows "\<FF>\<lparr>ArrMap\<rparr>\<lparr>inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f
[PROOF STEP]
by (cs_concl cs_simp: inv_dghm_components V_cs_simps cs_intro: dg_cs_intros)


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_HomDom_is_arr_conv:
  assumes "f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
  shows "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
by
    (
      metis
        assms
        HomDom.dg_is_arrE
        is_arr_def
        dghm_ArrMap_is_arr
        iso_dghm_ObjMap_eqE
    )


[STATEMENT]
lemma (in is_iso_dghm) iso_dghm_HomCod_is_arr_conv:
  assumes "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
    and "a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
    and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
    and "inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
  shows "f : a \<mapsto>\<^bsub>\<BB>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>\<BB>\<^esub> b
[PROOF STEP]
by
    (
      metis
        assms
        dghm_ArrMap_is_arr'
        is_arrI
        iso_dghm_ArrMap_inv_dghm_ArrMap_app
        iso_dghm_ObjMap_inv_dghm_ObjMap_app
    )