[STATEMENT]
lemma (in pdigraph_base) dg_prod_is_arrI:
  assumes "vsv f"
    and "\<D>\<^sub>\<circ> f = I"
    and "vsv a"
    and "\<D>\<^sub>\<circ> a = I"
    and "vsv b"
    and "\<D>\<^sub>\<circ> b = I"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>"
  shows "f : a \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b
[PROOF STEP]
proof(intro is_arrI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
interpret f: vsv f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv f
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
interpret a: vsv a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv a
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
interpret b: vsv b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv b
[PROOF STEP]
by (rule assms(5))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
from assms(7)
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
[PROOF STEP]
have f_components: "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Arr\<rparr>

goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
from assms(7)
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
[PROOF STEP]
have a_components: "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by (meson digraph.dg_is_arrD(2) pdg_digraphs)
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
from assms(7)
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
[PROOF STEP]
have b_components: "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> b\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> b\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by (meson digraph.dg_is_arrD(3) pdg_digraphs)
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> b\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
 2. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 3. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
show f_in_Arr: "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
by (intro vproductI)
      (auto simp: f_components assms(2) f.vsv_vrange_vsubset_vifunion_app)
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
 2. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
show "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>)
 2. vsv a
 3. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> a
 4. \<And>aa. aa \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>aa\<rparr> = a\<lparr>aa\<rparr>
[PROOF STEP]
from dg_prod_Dom_app_in_Obj[OF f_in_Arr]
[PROOF STATE]
proof (chain)
picking this:
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>)
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
(\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. vsv ((\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr>)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>)

goal (3 subgoals):
 1. vsv a
 2. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> a
 3. \<And>aa. aa \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>aa\<rparr> = a\<lparr>aa\<rparr>
[PROOF STEP]
from dg_prod_Dom_app_in_Obj[OF f_in_Arr] assms(4)
[PROOF STATE]
proof (chain)
picking this:
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> a = I
[PROOF STEP]
show [simp]:
      "\<D>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> a"
[PROOF STATE]
proof (prove)
using this:
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> a = I

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> a
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
(\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
\<D>\<^sub>\<circ> a = I

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> a
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> a

goal (2 subgoals):
 1. vsv a
 2. \<And>aa. aa \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>aa\<rparr> = a\<lparr>aa\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv a
 2. \<And>aa. aa \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>aa\<rparr> = a\<lparr>aa\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr>)"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>)

goal (2 subgoals):
 1. vsv a
 2. \<And>aa. aa \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>aa\<rparr> = a\<lparr>aa\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>)
[PROOF STEP]
have i: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>)

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> I
[PROOF STEP]
by (simp add: assms(4))
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (2 subgoals):
 1. vsv a
 2. \<And>aa. aa \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>aa\<rparr> = a\<lparr>aa\<rparr>
[PROOF STEP]
from a_components assms(7) i
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = a\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = a\<lparr>i\<rparr>
[PROOF STEP]
unfolding dg_prod_Dom_app_component_app[OF f_in_Arr i]
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = a\<lparr>i\<rparr>

goal (1 subgoal):
 1. vsv a
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a

goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
show "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>)
 2. vsv b
 3. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> b
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>a\<rparr> = b\<lparr>a\<rparr>
[PROOF STEP]
from dg_prod_Cod_app_in_Obj[OF f_in_Arr]
[PROOF STATE]
proof (chain)
picking this:
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "vsv ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>)
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
(\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. vsv ((\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr>)
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>)

goal (3 subgoals):
 1. vsv b
 2. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> b
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>a\<rparr> = b\<lparr>a\<rparr>
[PROOF STEP]
from dg_prod_Cod_app_in_Obj[OF f_in_Arr] assms(6)
[PROOF STATE]
proof (chain)
picking this:
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> b = I
[PROOF STEP]
show [simp]:
      "\<D>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> b"
[PROOF STATE]
proof (prove)
using this:
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> b = I

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> b
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
(\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
\<D>\<^sub>\<circ> b = I

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> b
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) = \<D>\<^sub>\<circ> b

goal (2 subgoals):
 1. vsv b
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>a\<rparr> = b\<lparr>a\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv b
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>a\<rparr> = b\<lparr>a\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr>)"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>)

