Many basic lemmas in homological algebra, such as the five lemma, the 3x3 lemma and the snake lemma, are typically proven by diagram chases. See for instance the proof at five lemma or any book on homological algebra.
Use genuine generalized elements, see element in an abelian category. With these, the naive way of constructing morphisms (first showing that for every there exists a certain , then showing that this is independent of any choices made) carries over to the general setting.
Interpret constructive element-based proofs written in the fragment of regular logic using categorical semantics, see internal logic. The naive way of constructing morphisms works because the “axiom of unique choice” is valid in abelian categories (see Johnstone, Prop. D1.3.12).