[STATEMENT]
lemma assoc_coherence:
    shows "LHS = RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LHS = RHS
[PROOF STEP]
proof (intro Span.arr_eqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Span.par LHS RHS
 2. Chn LHS = Chn RHS
[PROOF STEP]
show "Span.par LHS RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Span.par LHS RHS
[PROOF STEP]
using par_LHS_RHS
[PROOF STATE]
proof (prove)
using this:
Span.par LHS RHS

goal (1 subgoal):
 1. Span.par LHS RHS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Span.par LHS RHS

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
show "Chn LHS = Chn RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using Chn_LHS_eq
[PROOF STATE]
proof (prove)
using this:
Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> =
                \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh isomorphic_reflexive HHfgh_HfHgh.is_map THfgh_HHfgh.is_map
                  TTfgh_THfgh.is_map left_adjoints_compose
                  Maps.comp_CLS
                    [of THfgh_HHfgh.chine TTfgh_THfgh.chine "THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"]
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> ?f \<cong> ?f
is_left_adjoint HHfgh_HfHgh.chine
is_left_adjoint THfgh_HHfgh.chine
is_left_adjoint TTfgh_THfgh.chine
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')
\<lbrakk>is_left_adjoint THfgh_HHfgh.chine; is_left_adjoint TTfgh_THfgh.chine; THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> =
                \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
have "ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
using fg gh HHfgh_HfHgh.is_map THfgh_HHfgh.is_map TTfgh_THfgh.is_map
                      left_adjoint_is_ide left_adjoints_compose
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
is_left_adjoint HHfgh_HfHgh.chine
is_left_adjoint THfgh_HHfgh.chine
is_left_adjoint TTfgh_THfgh.chine
is_left_adjoint ?f \<Longrightarrow> ide ?f
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')

goal (1 subgoal):
 1. ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
have "src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
using fg gh HHfgh_HfHgh.chine_in_hom \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<guillemotleft>HHfgh_HfHgh.chine : src (tab\<^sub>0 (local.dom (\<alpha> (f, g, h)))) \<rightarrow> src (tab\<^sub>0 (cod (\<alpha> (f, g, h))))\<guillemotright>
\<guillemotleft>HHfgh_HfHgh.chine : HHfgh_HfHgh.chine \<rightarrow> HHfgh_HfHgh.chine\<guillemotright>
\<alpha> ?\<mu>\<nu>\<tau> \<equiv> \<a>[fst ?\<mu>\<nu>\<tau>, fst (snd ?\<mu>\<nu>\<tau>), snd (snd ?\<mu>\<nu>\<tau>)]

goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh isomorphic_reflexive HHfgh_HfHgh.is_map THfgh_HHfgh.is_map
                    TTfgh_THfgh.is_map left_adjoints_compose
                    Maps.comp_CLS
                      [of HHfgh_HfHgh.chine "THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"
                          "HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"]
[PROOF STATE]
proof (prove)
using this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> ?f \<cong> ?f
is_left_adjoint HHfgh_HfHgh.chine
is_left_adjoint THfgh_HHfgh.chine
is_left_adjoint TTfgh_THfgh.chine
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')
\<lbrakk>is_left_adjoint HHfgh_HfHgh.chine; is_left_adjoint (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine); HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret A: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> TTfgh.tab \<open>tab\<^sub>0 h \<star> TTfgh.p\<^sub>0\<close> \<open>(tab\<^sub>1 f \<star> Tfg.p\<^sub>1) \<star> TTfgh.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> TfTgh.tab \<open>(tab\<^sub>0 h \<star> Tgh.p\<^sub>0) \<star> TfTgh.p\<^sub>0\<close> \<open>tab\<^sub>1 f \<star> TfTgh.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> TfHgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 (g \<star> h) \<star> TfHgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 f \<star> TfHgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>\<a>[f, g, h]\<close> \<open>f \<star> g \<star> h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfHgh.\<rho>\<sigma>.tab (tab\<^sub>0 (g \<star> h) \<star> TfHgh.p\<^sub>0) (tab\<^sub>1 f \<star> TfHgh.p\<^sub>1) \<a>[f, g, h] (f \<star> g \<star> h)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret B: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> TTfgh.tab \<open>tab\<^sub>0 h \<star> TTfgh.p\<^sub>0\<close> \<open>(tab\<^sub>1 f \<star> Tfg.p\<^sub>1) \<star> TTfgh.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> TfHgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 (g \<star> h) \<star> TfHgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 f \<star> TfHgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> HfHgh.tab \<open>tab\<^sub>0 (f \<star> g \<star> h)\<close> \<open>tab\<^sub>1 (f \<star> g \<star> h)\<close>
                         \<open>\<a>[f, g, h]\<close> \<open>f \<star> g \<star> h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfHgh.\<rho>\<sigma>.tab (tab\<^sub>0 (g \<star> h) \<star> TfHgh.p\<^sub>0) (tab\<^sub>1 f \<star> TfHgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) \<a>[f, g, h] (f \<star> g \<star> h)
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfHgh.\<rho>\<sigma>.tab (tab\<^sub>0 (g \<star> h) \<star> TfHgh.p\<^sub>0) (tab\<^sub>1 f \<star> TfHgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) \<a>[f, g, h] (f \<star> g \<star> h)
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret C: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> THfgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 h \<star> THfgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 (f \<star> g) \<star> THfgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>(f \<star> g) \<star> h\<close> HHfgh.tab \<open>tab\<^sub>0 ((f \<star> g) \<star> h)\<close> \<open>tab\<^sub>1 ((f \<star> g) \<star> h)\<close>
                         \<open>f \<star> g \<star> h\<close> HfHgh.tab \<open>tab\<^sub>0 (f \<star> g \<star> h)\<close> \<open>tab\<^sub>1 (f \<star> g \<star> h)\<close>
                         \<open>(f \<star> g) \<star> h\<close> \<open>\<a>[f, g, h]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) ((f \<star> g) \<star> h) HHfgh.tab (tab\<^sub>0 ((f \<star> g) \<star> h)) (tab\<^sub>1 ((f \<star> g) \<star> h)) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) ((f \<star> g) \<star> h) HHfgh.tab (tab\<^sub>0 ((f \<star> g) \<star> h)) (tab\<^sub>1 ((f \<star> g) \<star> h)) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret D: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> TTfgh.tab \<open>tab\<^sub>0 h \<star> TTfgh.p\<^sub>0\<close> \<open>(tab\<^sub>1 f \<star> Tfg.p\<^sub>1) \<star> TTfgh.p\<^sub>1\<close>
                         \<open>(f \<star> g) \<star> h\<close> THfgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 h \<star> THfgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 (f \<star> g) \<star> THfgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> HfHgh.tab \<open>tab\<^sub>0 (f \<star> g \<star> h)\<close> \<open>tab\<^sub>1 (f \<star> g \<star> h)\<close>
                         \<open>(f \<star> g) \<star> h\<close> \<open>\<a>[f, g, h]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
