[STATEMENT]
lemma dg_prod_2_ArrI:
  assumes "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" and "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
  shows "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
proof(intro vproductI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [g, f]\<^sub>\<circ> = 2\<^sub>\<nat>
 3. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> [g, f]\<^sub>\<circ> = 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [g, f]\<^sub>\<circ> = 2\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps two)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [g, f]\<^sub>\<circ> = 2\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> 2\<^sub>\<nat>"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[PROOF STEP]
consider \<open>i = 0\<close> | \<open>i = 1\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "[g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0 then \<AA> else \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by cases (simp_all add: nat_omega_simps assms(1,2))
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv [g, f]\<^sub>\<circ>
[PROOF STEP]
qed auto


[STATEMENT]
lemma dg_prod_2_ArrI'[dg_prod_cs_intros]:
  assumes "gf = [g, f]\<^sub>\<circ>" and "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" and "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
  shows "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding assms(1)
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (rule dg_prod_2_ArrI)


[STATEMENT]
lemma dg_prod_2_ArrE:
  assumes "gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
  obtains g f where "gf = [g, f]\<^sub>\<circ>" and "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" and "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproductD[OF assms[unfolded dg_prod_2_def dg_prod_components]]
[PROOF STATE]
proof (chain)
picking this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
\<forall>i\<in>elts (2\<^sub>\<nat>). gf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
have vsv_gf: "vsv gf"
    and dom_gf: "\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>"
    and gf_app: "\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = 0 then \<AA> else \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
