Cancellation in direct products of finite groups

Let $A$, $B$, $C$ be finite groups. If $A \times B$ and $A \times C$ are isomorphic, then $B$ and $C$ are also isomorphic. That is, the common factor $A$ can be cancelled from both sides of the equation.

I learned a beautiful proof of this result from the Usenet newsgroup sci.math in 2001, while I was completing my Ph.D. dissertation. I rewrote the proof in a plain text file, and then forgot the details.

Today, I prompted ChatGPT to rewrite the proof carefully in LaTeX. I think that the result was pretty good. You can view the proof as a PDF.