proposition: Lemma is_colimit_cocone_compose : forall a u, is_colimit a -> cocone_composable u a -> invertible (cocone_target a) u -> is_colimit (cocone_compose u a).
proof: Proof. ir. assert (lem1: is_cocone (cocone_compose u a)). app is_cocone_cocone_compose. uhg; ee. uhg; ee. am. ir. assert (mor (cocone_target a) u0). uh H2; ee. rwi cocone_target_cocone_compose H5. am. assert (mor (cocone_target a) v). uh H3; ee. rwi cocone_target_cocone_compose H6; am. assert (target u = source u0). sy. uh H2; ee. rwi vertex_cocone_compose H8; am. assert (target u = source v). sy. uh H3; ee. rwi vertex_cocone_compose H9; am. assert (mor (cocone_target a) u). uh H0; ee. am. rwi cocone_compose_cocone_compose H4. rwi cocone_compose_cocone_compose H4. uh H; ee. uh H; ee. assert (comp (cocone_target a) u0 u = comp (cocone_target a) v u). ap H11. uhg; ee. am. rww mor_comp. wrr H7. rww source_comp. uh H0; ee; am. sy; am. uhg; ee. am. rww mor_comp. sy; am. rw source_comp. uh H0; ee; am. lu. lu. sy; am. am. transitivity (comp (cocone_target a) (comp (cocone_target a) u0 u) (inverse (cocone_target a) u)). rw assoc. rw right_inverse. rw right_id. tv. rww ob_target. am. sy; am. tv. am. am. am. ap mor_inverse. am. sy; am. rw target_inverse. tv. am. tv. rw H12. rw assoc. rw right_inverse. rw right_id. tv. rww ob_target. am. sy; am. tv. am. am. am. app mor_inverse. sy; am. rww target_inverse. tv. am. app show_composable. sy; am. am. app show_composable. sy; am. assert (lema: source u = vertex a). lu. uhg; ee. am. ir. assert (lem0 : cosocle b = cosocle a). rwi cosocle_cocone_compose H3. am. assert (lem2: composable (cocone_target a) (colimit_to_cocone a b) (inverse (cocone_target a) u)). ap show_composable. app mor_colimit_to_cocone. app mor_inverse. rw target_inverse. rww source_colimit_to_cocone. sy; am. am. assert (is_cocone a). uh H; ee. uh H; ee; am. sh (comp (cocone_target a) (colimit_to_cocone a b) (inverse (cocone_target a) u)). ee. uhg; ee. am. rw cocone_target_cocone_compose. rww mor_comp. ap mor_colimit_to_cocone. am. am. am. tv. app mor_inverse. rww target_inverse. rww source_colimit_to_cocone. sy; am. rww source_comp. rww source_inverse. rww vertex_cocone_compose. app mor_colimit_to_cocone. app mor_inverse. rww source_colimit_to_cocone. rww target_inverse. sy; am. assert (cocone_target a = cocone_target (cocone_compose u a)). rww cocone_target_cocone_compose. assert (mor (cocone_target a) u). uh H0; ee; am. rw cocone_compose_cocone_compose. rw assoc. rww left_inverse. rw right_id. rw cocone_compose_colimit_to_cocone. tv. am. am. am. rww ob_source. app mor_colimit_to_cocone. rw source_colimit_to_cocone. sy; am. am. am. am. tv. app mor_colimit_to_cocone. app mor_inverse. am. rww target_inverse. rww source_colimit_to_cocone. sy; am. rww source_inverse. tv. am. ap show_composable. rww mor_comp. app mor_colimit_to_cocone. app mor_inverse. rww target_inverse. rww source_colimit_to_cocone. sy; am. am. rww source_comp. rww source_inverse. app mor_colimit_to_cocone. app mor_inverse. rww target_inverse. rww source_colimit_to_cocone. sy; am. Qed.
imports: Arith limits