@mikeshulman That's a failure of my tactic, I think, not a failure of this approach.  I've updated this pull request to factor out this part of the tactic into a separate lemma, which I've called `path_path_sigma`.  (This was at 64da19f14db7bf0abd15a3563ccd0a1f67caa854.  I subsequently realized that each step only got applied once, and removed the `repeat match goal` all together.  But I do think it's useful in other places, where lemmas will be applied multiple times.)  I think that any reasoning sufficiently complicated to be more enlightening as a step-by-step proof than as a tactic deserves its own lemma.  The idea behind fully automated proofs, I think, is that the automation should be mostly trivial and mostly brute force (I make exceptions for the "trivial" part when I need to do fancy things to get Coq to infer arguments correctly).  I do think that you should be able to understand a proof, at a high level, without stepping through it (though you might need to get the type of all the lemmas that it uses); any non-trivial bits of reasoning should be in their own lemmas.  (Trivial bits of reasoning include things like "remove all of the compositions with identity morphisms" and "uniformize associativity", which I think is where some of the tedium in simple diagram chasing proofs comes from.)