goal (2 subgoals):
 1. vsv b
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>a\<rparr> = b\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>)
[PROOF STEP]
have i: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>)

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> I
[PROOF STEP]
by (simp add: assms(6))
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (2 subgoals):
 1. vsv b
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>) \<Longrightarrow> dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>a\<rparr> = b\<lparr>a\<rparr>
[PROOF STEP]
from b_components assms(7) i
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> b\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> b\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
unfolding dg_prod_Cod_app_component_app[OF f_in_Arr i]
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> b\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = b\<lparr>i\<rparr>

goal (1 subgoal):
 1. vsv b
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph_base) dg_prod_is_arrD[dest]:
  assumes "f : a \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<^esub> b"
  shows "vsv f"
    and "\<D>\<^sub>\<circ> f = I"
    and "vsv a"
    and "\<D>\<^sub>\<circ> a = I"
    and "vsv b"
    and "\<D>\<^sub>\<circ> b = I"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vsv f &&& \<D>\<^sub>\<circ> f = I &&& vsv a) &&& (\<D>\<^sub>\<circ> a = I &&& vsv b) &&& \<D>\<^sub>\<circ> b = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv f
 2. \<D>\<^sub>\<circ> f = I
 3. vsv a
 4. \<D>\<^sub>\<circ> a = I
 5. vsv b
 6. \<D>\<^sub>\<circ> b = I
 7. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
from is_arrD[OF assms]
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b
[PROOF STEP]
have f: "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
    and a: "a \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
    and b: "b \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> = a
dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> = b

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

goal (7 subgoals):
 1. vsv f
 2. \<D>\<^sub>\<circ> f = I
 3. vsv a
 4. \<D>\<^sub>\<circ> a = I
 5. vsv b
 6. \<D>\<^sub>\<circ> b = I
 7. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> f = I" "\<D>\<^sub>\<circ> a = I" "\<D>\<^sub>\<circ> b = I" "vsv f" "vsv a" "vsv b"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<D>\<^sub>\<circ> f = I &&& \<D>\<^sub>\<circ> a = I &&& \<D>\<^sub>\<circ> b = I) &&& vsv f &&& vsv a &&& vsv b
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
a \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. (\<D>\<^sub>\<circ> f = I &&& \<D>\<^sub>\<circ> a = I &&& \<D>\<^sub>\<circ> b = I) &&& vsv f &&& vsv a &&& vsv b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> f = I
\<D>\<^sub>\<circ> a = I
\<D>\<^sub>\<circ> b = I
vsv f
vsv a
vsv b

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
show "f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
proof(intro is_arrI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
 2. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr>
 3. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b
[PROOF STEP]
have f: "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
      and a: "a \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
      and b: "b \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b

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

goal (3 subgoals):
 1. f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
 2. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr>
 3. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
from f prems
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
i \<in>\<^sub>\<circ> I

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

goal (2 subgoals):
 1. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr>
 2. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
from a b assms(1) prems dg_prod_components(2,3,4)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b
i \<in>\<^sub>\<circ> I
dg_prod ?I ?\<AA>\<lparr>Arr\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Arr\<rparr>)
dg_prod ?I ?\<AA>\<lparr>Dom\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
dg_prod ?I ?\<AA>\<lparr>Cod\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
show
      "\<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr>" "\<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b
i \<in>\<^sub>\<circ> I
dg_prod ?I ?\<AA>\<lparr>Arr\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Arr\<rparr>)
dg_prod ?I ?\<AA>\<lparr>Dom\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
dg_prod ?I ?\<AA>\<lparr>Cod\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>?I. ?\<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)

goal (1 subgoal):
 1. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr> &&& \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
\<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = a\<lparr>i\<rparr>
\<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr> = b\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph_base) dg_prod_is_arrE[elim]:
  assumes "f : a \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<^esub> b"
  obtains "vsv f"
    and "\<D>\<^sub>\<circ> f = I"
    and "vsv a"
    and "\<D>\<^sub>\<circ> a = I"
    and "vsv b"
    and "\<D>\<^sub>\<circ> b = I"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>vsv f; \<D>\<^sub>\<circ> f = I; vsv a; \<D>\<^sub>\<circ> a = I; vsv b; \<D>\<^sub>\<circ> b = I; \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b

