[STATEMENT]
lemma cat_SemiCAT_is_iso_arrI: 
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_iso_arrI is_inverseI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
 2. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 3. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 4. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 5. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
interpret is_iso_semifunctor \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
 2. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 3. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 4. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 5. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show \<FF>: "\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_SemiCAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>

goal (4 subgoals):
 1. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 2. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 3. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 4. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
note iso_thms = is_iso_semifunctor_is_iso_arr[OF assms]
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>

goal (4 subgoals):
 1. ?g : ?b1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?a1
 2. \<FF> : ?a1 \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?b1
 3. ?g \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?a1\<rparr>
 4. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> ?g = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>?b1\<rparr>
[PROOF STEP]
from iso_thms(1)
[PROOF STATE]
proof (chain)
picking this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show inv_\<FF>: "inv_smcf \<FF> : \<BB> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<AA>
[PROOF STEP]
unfolding cat_SemiCAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
 2. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 3. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show "\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding cat_SemiCAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<BB>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 2. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have \<AA>: "semicategory \<alpha> \<AA>" and \<BB>: "semicategory \<alpha> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. semicategory \<alpha> \<AA> &&& semicategory \<alpha> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
semicategory \<alpha> \<AA>
semicategory \<alpha> \<BB>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
 2. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
show "inv_smcf \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>
[PROOF STEP]
unfolding cat_SemiCAT_CId_app[OF \<AA>] cat_SemiCAT_Comp_app[OF inv_\<FF> \<FF>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
[PROOF STEP]
by (rule iso_thms(2))
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<AA>\<rparr>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
show "\<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_smcf \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>
[PROOF STEP]
unfolding cat_SemiCAT_CId_app[OF \<BB>] cat_SemiCAT_Comp_app[OF \<FF> inv_\<FF>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
by (rule iso_thms(3))
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>A\<^bsub>cat_SemiCAT \<alpha>\<^esub> inv_dghm \<FF> = cat_SemiCAT \<alpha>\<lparr>CId\<rparr>\<lparr>\<BB>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed