[STATEMENT]
lemma is_left_adjoint_functor:
    shows "left_adjoint_functor C D F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_adjoint_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. D.ide y \<Longrightarrow> \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. D.ide y \<Longrightarrow> \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
assume y: "D.ide y"
[PROOF STATE]
proof (state)
this:
D.ide y

goal (1 subgoal):
 1. \<And>y. D.ide y \<Longrightarrow> \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
let ?x = "SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. D.ide y \<Longrightarrow> \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
let ?e = "SOME e. D.iso e \<and> \<guillemotleft>e : F ?x \<rightarrow>\<^sub>D y\<guillemotright>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. D.ide y \<Longrightarrow> \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
have "\<exists>x e. D.iso e \<and> terminal_arrow_from_functor C D F x y e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
have "\<exists>x. D.iso ?e \<and> terminal_arrow_from_functor C D F x y ?e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
have x: "C.ide ?x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F ?x \<rightarrow>\<^sub>D y\<guillemotright>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
using y essentially_surjective
                  someI_ex [of "\<lambda>x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)"]
[PROOF STATE]
proof (prove)
using this:
D.ide y
D.ide ?b \<Longrightarrow> \<exists>a. C.ide a \<and> D.isomorphic (F a) ?b
\<exists>x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>) \<Longrightarrow> C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal (1 subgoal):
 1. C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
hence e: "D.iso ?e \<and> \<guillemotleft>?e : F ?x \<rightarrow>\<^sub>D y\<guillemotright>"
[PROOF STATE]
proof (prove)
using this:
C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal (1 subgoal):
 1. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