goal (1 subgoal):
 1. (\<lbrakk>vsv f; \<D>\<^sub>\<circ> f = I; vsv a; \<D>\<^sub>\<circ> a = I; vsv b; \<D>\<^sub>\<circ> b = I; \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma (in pdigraph) pdigraph_axioms'[dg_prod_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "I' = I"
  shows "pdigraph \<alpha>' I' \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph \<alpha>' I' \<AA>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph \<alpha> I \<AA>
[PROOF STEP]
by (rule pdigraph_axioms)


[STATEMENT]
lemma (in pdigraph) pdg_Obj_vsubset_Vset': "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule pdg_Obj_vsubset_Vset) simp


[STATEMENT]
lemma (in pdigraph) pdg_Hom_vifunion_in_Vset':
  assumes "A \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
    and "B \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
    and "A \<in>\<^sub>\<circ> Vset \<alpha>"
    and "B \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "(\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. Hom (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i) a b) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod I \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
B \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod I \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro pdg_Hom_vifunion_in_Vset) simp_all


[STATEMENT]
lemma (in pdigraph) pdg_vsubset_index_pdigraph:
  assumes "J \<subseteq>\<^sub>\<circ> I"
  shows "pdigraph \<alpha> J \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph \<alpha> J \<AA>
