[STATEMENT]
lemma (in is_cat_limit) is_cat_colimit_op'[cat_op_intros]:
  assumes "\<FF>' = op_cf \<FF>" and "\<JJ>' = op_cat \<JJ>" and "\<CC>' = op_cat \<CC>"
  shows "op_ntcf u : \<FF>' >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : \<JJ>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf u : \<FF>' >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : \<JJ>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf u : op_cf \<FF> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : op_cat \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>
[PROOF STEP]
by (rule is_cat_colimit_op)