\<forall>i\<in>elts (2\<^sub>\<nat>). gf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv gf &&& \<D>\<^sub>\<circ> gf = 2\<^sub>\<nat> &&& (\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have dom_gf[simp]: "\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
[PROOF STEP]
unfolding dom_gf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2\<^sub>\<nat> = 2\<^sub>\<nat>
[PROOF STEP]
by (simp add: two)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret vsv gf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv gf
[PROOF STEP]
by (rule vsv_gf)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "gf = [vpfst gf, vpsnd gf]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (rule vsv_vfsequence_two[symmetric]) auto
[PROOF STATE]
proof (state)
this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from gf_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "vpfst gf \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from gf_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "vpsnd gf \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
\<lbrakk>gf = [?g, ?f]\<^sub>\<circ>; ?g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; ?f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_is_arrI:
  assumes "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c" and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
  shows "[g, f]\<^sub>\<circ> : [a, b]\<^sub>\<circ> \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> [c, d]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> : [a, b]\<^sub>\<circ> \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> [c, d]\<^sub>\<circ>
[PROOF STEP]
unfolding dg_prod_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> : [a, b]\<^sub>\<circ> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>
[PROOF STEP]
proof(rule dg_prod_is_arrI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [g, f]\<^sub>\<circ> = 2\<^sub>\<nat>
 3. vsv [a, b]\<^sub>\<circ>
 4. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
 5. vsv [c, d]\<^sub>\<circ>
 6. \<D>\<^sub>\<circ> [c, d]\<^sub>\<circ> = 2\<^sub>\<nat>
 7. \<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
show "[g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = 0 then \<AA> else \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>"
    if "i \<in>\<^sub>\<circ> 2\<^sub>\<nat>" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[PROOF STEP]
consider \<open>i = 0\<close> | \<open>i = 1\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> 2\<^sub>\<nat>

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding two
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "[g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = 0 then \<AA> else \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
by cases (simp_all add: nat_omega_simps assms)
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ>\<lparr>i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> [g, f]\<^sub>\<circ>\<lparr>?i\<rparr> : [a, b]\<^sub>\<circ>\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> [c, d]\<^sub>\<circ>\<lparr>?i\<rparr>

goal (6 subgoals):
 1. vsv [g, f]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [g, f]\<^sub>\<circ> = 2\<^sub>\<nat>
 3. vsv [a, b]\<^sub>\<circ>
 4. \<D>\<^sub>\<circ> [a, b]\<^sub>\<circ> = 2\<^sub>\<nat>
 5. vsv [c, d]\<^sub>\<circ>
 6. \<D>\<^sub>\<circ> [c, d]\<^sub>\<circ> = 2\<^sub>\<nat>
[PROOF STEP]
qed (auto simp: nat_omega_simps two)


[STATEMENT]
lemma dg_prod_2_is_arrI'[dg_prod_cs_intros]:
  assumes "gf = [g, f]\<^sub>\<circ>"
    and "ab = [a, b]\<^sub>\<circ>"
    and "cd = [c, d]\<^sub>\<circ>"
    and "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c"
    and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
  shows "gf : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gf : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd
[PROOF STEP]
using assms(4,5)
[PROOF STATE]
proof (prove)
using this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. gf : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd
[PROOF STEP]
unfolding assms(1,2,3)
[PROOF STATE]
proof (prove)
using this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> : [a, b]\<^sub>\<circ> \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> [c, d]\<^sub>\<circ>
[PROOF STEP]
by (rule dg_prod_2_is_arrI)


[STATEMENT]
lemma dg_prod_2_Dom_vsv: "vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_2_Dom_vdomain[dg_cs_simps]:
  "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_2_Dom_app[dg_prod_cs_simps]:
  assumes "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
  shows "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain ab cd where gf: "[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>ab cd. [g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: is_arrI)
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd
[PROOF STEP]
have Dom_gf: "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = ab"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = ab
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = ab

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from gf
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd
[PROOF STEP]
obtain a b c d
    where ab_def: "ab = [a, b]\<^sub>\<circ>"
      and "cd = [c, d]\<^sub>\<circ>"
      and "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c"
      and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_2_is_arrE[OF \<AA> \<BB>]) simp
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
cd = [c, d]\<^sub>\<circ>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ab = [a, b]\<^sub>\<circ>
cd = [c, d]\<^sub>\<circ>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d
[PROOF STEP]
have Dom_g: "\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr> = a" and Dom_f: "\<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = b"
[PROOF STATE]
proof (prove)
using this:
ab = [a, b]\<^sub>\<circ>
cd = [c, d]\<^sub>\<circ>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. \<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr> = a &&& \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
by (simp_all add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr> = a
\<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = b

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding Dom_gf ab_def Dom_g Dom_f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> = [a, b]\<^sub>\<circ>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_Dom_vrange: "\<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
[PROOF STEP]
by (rule dg_prod_2_Dom_vsv)
[PROOF STATE]
proof (state)
this:
vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix gf
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain g f where gf_def: "gf = [g, f]\<^sub>\<circ>"
    and g: "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and f: "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_2_ArrE[OF \<AA> \<BB>]) simp
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from g f
[PROOF STATE]
proof (chain)
picking this:
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain a b c d where g: "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c" and f: "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>a c b d. \<lbrakk>g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro!: is_arrI)
[PROOF STATE]
proof (state)
this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> g f
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding gf_def dg_prod_2_Dom_app[OF prems[unfolded gf_def]]
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. [\<AA>\<lparr>Dom\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Dom\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_Cod_vsv: "vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_2_Cod_vdomain[dg_cs_simps]:
  "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_prod_2_Cod_app[dg_prod_cs_simps]:
  assumes "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
  shows "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain ab cd where gf: "[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>ab cd. [g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: is_arrI)
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd
[PROOF STEP]
have Cod_gf: "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = cd"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = cd
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = cd

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
from gf
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd
[PROOF STEP]
obtain a b c d
    where "ab = [a, b]\<^sub>\<circ>"
      and cd_def: "cd = [c, d]\<^sub>\<circ>"
      and "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c"
      and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_2_is_arrE[OF \<AA> \<BB>]) simp
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
cd = [c, d]\<^sub>\<circ>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ab = [a, b]\<^sub>\<circ>
cd = [c, d]\<^sub>\<circ>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d
[PROOF STEP]
have Cod_g: "\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr> = c" and Cod_f: "\<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = d"
[PROOF STATE]
proof (prove)
using this:
ab = [a, b]\<^sub>\<circ>
cd = [c, d]\<^sub>\<circ>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. \<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr> = c &&& \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = d
[PROOF STEP]
by (simp_all add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr> = c
\<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = d

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding Cod_gf cd_def Cod_g Cod_f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [c, d]\<^sub>\<circ> = [c, d]\<^sub>\<circ>
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_Cod_vrange: "\<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)
[PROOF STEP]
by (rule dg_prod_2_Cod_vsv)
[PROOF STATE]
proof (state)
this:
vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix gf
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain g f where gf_def: "gf = [g, f]\<^sub>\<circ>"
    and g: "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and f: "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dg_prod_2_ArrE[OF \<AA> \<BB>]) simp
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from g f
[PROOF STATE]
proof (chain)
picking this:
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain a b c d where g: "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c" and f: "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>a c b d. \<lbrakk>g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro!: is_arrI)
[PROOF STATE]
proof (state)
this:
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> g f
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding gf_def dg_prod_2_Cod_app[OF prems[unfolded gf_def]]
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g : a \<mapsto>\<^bsub>\<AA>\<^esub> c
f : b \<mapsto>\<^bsub>\<BB>\<^esub> d

goal (1 subgoal):
 1. [\<AA>\<lparr>Cod\<rparr>\<lparr>g\<rparr>, \<BB>\<lparr>Cod\<rparr>\<lparr>f\<rparr>]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_cs_intros
      )
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_op_dg_dg_Obj[dg_op_simps]:
  "(op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof
  (
    intro vsubset_antisym vsubsetI;
    elim dg_prod_2_ObjE[OF \<AA>.digraph_op \<BB>] dg_prod_2_ObjE[OF \<AA> \<BB>],
    (unfold dg_op_simps)?
  )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
 2. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
 2. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
 2. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_op_intros dg_prod_cs_intros
      )
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_dg_op_dg_Obj[dg_op_simps]:
  "(\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
proof
  (
    intro vsubset_antisym vsubsetI;
    elim dg_prod_2_ObjE[OF \<AA> \<BB>.digraph_op] dg_prod_2_ObjE[OF \<AA> \<BB>],
    (unfold dg_op_simps)?
  )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
 2. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
 2. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
 2. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>x = [a, b]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros dg_op_intros
      )
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_op_dg_dg_Arr[dg_op_simps]:
  "(op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
proof
  (
    intro vsubset_antisym vsubsetI;
    elim dg_prod_2_ArrE[OF \<AA>.digraph_op \<BB>] dg_prod_2_ArrE[OF \<AA> \<BB>],
    (unfold dg_op_simps)?
  )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
 2. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
 2. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
 2. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros dg_op_intros
      )
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_2_dg_op_dg_Arr[dg_op_simps]:
  "(\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr> = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
proof
  (
    intro vsubset_antisym vsubsetI;
    elim dg_prod_2_ArrE[OF \<AA> \<BB>.digraph_op] dg_prod_2_ArrE[OF \<AA> \<BB>],
    (unfold dg_op_simps)?
  )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
 2. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
 2. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
 2. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
fix ab a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "ab = [a, b]\<^sub>\<circ>" "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" "b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
ab = [a, b]\<^sub>\<circ>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x g f. \<lbrakk>x = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> x \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
from \<AA> \<BB> prems(2,3)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding prems(1) dg_op_simps
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_prod_cs_intros dg_op_intros
      )
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed