I know that in the area of "mechanical theorem proving in Geometry", there is a method (I may call it "point elimination" method) to solve some kinds of mechanical theorems proving problems in elementary geometry, and the algorithm is something like:
(1) Construct the points(and relations) involved according to the order of dependency.
(2) Eliminate the points(and relations) step by step by reversed order of dependency.
(3) You get the minimal amount of points in the game and the problem becomes an easy one.
I realize that this procedure of solving elementary geometry problems might be applied to the diagram chasing problem. Because the diagram chasing problem can be viewed as a graph problem in which "we construct the objects and arrows step by step and then figure out the relationship between them", and the "an object is unique up to unique isomorphism" in category theory is the same as "a point is determined by other points" in elementary geometry.
This idea comes to me when I was trying to prove that "the direct limit and stalk are interchangeable. i.e. $ (\lim \limits_{\longrightarrow pre} F_i)_p = \lim \limits_{\longrightarrow pre} (F_i)_p$", noticing that a stalk is just another direct limit, thus this proposition fits well in "diagram chasing" paradigm with basic ingredient in category theory, it should be solved mechanically in my simple mind...
I tried the "point(object) elimination" procedure in dealing with this proposition but I got stuck because it seems to me that there is no easy way of eliminating objects.
I wonder if the above idea makes any sense... Do I have a point here?
Update: I realize that the difficulty is to establish a verification relation $R$ releted to the proposition we want to prove. As the "elimination" precedure goes, $R$ becomes complicated in size but simple in nature(with less objects in $R$!). So for example, what is the verification relation $R$ when it comes to "the unique isomorphism between two objects"? I failed to establish $R$ to the "the direct limit and stalk are interchangeable" proposition.