[STATEMENT]
lemma iso_in_homI [intro]:
    assumes "\<guillemotleft>f : a \<rightarrow> b\<guillemotright>" and "iso f"
    shows "\<guillemotleft>f : a \<cong> b\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : a \<cong> b\<guillemotright>
[PROOF STEP]
using assms iso_in_hom_def
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f : a \<rightarrow> b\<guillemotright>
local.iso f
\<guillemotleft>?f : ?a \<cong> ?b\<guillemotright> \<equiv> \<guillemotleft>?f : ?a \<rightarrow> ?b\<guillemotright> \<and> local.iso ?f

goal (1 subgoal):
 1. \<guillemotleft>f : a \<cong> b\<guillemotright>
[PROOF STEP]
by simp