proposition: Lemma are_finverse_preserves_limits : forall a f g, is_limit a -> are_finverse f g -> source f = cone_target a -> is_limit (cone_pushdown f a).
proof: Proof. ir. uh H0; ee. assert (is_cone a). uh H; ee. uh H; ee. am. assert (is_cone (cone_pushdown f a)). ap is_cone_cone_pushdown. am. am. am. assert (lem1 : forall x, ob (source f) x -> fob g (fob f x) = x). ir. wr fob_fcompose. rw H6. rw fob_fidentity. tv. am. am. am. am. am. assert (lem2 : forall x, ob (target f) x -> fob f (fob g x) = x). ir. wr fob_fcompose. rw H5. rw fob_fidentity. tv. rww H4. am. am. am. rww H4. assert (lem3 : forall u, mor (source f) u -> fmor g (fmor f u) = u). ir. wr fmor_fcompose. rw H6. rw fmor_fidentity. tv. am. am. am. am. am. assert (lem4 : forall u, mor (target f) u -> fmor f (fmor g u) = u). ir. wr fmor_fcompose. rw H5. rw fmor_fidentity. tv. rww H4. am. am. am. rww H4. uhg; ee. uhg; ee. am. ir. uh H9; ee. uh H10; ee. rwi cone_target_cone_pushdown H12. rwi cone_target_cone_pushdown H14. assert (cone_pushdown g (cone_pushdown f a) = a). rw cone_pushdown_are_inverse_invol. tv. am. uhg; ee; am. am. assert (cone_compose a (fmor g u) = cone_compose a (fmor g v)). wr H16. wr cone_pushdown_cone_compose. sy; wr cone_pushdown_cone_compose. rw H11. reflexivity. am. am. rw cone_target_cone_pushdown. am. rww H4. am. ap is_cone_cone_pushdown. am. am. am. am. rw cone_target_cone_pushdown. am. rw H4. am. am. uh H; ee. uh H; ee. assert (fmor g u = fmor g v). ap H19. uhg; ee. am. wr H1. rw H3. ap mor_fmor. am. rww H4. rw target_fmor. rw H13. rw vertex_cone_pushdown. rw lem1. tv. rw H1. ap ob_vertex. am. am. rww H4. uhg; ee. am. wr H1. rw H3. ap mor_fmor. am. rw H4. am. rw target_fmor. rw H15. rw vertex_cone_pushdown. rw lem1. tv. rw H1. ap ob_vertex. am. am. rww H4. am. wr lem4. wr H20. rw lem4. tv. am. am. uhg; ee. am. ir. cp H. uh H11. ee. uh H12. ee. util (H13 (cone_pushdown g b)). ap is_cone_cone_pushdown. am. am. uf cone_target. rw H10. rw socle_cone_pushdown. rw target_fcompose. am. rw socle_cone_pushdown. rw H10. rw socle_cone_pushdown. wr fcompose_assoc. rw H6. rw left_fidentity. tv. app socle_axioms. exact H1. am. am. app socle_axioms. am. exact H1. nin H14. ee. uh H14; ee. sh (fmor f x). ee. uhg; ee. ap is_cone_cone_pushdown. am. am. am. rw cone_target_cone_pushdown. ap mor_fmor. am. rw H1. am. rw vertex_cone_pushdown. rw target_fmor. rww H17. am. rww H1. wr cone_pushdown_cone_compose. rw H15. rw cone_pushdown_are_inverse_invol. tv. am. uhg; ee; am. uf cone_target. rw H10. rw socle_cone_pushdown. rw target_fcompose. am. am. am. am. rww H1. am. Qed.
imports: Arith nat_trans