theorem SnakeLemma.snake_lemma_exact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.composableArrows.Exact

Snake lemma: a snake input in an abelian category yields an exact sequence through the connecting homomorphism (Prop 42, Lec 23).

noncomputable def SnakeLemma.connectingHomomorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₀.X₃ ⟶ S.L₃.X₁

The connecting homomorphism produced by the snake lemma, mapping the third object of the top row to the first object of the bottom row.