The original proof I posted was organized slightly differently from your argument.

Some of those 120 lines were commentary, blanks and things like "qed". Also, I tried to used small steps in the proof. You can have a more concise proof if you are willing to take larger steps and rely more on automation. The cost is that the justification for the steps might become opaque to humans.

Here is a second attempt at the proof that follows your argument and uses more automation. It is much shorter than the original: https://gist.github.com/jmoy/27bcc72fb5a3f871b72c31e81bccb55...