[STATEMENT]
lemma (in category) cat_is_iso_arr_if_ntcf_Hom_snd_is_iso_ntcf:
  assumes "f : s \<mapsto>\<^bsub>\<CC>\<^esub> r"
    and "Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-) :
      Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>"
  shows "f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
f : s \<mapsto>\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
have r: "r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>" and s: "s \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : s \<mapsto>\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> &&& s \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
s \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
note unique = cat_ntcf_Hom_snd_is_iso_ntcf_Hom_snd_unique[OF r s assms(2)]
[PROOF STATE]
proof (state)
this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-) = Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr>,-)
\<lbrakk>?f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>; Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-) = Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(?f,-)\<rbrakk> \<Longrightarrow> ?f = Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr>

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
from unique(1)
[PROOF STATE]
proof (chain)
picking this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
have Ym_Hf: 
    "Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^bsub>\<CC>\<^esub> r"
[PROOF STATE]
proof (prove)
using this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
from unique(1)
[PROOF STATE]
proof (chain)
picking this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Yoneda_map \<alpha> Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(s,-) r\<lparr>Hom\<^sub>A\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(f,-)\<rparr> : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
unfolding cat_ntcf_Hom_snd_inj[OF unique(2) assms(1) Ym_Hf, symmetric]
[PROOF STATE]
proof (prove)
using this:
f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal (1 subgoal):
 1. f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f : s \<mapsto>\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<CC>\<^esub> r

goal:
No subgoals!
[PROOF STEP]
qed