[STATEMENT]
lemma reflects_iso:
    assumes "\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>" and "B.iso (F f)"
    shows "A.iso f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)
[PROOF STEP]
obtain g' where g': "B.inverse_arrows (F f) g'"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)

goal (1 subgoal):
 1. (\<And>g'. B.inverse_arrows (F f) g' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B.inverse_arrows (F f) g'

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
have 1: "\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
[PROOF STEP]
using assms g'
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)
B.inverse_arrows (F f) g'

goal (1 subgoal):
 1. \<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
[PROOF STEP]
by (metis B.inv_in_hom B.inverse_unique preserves_hom)
[PROOF STATE]
proof (state)
this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
[PROOF STEP]
obtain g where g: "\<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g'"
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>

goal (1 subgoal):
 1. (\<And>g. \<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) is_full
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
\<lbrakk>A.ide ?a; A.ide ?a'; \<guillemotleft>?g : F ?a' \<rightarrow>\<^sub>B F ?a\<guillemotright>\<rbrakk> \<Longrightarrow> \<exists>f. \<guillemotleft>f : ?a' \<rightarrow>\<^sub>A ?a\<guillemotright> \<and> F f = ?g

goal (1 subgoal):
 1. (\<And>g. \<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis A.arrI A.ide_cod A.ide_dom A.in_homE)
[PROOF STATE]
proof (state)
this:
\<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g'

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
have "A.inverse_arrows f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A.inverse_arrows f g
[PROOF STEP]
using assms 1 g g' A.inverse_arrowsI
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a' \<rightarrow>\<^sub>A a\<guillemotright>
B.iso (F f)
\<guillemotleft>g' : F a \<rightarrow>\<^sub>B F a'\<guillemotright>
\<guillemotleft>g : a \<rightarrow>\<^sub>A a'\<guillemotright> \<and> F g = g'
B.inverse_arrows (F f) g'
\<lbrakk>A.ide (A ?g ?f); A.ide (A ?f ?g)\<rbrakk> \<Longrightarrow> A.inverse_arrows ?f ?g

goal (1 subgoal):
 1. A.inverse_arrows f g
[PROOF STEP]
by (metis A.arr_iff_in_hom A.dom_comp A.in_homE A.seqI' B.inverse_arrowsE
            A.cod_comp locally_reflects_ide preserves_comp)
[PROOF STATE]
proof (state)
this:
A.inverse_arrows f g

goal (1 subgoal):
 1. A.iso f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A.inverse_arrows f g

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

goal:
No subgoals!
[PROOF STEP]
qed