[PROOF STEP]
proof(intro pdigraphI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pdigraph_base \<alpha> J \<AA>
 2. \<And>Ja. Ja \<subseteq>\<^sub>\<circ> J \<Longrightarrow> dg_prod Ja \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 3. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>" if \<open>J' \<subseteq>\<^sub>\<circ> J\<close> for J'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from that assms
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
have "J' \<subseteq>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
show "dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule pdg_Obj_vsubset_Vset)
[PROOF STATE]
proof (state)
this:
dg_prod J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?J' \<subseteq>\<^sub>\<circ> J \<Longrightarrow> dg_prod ?J' \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. pdigraph_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
fix A B J'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pdigraph_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume prems:
    "J' \<subseteq>\<^sub>\<circ> J"
    "A \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>J'. \<AA> i)\<lparr>Obj\<rparr>"
    "B \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>J'. \<AA> i)\<lparr>Obj\<rparr>"
    "A \<in>\<^sub>\<circ> Vset \<alpha>"
    "B \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> J
A \<subseteq>\<^sub>\<circ> dg_prod J' \<AA>\<lparr>Obj\<rparr>
B \<subseteq>\<^sub>\<circ> dg_prod J' \<AA>\<lparr>Obj\<rparr>
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. pdigraph_base \<alpha> J \<AA>
 2. \<And>Ja A B. \<lbrakk>Ja \<subseteq>\<^sub>\<circ> J; A \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_prod Ja \<AA>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod Ja \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>B. Hom (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>J'. \<AA> i) a b) \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from prems(1) assms
[PROOF STATE]
proof (chain)
picking this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
have "J' \<subseteq>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
J' \<subseteq>\<^sub>\<circ> J
J \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. J' \<subseteq>\<^sub>\<circ> I
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
J' \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from pdg_Hom_vifunion_in_Vset[OF this prems(2-5)]
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_prod J' \<AA>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. pdigraph_base \<alpha> J \<AA>
[PROOF STEP]
qed (rule pdg_vsubset_index_pdigraph_base[OF assms])


[STATEMENT]
lemma (in pdigraph) pdg_digraph_dg_prod: "digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (dg_prod I \<AA>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. digraph \<alpha> (dg_prod I \<AA>)
[PROOF STEP]
interpret tiny_digraph \<open>\<alpha> + \<omega>\<close> \<open>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tiny_digraph (\<alpha> + \<omega>) (dg_prod I \<AA>)
[PROOF STEP]
by (intro pdg_tiny_digraph_dg_prod)
      (auto simp: \<Z>_\<alpha>_\<alpha>\<omega> \<Z>.intro \<Z>_Limit_\<alpha>\<omega> \<Z>_\<omega>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. digraph \<alpha> (dg_prod I \<AA>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (dg_prod I \<AA>)
[PROOF STEP]
by (rule digraph_if_digraph)
      (
        auto
          intro!: pdg_Hom_vifunion_in_Vset pdg_Obj_vsubset_Vset
          intro: dg_cs_intros
      )
[PROOF STATE]
proof (state)
this:
digraph \<alpha> (dg_prod I \<AA>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in finite_pdigraph) finite_pdigraph_axioms'[dg_prod_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "I' = I"
  shows "finite_pdigraph \<alpha>' I' \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha>' I' \<AA>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> I \<AA>
[PROOF STEP]
by (rule finite_pdigraph_axioms)


[STATEMENT]
lemma dg_prod_vunion_Obj_in_Obj:
  assumes "vdisjnt J K"
    and "b \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>J. \<AA> j)\<lparr>Obj\<rparr>"
    and "c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gk\<in>\<^sub>\<circ>K. \<AA> k)\<lparr>Obj\<rparr>"
  shows "b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
interpret b: vsv b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv b
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv b
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. vsv b
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
interpret c: vsv c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv c
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv c
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>K. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. vsv c
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Obj\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have dom_b: "\<D>\<^sub>\<circ> b = J" and dom_c: "\<D>\<^sub>\<circ> c = K"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Obj\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> b = J &&& \<D>\<^sub>\<circ> c = K
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J. \<AA> i\<lparr>Obj\<rparr>)
c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>K. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> b = J &&& \<D>\<^sub>\<circ> c = K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> b = J
\<D>\<^sub>\<circ> c = K

goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
[PROOF STEP]
have disjnt: "\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = 0"
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
[PROOF STEP]
unfolding dom_b dom_c
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>

goal (1 subgoal):
 1. J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>

goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
proof(intro vproductI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 3. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
[PROOF STEP]
by (auto simp: vdomain_vunion dom_b dom_c)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K

goal (2 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
proof(intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
[PROOF STEP]
consider (ib) \<open>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b\<close> | (ic) \<open>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_b dom_c
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<lbrakk>i \<in>\<^sub>\<circ> J \<Longrightarrow> thesis; i \<in>\<^sub>\<circ> K \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 2. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
case ib
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 2. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
with prems disjnt
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b
[PROOF STEP]
have bc_i: "(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
by (auto intro!: vsv_vunion_app_left)
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = b\<lparr>i\<rparr>

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 2. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
from assms(2) ib
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding bc_i dg_prod_components
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J. \<AA> i\<lparr>Obj\<rparr>)
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

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

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
case ic
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
with prems disjnt
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c
[PROOF STEP]
have bc_i: "(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>
[PROOF STEP]
by (auto intro!: vsv_vunion_app_right)
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
from assms(3) ic
[PROOF STATE]
proof (chain)
picking this:
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding bc_i dg_prod_components
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>K. \<AA> i\<lparr>Obj\<rparr>)
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv (b \<union>\<^sub>\<circ> c)
[PROOF STEP]
qed (auto simp: disjnt)
[PROOF STATE]
proof (state)
this:
b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_vunion_Arr_in_Arr:
  assumes "vdisjnt J K"
    and "b \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>J. \<AA> j)\<lparr>Arr\<rparr>"
    and "c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gk\<in>\<^sub>\<circ>K. \<AA> k)\<lparr>Arr\<rparr>"
  shows "b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
proof(intro vproductI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 3. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
interpret b: vsv b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv b
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv b
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. vsv b
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 3. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
interpret c: vsv c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv c
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv c
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>K. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. vsv c
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 3. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
have dom_b: "\<D>\<^sub>\<circ> b = J" and dom_c: "\<D>\<^sub>\<circ> c = K"
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> b = J &&& \<D>\<^sub>\<circ> c = K
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J. \<AA> i\<lparr>Arr\<rparr>)
c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>K. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> b = J &&& \<D>\<^sub>\<circ> c = K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> b = J
\<D>\<^sub>\<circ> c = K

goal (3 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 3. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
have disjnt: "\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = 0"
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
[PROOF STEP]
unfolding dom_b dom_c
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>

goal (3 subgoals):
 1. vsv (b \<union>\<^sub>\<circ> c)
 2. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 3. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from disjnt
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
[PROOF STEP]
show "vsv (b \<union>\<^sub>\<circ> c)"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>

goal (1 subgoal):
 1. vsv (b \<union>\<^sub>\<circ> c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (b \<union>\<^sub>\<circ> c)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 2. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
show dom_bc: "\<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
[PROOF STEP]
unfolding vdomain_vunion dom_b dom_c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. J \<union>\<^sub>\<circ> K = J \<union>\<^sub>\<circ> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
[PROOF STEP]
consider (ib) \<open>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b\<close> | (ic) \<open>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding dom_b dom_c
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<lbrakk>i \<in>\<^sub>\<circ> J \<Longrightarrow> thesis; i \<in>\<^sub>\<circ> K \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
 2. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
case ib
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
 2. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
with prems disjnt
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b
[PROOF STEP]
have bc_i: "(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
by (auto intro!: vsv_vunion_app_left)
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = b\<lparr>i\<rparr>

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
 2. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from assms(2) ib
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> dg_prod J \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding bc_i dg_prod_components
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>J. \<AA> i\<lparr>Arr\<rparr>)
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> b

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

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
case ic
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
with prems disjnt
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c
[PROOF STEP]
have bc_i: "(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
\<D>\<^sub>\<circ> b \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> c = []\<^sub>\<circ>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>
[PROOF STEP]
by (auto intro!: vsv_vunion_app_right)
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c \<Longrightarrow> (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from assms(3) ic
[PROOF STATE]
proof (chain)
picking this:
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> dg_prod K \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding bc_i dg_prod_components
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>K. \<AA> i\<lparr>Arr\<rparr>)
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> c

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts (J \<union>\<^sub>\<circ> K). (b \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_vdiff_vunion_Arr_in_Arr:
  assumes "J \<subseteq>\<^sub>\<circ> I"
    and "b \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gk\<in>\<^sub>\<circ>I -\<^sub>\<circ> J. \<AA> k)\<lparr>Arr\<rparr>"
    and "c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>J. \<AA> j)\<lparr>Arr\<rparr>"
  shows "b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<union>\<^sub>\<circ> c \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by
    (
      vdiff_of_vunion
        rule: dg_prod_vunion_Arr_in_Arr assms: assms(2,3) subset: assms(1)
    )


[STATEMENT]
lemma (in pdigraph) pdg_dg_prod_vunion_is_arr:
  assumes "vdisjnt J K"
    and "J \<subseteq>\<^sub>\<circ> I"
    and "K \<subseteq>\<^sub>\<circ> I"
    and "g : a \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>J. \<AA> j)\<^esub> b"
    and "f : c \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gk\<in>\<^sub>\<circ>K. \<AA> k)\<^esub> d"
  shows "g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>J \<union>\<^sub>\<circ> K. \<AA> i)\<^esub> b \<union>\<^sub>\<circ> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
interpret J\<AA>: pdigraph \<alpha> J \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph \<alpha> J \<AA>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
J \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. pdigraph \<alpha> J \<AA>
[PROOF STEP]
by (simp add: pdg_vsubset_index_pdigraph)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
interpret K\<AA>: pdigraph \<alpha> K \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph \<alpha> K \<AA>
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
K \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. pdigraph \<alpha> K \<AA>
[PROOF STEP]
by (simp add: pdg_vsubset_index_pdigraph)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
interpret JK\<AA>: pdigraph \<alpha> \<open>J \<union>\<^sub>\<circ> K\<close> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph \<alpha> (J \<union>\<^sub>\<circ> K) \<AA>
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
J \<subseteq>\<^sub>\<circ> I
K \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. pdigraph \<alpha> (J \<union>\<^sub>\<circ> K) \<AA>
[PROOF STEP]
by (simp add: pdg_vsubset_index_pdigraph)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
proof(intro JK\<AA>.dg_prod_is_arrI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv (g \<union>\<^sub>\<circ> f)
 2. \<D>\<^sub>\<circ> (g \<union>\<^sub>\<circ> f) = J \<union>\<^sub>\<circ> K
 3. vsv (a \<union>\<^sub>\<circ> c)
 4. \<D>\<^sub>\<circ> (a \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 5. vsv (b \<union>\<^sub>\<circ> d)
 6. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> d) = J \<union>\<^sub>\<circ> K
 7. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
note gD = J\<AA>.dg_prod_is_arrD[OF assms(4)]
      and fD = K\<AA>.dg_prod_is_arrD[OF assms(5)]
[PROOF STATE]
proof (state)
this:
vsv g
\<D>\<^sub>\<circ> g = J
vsv a
\<D>\<^sub>\<circ> a = J
vsv b
\<D>\<^sub>\<circ> b = J
?i \<in>\<^sub>\<circ> J \<Longrightarrow> g\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
vsv f
\<D>\<^sub>\<circ> f = K
vsv c
\<D>\<^sub>\<circ> c = K
vsv d
\<D>\<^sub>\<circ> d = K
?i \<in>\<^sub>\<circ> K \<Longrightarrow> f\<lparr>?i\<rparr> : c\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> d\<lparr>?i\<rparr>

goal (7 subgoals):
 1. vsv (g \<union>\<^sub>\<circ> f)
 2. \<D>\<^sub>\<circ> (g \<union>\<^sub>\<circ> f) = J \<union>\<^sub>\<circ> K
 3. vsv (a \<union>\<^sub>\<circ> c)
 4. \<D>\<^sub>\<circ> (a \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
 5. vsv (b \<union>\<^sub>\<circ> d)
 6. \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> d) = J \<union>\<^sub>\<circ> K
 7. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
from assms(1) gD fD
[PROOF STATE]
proof (chain)
picking this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
vsv g
\<D>\<^sub>\<circ> g = J
vsv a
\<D>\<^sub>\<circ> a = J
vsv b
\<D>\<^sub>\<circ> b = J
?i \<in>\<^sub>\<circ> J \<Longrightarrow> g\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
vsv f
\<D>\<^sub>\<circ> f = K
vsv c
\<D>\<^sub>\<circ> c = K
vsv d
\<D>\<^sub>\<circ> d = K
?i \<in>\<^sub>\<circ> K \<Longrightarrow> f\<lparr>?i\<rparr> : c\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> d\<lparr>?i\<rparr>
[PROOF STEP]
show
      "vsv (g \<union>\<^sub>\<circ> f)"
      "\<D>\<^sub>\<circ> (g \<union>\<^sub>\<circ> f) = J \<union>\<^sub>\<circ> K"
      "vsv (a \<union>\<^sub>\<circ> c)"
      "\<D>\<^sub>\<circ> (a \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K"
      "vsv (b \<union>\<^sub>\<circ> d)"
      "\<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> d) = J \<union>\<^sub>\<circ> K"
[PROOF STATE]
proof (prove)
using this:
J \<inter>\<^sub>\<circ> K = []\<^sub>\<circ>
vsv g
\<D>\<^sub>\<circ> g = J
vsv a
\<D>\<^sub>\<circ> a = J
vsv b
\<D>\<^sub>\<circ> b = J
?i \<in>\<^sub>\<circ> J \<Longrightarrow> g\<lparr>?i\<rparr> : a\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> b\<lparr>?i\<rparr>
vsv f
\<D>\<^sub>\<circ> f = K
vsv c
\<D>\<^sub>\<circ> c = K
vsv d
\<D>\<^sub>\<circ> d = K
?i \<in>\<^sub>\<circ> K \<Longrightarrow> f\<lparr>?i\<rparr> : c\<lparr>?i\<rparr> \<mapsto>\<^bsub>\<AA> ?i\<^esub> d\<lparr>?i\<rparr>

goal (1 subgoal):
 1. (vsv (g \<union>\<^sub>\<circ> f) &&& \<D>\<^sub>\<circ> (g \<union>\<^sub>\<circ> f) = J \<union>\<^sub>\<circ> K &&& vsv (a \<union>\<^sub>\<circ> c)) &&& \<D>\<^sub>\<circ> (a \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K &&& vsv (b \<union>\<^sub>\<circ> d) &&& \<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> d) = J \<union>\<^sub>\<circ> K
[PROOF STEP]
by (auto simp: vdomain_vunion)
[PROOF STATE]
proof (state)
this:
vsv (g \<union>\<^sub>\<circ> f)
\<D>\<^sub>\<circ> (g \<union>\<^sub>\<circ> f) = J \<union>\<^sub>\<circ> K
vsv (a \<union>\<^sub>\<circ> c)
\<D>\<^sub>\<circ> (a \<union>\<^sub>\<circ> c) = J \<union>\<^sub>\<circ> K
vsv (b \<union>\<^sub>\<circ> d)
\<D>\<^sub>\<circ> (b \<union>\<^sub>\<circ> d) = J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K
[PROOF STEP]
consider (iJ) \<open>i \<in>\<^sub>\<circ> J\<close> | (iK) \<open>i \<in>\<^sub>\<circ> K\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K

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

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> J \<union>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<in>\<^sub>\<circ> J \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> K \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<in>\<^sub>\<circ> J \<Longrightarrow> ?thesis; i \<in>\<^sub>\<circ> K \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> J \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
 2. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
case iJ
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> J

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> J \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
 2. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
have gf_i: "(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> = g\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> = g\<lparr>i\<rparr>
[PROOF STEP]
by (simp add: iJ assms(1) gD(1,2) fD(1,2))
[PROOF STATE]
proof (state)
this:
(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> = g\<lparr>i\<rparr>

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> J \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
 2. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
have ac_i: "(a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = a\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = a\<lparr>i\<rparr>
[PROOF STEP]
by (simp add: iJ assms(1) gD(3,4) fD(3,4))
[PROOF STATE]
proof (state)
this:
(a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = a\<lparr>i\<rparr>

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> J \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
 2. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
have bd_i: "(b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr> = b\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr> = b\<lparr>i\<rparr>
[PROOF STEP]
by (simp add: iJ assms(1) gD(5,6) fD(5,6))
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr> = b\<lparr>i\<rparr>

goal (2 subgoals):
 1. i \<in>\<^sub>\<circ> J \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
 2. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
unfolding gf_i ac_i bd_i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g\<lparr>i\<rparr> : a\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> b\<lparr>i\<rparr>
[PROOF STEP]
by (rule gD(7)[OF iJ])
[PROOF STATE]
proof (state)
this:
(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
case iK
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> K

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
have gf_i: "(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> = f\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> = f\<lparr>i\<rparr>
[PROOF STEP]
by (simp add: iK assms(1) gD(1,2) fD(1,2))
[PROOF STATE]
proof (state)
this:
(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> = f\<lparr>i\<rparr>

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
have ac_i: "(a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>
[PROOF STEP]
by (simp add: iK assms(1) gD(3,4) fD(3,4))
[PROOF STATE]
proof (state)
this:
(a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> = c\<lparr>i\<rparr>

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
have bd_i: "(b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr> = d\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr> = d\<lparr>i\<rparr>
[PROOF STEP]
by (simp add: iK assms(1) gD(5,6) fD(5,6))
[PROOF STATE]
proof (state)
this:
(b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr> = d\<lparr>i\<rparr>

goal (1 subgoal):
 1. i \<in>\<^sub>\<circ> K \<Longrightarrow> (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>
[PROOF STEP]
unfolding gf_i ac_i bd_i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<lparr>i\<rparr> : c\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> d\<lparr>i\<rparr>
[PROOF STEP]
by (rule fD(7)[OF iK])
[PROOF STATE]
proof (state)
this:
(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(g \<union>\<^sub>\<circ> f)\<lparr>i\<rparr> : (a \<union>\<^sub>\<circ> c)\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> (b \<union>\<^sub>\<circ> d)\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod (J \<union>\<^sub>\<circ> K) \<AA>\<^esub> b \<union>\<^sub>\<circ> d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph) pdg_dg_prod_vdiff_vunion_is_arr:
  assumes "J \<subseteq>\<^sub>\<circ> I"
    and "g : a \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gk\<in>\<^sub>\<circ>I -\<^sub>\<circ> J. \<AA> k)\<^esub> b"
    and "f : c \<mapsto>\<^bsub>(\<Prod>\<^sub>D\<^sub>Gj\<in>\<^sub>\<circ>J. \<AA> j)\<^esub> d"
  shows "g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<^esub> b \<union>\<^sub>\<circ> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<union>\<^sub>\<circ> f : a \<union>\<^sub>\<circ> c \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b \<union>\<^sub>\<circ> d
[PROOF STEP]
by
    (
      vdiff_of_vunion'
        rule: pdg_dg_prod_vunion_is_arr assms: assms(2,3) subset: assms(1)
    )


[STATEMENT]
lemma dghm_proj_components:
  shows "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>). a\<lparr>i\<rparr>)"
    and "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>). f\<lparr>i\<rparr>)"
    and "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
    and "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) &&& \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>)) &&& \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = dg_prod I \<AA> &&& \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
[PROOF STEP]
unfolding dghm_proj_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, dg_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, dg_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>)) &&& [\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, dg_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = dg_prod I \<AA> &&& [\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, dg_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<AA> i
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma (in pdigraph) dghm_proj_ObjMap_vrange:
  assumes "i \<in>\<^sub>\<circ> I"
  shows "\<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dghm_proj_components
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by (intro vrange_VLambda_vsubset) (clarsimp simp: dg_prod_components)


[STATEMENT]
lemma (in pdigraph) dghm_proj_ArrMap_vrange:
  assumes "i \<in>\<^sub>\<circ> I"
  shows "\<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dghm_proj_components
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
by (intro vrange_VLambda_vsubset) (clarsimp simp: dg_prod_components)