using D.chine_char
[PROOF STATE]
proof (prove)
using this:
D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> C.chine \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
using fg gh comp_arr_dom isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; local.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot> ?a = ?f
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
using C.chine_char hcomp_isomorphic_ide
[PROOF STATE]
proof (prove)
using this:
C.chine \<cong> C.\<pi>.chine \<star> THfgh_HHfgh.chine
\<lbrakk>?f \<cong> ?g; ide ?h; src ?f = trg ?h\<rbrakk> \<Longrightarrow> ?f \<star> ?h \<cong> ?g \<star> ?h

goal (1 subgoal):
 1. C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
have "C.\<pi>.chine = HHfgh_HfHgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.\<pi>.chine = HHfgh_HfHgh.chine
[PROOF STEP]
using fg gh comp_arr_dom comp_cod_arr \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; local.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot> ?a = ?f
\<lbrakk>arr ?f; cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot> ?f = ?f
\<alpha> ?\<mu>\<nu>\<tau> \<equiv> \<a>[fst ?\<mu>\<nu>\<tau>, fst (snd ?\<mu>\<nu>\<tau>), snd (snd ?\<mu>\<nu>\<tau>)]

goal (1 subgoal):
 1. C.\<pi>.chine = HHfgh_HfHgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.\<pi>.chine = HHfgh_HfHgh.chine

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
hence "isomorphic C.\<pi>.chine HHfgh_HfHgh.chine"
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine = HHfgh_HfHgh.chine