[PROOF STEP]
using someI_ex [of "\<lambda>e. D.iso e \<and> \<guillemotleft>e : F ?x \<rightarrow>\<^sub>D y\<guillemotright>"]
[PROOF STATE]
proof (prove)
using this:
C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
\<exists>x. D.iso x \<and> \<guillemotleft>x : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> \<Longrightarrow> D.iso (SOME x. D.iso x \<and> \<guillemotleft>x : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME x. D.iso x \<and> \<guillemotleft>x : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>

goal (1 subgoal):
 1. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>

goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
interpret arrow_from_functor C D F ?x y ?e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
using x e
[PROOF STATE]
proof (prove)
using this:
C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>

goal (1 subgoal):
 1. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
by (unfold_locales, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
interpret terminal_arrow_from_functor C D F ?x y ?e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x' f. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f \<Longrightarrow> \<exists>!g. is_coext x' f g
[PROOF STEP]
fix x' f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x' f. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f \<Longrightarrow> \<exists>!g. is_coext x' f g
[PROOF STEP]
assume 1: "arrow_from_functor C D F x' y f"
[PROOF STATE]
proof (state)
this:
arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f

goal (1 subgoal):
 1. \<And>x' f. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f \<Longrightarrow> \<exists>!g. is_coext x' f g
[PROOF STEP]
interpret f: arrow_from_functor C D F x' y f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f

goal (1 subgoal):
 1. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x' f. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f \<Longrightarrow> \<exists>!g. is_coext x' f g
[PROOF STEP]
have f: "\<guillemotleft>f: F x' \<rightarrow>\<^sub>D y\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>
[PROOF STEP]
by (meson f.arrow)
[PROOF STATE]
proof (state)
this:
\<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>

goal (1 subgoal):
 1. \<And>x' f. arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x' y f \<Longrightarrow> \<exists>!g. is_coext x' f g
[PROOF STEP]
show "\<exists>!g. is_coext x' f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!g. is_coext x' f g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_coext x' f ?a
 2. \<And>g. is_coext x' f g \<Longrightarrow> g = ?a
[PROOF STEP]
let ?g = "SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C ?x\<guillemotright> \<and> F g = D.inv ?e \<cdot>\<^sub>D f"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_coext x' f ?a
 2. \<And>g. is_coext x' f g \<Longrightarrow> g = ?a
[PROOF STEP]
have g: "\<guillemotleft>?g : x' \<rightarrow>\<^sub>C ?x\<guillemotright> \<and> F ?g = D.inv ?e \<cdot>\<^sub>D f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f
[PROOF STEP]
using f e x f.arrow is_full D.comp_in_homI D.inv_in_hom
                      someI_ex [of "\<lambda>g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C ?x\<guillemotright> \<and> F g = D.inv ?e \<cdot>\<^sub>D f"]
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
C.ide (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
C.ide x' \<and> \<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>
\<lbrakk>C.ide ?a; C.ide ?a'; \<guillemotleft>?g : F ?a' \<rightarrow>\<^sub>D F ?a\<guillemotright>\<rbrakk> \<Longrightarrow> \<exists>f. \<guillemotleft>f : ?a' \<rightarrow>\<^sub>C ?a\<guillemotright> \<and> F f = ?g
\<lbrakk>\<guillemotleft>?f : ?a \<rightarrow>\<^sub>D ?b\<guillemotright>; \<guillemotleft>?g : ?b \<rightarrow>\<^sub>D ?c\<guillemotright>\<rbrakk> \<Longrightarrow> \<guillemotleft>?g \<cdot>\<^sub>D ?f : ?a \<rightarrow>\<^sub>D ?c\<guillemotright>
\<lbrakk>D.iso ?f; \<guillemotleft>?f : ?a \<rightarrow>\<^sub>D ?b\<guillemotright>\<rbrakk> \<Longrightarrow> \<guillemotleft>D.inv ?f : ?b \<rightarrow>\<^sub>D ?a\<guillemotright>
\<exists>x. \<guillemotleft>x : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F x = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f \<Longrightarrow> \<guillemotleft>SOME x. \<guillemotleft>x : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F x = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F (SOME x. \<guillemotleft>x : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F x = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f

goal (2 subgoals):
 1. is_coext x' f ?a
 2. \<And>g. is_coext x' f g \<Longrightarrow> g = ?a
[PROOF STEP]
show 1: "is_coext x' f ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
have "\<guillemotleft>?g : x' \<rightarrow>\<^sub>C ?x\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>

goal (1 subgoal):
 1. is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>

goal (1 subgoal):
 1. is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
have "?e \<cdot>\<^sub>D F ?g = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
have "?e \<cdot>\<^sub>D F ?g = ?e \<cdot>\<^sub>D D.inv ?e \<cdot>\<^sub>D f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
have "... = (?e \<cdot>\<^sub>D D.inv ?e) \<cdot>\<^sub>D f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f = ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f
[PROOF STEP]
using e f D.inv_in_hom
[PROOF STATE]
proof (prove)
using this:
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
\<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>
\<lbrakk>D.iso ?f; \<guillemotleft>?f : ?a \<rightarrow>\<^sub>D ?b\<guillemotright>\<rbrakk> \<Longrightarrow> \<guillemotleft>D.inv ?f : ?b \<rightarrow>\<^sub>D ?a\<guillemotright>

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f = ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f
[PROOF STEP]
by (metis D.comp_assoc)
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f = ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f = ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
have "... = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f
[PROOF STEP]
have "?e \<cdot>\<^sub>D D.inv ?e = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) = y
[PROOF STEP]
using e D.comp_arr_inv D.inv_is_inverse
[PROOF STATE]
proof (prove)
using this:
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
D.inverse_arrows ?f ?g \<Longrightarrow> ?f \<cdot>\<^sub>D ?g = D.dom ?g
D.iso ?f \<Longrightarrow> D.inverse_arrows ?f (D.inv ?f)

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) = y

goal (1 subgoal):
 1. ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) = y

goal (1 subgoal):
 1. ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f
[PROOF STEP]
using f D.comp_cod_arr
[PROOF STATE]
proof (prove)
using this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) = y
\<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>
\<lbrakk>D.arr ?f; D.cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot>\<^sub>D ?f = ?f

goal (1 subgoal):
 1. ((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)) \<cdot>\<^sub>D f = f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal (1 subgoal):
 1. (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal (1 subgoal):
 1. is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal (1 subgoal):
 1. is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
unfolding is_coext_def
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright>
(SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> f = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal (1 subgoal):
 1. \<And>g. is_coext x' f g \<Longrightarrow> g = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
show "\<And>g'. is_coext x' f g' \<Longrightarrow> g' = ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
fix g'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
assume g': "is_coext x' f g'"
[PROOF STATE]
proof (state)
this:
is_coext x' f g'

goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
have 2: "\<guillemotleft>g' : x' \<rightarrow>\<^sub>C ?x\<guillemotright> \<and> ?e \<cdot>\<^sub>D F g' = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>g' : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F g' = f
[PROOF STEP]
using g' is_coext_def
[PROOF STATE]
proof (prove)
using this:
is_coext x' f g'
is_coext ?x' ?f ?g \<equiv> \<guillemotleft>?g : ?x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> ?f = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F ?g

goal (1 subgoal):
 1. \<guillemotleft>g' : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F g' = f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<guillemotleft>g' : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F g' = f

goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
have 3: "\<guillemotleft>?g : x' \<rightarrow>\<^sub>C ?x\<guillemotright> \<and> ?e \<cdot>\<^sub>D F ?g = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
using 1 is_coext_def
[PROOF STATE]
proof (prove)
using this:
is_coext x' f (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
is_coext ?x' ?f ?g \<equiv> \<guillemotleft>?g : ?x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> ?f = (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F ?g

goal (1 subgoal):
 1. \<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
have "F g' = F ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
using e f 2 3 D.iso_is_section D.section_is_mono D.monoE D.arrI
[PROOF STATE]
proof (prove)
using this:
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
\<guillemotleft>f : F x' \<rightarrow>\<^sub>D y\<guillemotright>
\<guillemotleft>g' : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F g' = f
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f
D.iso ?f \<Longrightarrow> D.section ?f
D.section ?g \<Longrightarrow> D.mono ?g
\<lbrakk>D.mono ?g; D.seq ?g ?f; D.seq ?g ?f'; ?g \<cdot>\<^sub>D ?f = ?g \<cdot>\<^sub>D ?f'\<rbrakk> \<Longrightarrow> ?f' = ?f
\<guillemotleft>?f : ?a \<rightarrow>\<^sub>D ?b\<guillemotright> \<Longrightarrow> D.arr ?f

goal (1 subgoal):
 1. F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
by (metis (no_types, lifting) D.arrI)
[PROOF STATE]
proof (state)
this:
F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
have "C.par g' ?g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>g' : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F g' = f
\<guillemotleft>SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f) = f

goal (1 subgoal):
 1. C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal (1 subgoal):
 1. \<And>g'. is_coext x' f g' \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
show "g' = ?g"
[PROOF STATE]
proof (prove)
using this:
F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal (1 subgoal):
 1. g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
using is_faithful [of g' ?g]
[PROOF STATE]
proof (prove)
using this:
F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
\<lbrakk>C.par g' (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f); F g' = F (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)\<rbrakk> \<Longrightarrow> g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal (1 subgoal):
 1. g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_coext x' f ?g' \<Longrightarrow> ?g' = (SOME g. \<guillemotleft>g : x' \<rightarrow>\<^sub>C SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)\<guillemotright> \<and> F g = D.inv (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<cdot>\<^sub>D f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!g. is_coext x' f g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
using e terminal_arrow_from_functor_axioms
[PROOF STATE]
proof (prove)
using this:
D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> \<guillemotleft>SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright> : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>
terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal (1 subgoal):
 1. \<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal (1 subgoal):
 1. \<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>x. D.iso (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>) \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y (SOME e. D.iso e \<and> \<guillemotleft>e : F (SOME x. C.ide x \<and> (\<exists>e. D.iso e \<and> \<guillemotleft>e : F x \<rightarrow>\<^sub>D y\<guillemotright>)) \<rightarrow>\<^sub>D y\<guillemotright>)

goal (1 subgoal):
 1. \<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e

goal (1 subgoal):
 1. \<And>y. D.ide y \<Longrightarrow> \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
thus "\<exists>x e. terminal_arrow_from_functor C D F x y e"
[PROOF STATE]
proof (prove)
using this:
\<exists>x e. D.iso e \<and> terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e

goal (1 subgoal):
 1. \<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x e. terminal_arrow_from_functor (\<cdot>\<^sub>C) (\<cdot>\<^sub>D) F x y e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ext_def: "f\<equiv>g \<Longrightarrow> f x \<equiv> g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<equiv> g \<Longrightarrow> f x \<equiv> g x
[PROOF STEP]
by auto


[STATEMENT]
lemma (in Module) sc_un:" m \<in> carrier M \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> carrier M \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s m = m
[PROOF STEP]
apply (simp add:sprod_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done