goal (1 subgoal):
 1. C.\<pi>.chine \<cong> HHfgh_HfHgh.chine
[PROOF STEP]
using isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine = HHfgh_HfHgh.chine
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. C.\<pi>.chine \<cong> HHfgh_HfHgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.\<pi>.chine \<cong> HHfgh_HfHgh.chine

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine \<cong> HHfgh_HfHgh.chine

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
using hcomp_isomorphic_ide
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine \<cong> HHfgh_HfHgh.chine
\<lbrakk>?f \<cong> ?g; ide ?h; src ?f = trg ?h\<rbrakk> \<Longrightarrow> ?f \<star> ?h \<cong> ?g \<star> ?h

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
have "ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
have "src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and>
                             src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
[PROOF STEP]
using fg gh HHfgh_HfHgh.chine_in_hom THfgh_HHfgh.chine_in_hom 
                      TTfgh_THfgh.chine_in_hom \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<guillemotleft>HHfgh_HfHgh.chine : src (tab\<^sub>0 (local.dom (\<alpha> (f, g, h)))) \<rightarrow> src (tab\<^sub>0 (cod (\<alpha> (f, g, h))))\<guillemotright>
\<guillemotleft>HHfgh_HfHgh.chine : HHfgh_HfHgh.chine \<rightarrow> HHfgh_HfHgh.chine\<guillemotright>
\<guillemotleft>THfgh_HHfgh.chine : src (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) \<rightarrow> src (tab\<^sub>0 ((f \<star> g) \<star> h))\<guillemotright>
\<guillemotleft>THfgh_HHfgh.chine : THfgh_HHfgh.chine \<rightarrow> THfgh_HHfgh.chine\<guillemotright>
\<guillemotleft>TTfgh_THfgh.chine : src (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<rightarrow> src (tab\<^sub>0 h \<star> THfgh.p\<^sub>0)\<guillemotright>
\<guillemotleft>TTfgh_THfgh.chine : TTfgh_THfgh.chine \<rightarrow> TTfgh_THfgh.chine\<guillemotright>
\<alpha> ?\<mu>\<nu>\<tau> \<equiv> \<a>[fst ?\<mu>\<nu>\<tau>, fst (snd ?\<mu>\<nu>\<tau>), snd (snd ?\<mu>\<nu>\<tau>)]

goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
using fg gh iso_assoc isomorphic_def
                       assoc_in_hom [of HHfgh_HfHgh.chine THfgh_HHfgh.chine TTfgh_THfgh.chine]
[PROOF STATE]
proof (prove)
using this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
src f = trg g
src g = trg h
\<lbrakk>ide ?f; ide ?g; ide ?h; src ?f = trg ?g; src ?g = trg ?h\<rbrakk> \<Longrightarrow> local.iso \<a>[?f, ?g, ?h]
(?a \<cong> ?a') = (\<exists>f. \<guillemotleft>f : ?a \<rightarrow> ?a'\<guillemotright> \<and> local.iso f)
\<lbrakk>ide HHfgh_HfHgh.chine; ide THfgh_HHfgh.chine; ide TTfgh_THfgh.chine; src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine; src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<guillemotleft>\<a>[HHfgh_HfHgh.chine, THfgh_HHfgh.chine, TTfgh_THfgh.chine] : src TTfgh_THfgh.chine \<rightarrow> trg HHfgh_HfHgh.chine\<guillemotright>
\<lbrakk>ide HHfgh_HfHgh.chine; ide THfgh_HHfgh.chine; ide TTfgh_THfgh.chine; src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine; src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<guillemotleft>\<a>[HHfgh_HfHgh.chine, THfgh_HHfgh.chine, TTfgh_THfgh.chine] : (local.dom HHfgh_HfHgh.chine \<star> local.dom THfgh_HHfgh.chine) \<star> local.dom TTfgh_THfgh.chine \<rightarrow> cod HHfgh_HfHgh.chine \<star> cod THfgh_HHfgh.chine \<star> cod TTfgh_THfgh.chine\<guillemotright>

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
D.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
D.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
using isomorphic_symmetric
[PROOF STATE]
proof (prove)
using this:
D.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
?f \<cong> ?g \<Longrightarrow> ?g \<cong> ?f

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "... \<cong> B.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
have "D.chine = B.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.chine = B.chine
[PROOF STEP]
using fg gh comp_arr_dom comp_cod_arr
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; local.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot> ?a = ?f
\<lbrakk>arr ?f; cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot> ?f = ?f

goal (1 subgoal):
 1. D.chine = B.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.chine = B.chine

goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
D.chine = B.chine

goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
using isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
D.chine = B.chine
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.chine \<cong> B.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
D.chine \<cong> B.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D.chine \<cong> B.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "... \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine
[PROOF STEP]
using B.chine_char
[PROOF STATE]
proof (prove)
using this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "... \<cong> TfHgh_HfHgh.chine \<star> A.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine
[PROOF STEP]
using fg gh comp_cod_arr isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot> ?f = ?f
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "... \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> A.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
using A.chine_char hcomp_ide_isomorphic
[PROOF STATE]
proof (prove)
using this:
A.chine \<cong> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
\<lbrakk>ide ?f; ?g \<cong> ?h; src ?f = trg ?g\<rbrakk> \<Longrightarrow> ?f \<star> ?g \<cong> ?f \<star> ?h

goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> A.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TfHgh_HfHgh.chine \<star> A.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong>
                        TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
[PROOF STATE]
proof (prove)
using this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh Maps.CLS_eqI isomorphic_implies_hpar(1)
[PROOF STATE]
proof (prove)
using this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> (\<lbrakk>\<lbrakk>?f\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>?g\<rbrakk>\<rbrakk>) = (?f \<cong> ?g)
?f \<cong> ?f' \<Longrightarrow> ide ?f

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh isomorphic_reflexive TfTgh_TfHgh.is_map TfHgh_HfHgh.is_map TTfgh_TfTgh.is_map
                left_adjoints_compose
                Maps.comp_CLS
                  [of TfTgh_TfHgh.chine TTfgh_TfTgh.chine "TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"]
                Maps.comp_CLS
                  [of TfHgh_HfHgh.chine "TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
                      "TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"]
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> ?f \<cong> ?f
is_left_adjoint TfTgh_TfHgh.chine
is_left_adjoint TfHgh_HfHgh.chine
is_left_adjoint TTfgh_TfTgh.chine
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')
\<lbrakk>is_left_adjoint TfTgh_TfHgh.chine; is_left_adjoint TTfgh_TfTgh.chine; TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine \<cong> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
\<lbrakk>is_left_adjoint TfHgh_HfHgh.chine; is_left_adjoint (TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine); TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = Chn RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = Chn RHS
[PROOF STEP]
using Chn_RHS_eq CLS_chine tuple_ABC_eq_ABC'(2)
[PROOF STATE]
proof (prove)
using this:
Chn RHS = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> tuple_ABC'
\<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = tuple_ABC
tuple_ABC = tuple_ABC'

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = Chn RHS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = Chn RHS

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Chn LHS = Chn RHS
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Chn LHS = Chn RHS

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Chn LHS = Chn RHS

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Chn LHS = Chn RHS

goal:
No subgoals!
[PROOF STEP]
qed