1) GCD3 theorem information in the text seems to suggest the following should work:
==========================
THEOREM GCD3 == \A m, n \in Number : (n > m) => (GCD(m, n) = GCD(m, n-m))
<1> SUFFICES ASSUME NEW m \in Number, NEW n \in Number,
n > m
PROVE GCD(m, n) = GCD(m, n-m)
OBVIOUS
<1>1. \A i \in Int : Divides(i, m) /\ Divides(i, n)
<=> Divides(i, m) /\ Divides(i, n - m)
BY LemmaDiv DEF Divides
<1> QED
BY DEF GCD, SetMax, DivisorsOf, Divides
==========================
But <1>1 doesn't prove. I probably misunderstood.
I'm not quite sure which part of the hyperbook you looked at. The informal proof in the main track has four steps and uses lemma Div. The formal proof in the proof track (chapter 11.2) doesn't mention that lemma: in fact, the SMT backend is smart enough to perform that reasoning. Reconstructing the lemma from what is written in the hyperbook, I obtain
THEOREM GCD3 == \A m,n \in Nat \ {0} : (n > m) => (GCD(m, n) = GCD(m, n - m))
<1>. SUFFICES ASSUME NEW m \in Nat \ {0}, NEW n \in Nat \ {0}, n > m
PROVE GCD(m, n) = GCD(m, n - m)
OBVIOUS
<1>. \A i \in Int : Divides(i,m) /\ Divides(i,n)
<=> Divides(i,m) /\ Divides(i, n - m)
BY DEF Divides
<1>. QED BY DEF GCD, SetMax, DivisorsOf
and this is indeed proved. It's very similar to what you wrote except that (a) I don't invoke LemmaDiv, (b) all steps are unnumbered, and (c) I use Nat and Int whereas you have Number and Int. Let's look at each difference:
(a) Adding LemmaDiv (whatever it may be) might confuse the backend but it seems unlikely that this is the problem.
(b) It's obvious that you need to add <1>1 as a fact to the proof of the QED step, but that doesn't affect the proof of your step <1>1.
(c) This must be the real difference: you should expand the definition of Number, otherwise the prover cannot apply the definition of Divides, which (according to the hyperbook) is stated for Int.
Anyway, I attach my full module to this message so that we are on the same page.
2) The proofs section breaking down Inv /\ [Next]_vars => Inv', I needed to add 'BY UNCHANGED vars' to steps <2>2 and <2>3. It didn't seem to pick it up from ASSUMES, and I didn't see anything in the text about it.
I don't quite see where you are pointing since the hyperbook doesn't seem to show all the details of that proof but I presume that the assumption UNCHANGED vars appears the step enclosing the one you are trying to prove. You have to invoke that step in the facts that appear in the BY clause, as in:
<4>42. ASSUME Inv, UNCHANGED vars PROVE Inv'
BY <4>42 DEF Inv, vars
The basic principle is that all necessary facts and definitions have to be named explicitly in proofs, except for those mentioned in a USE [DEF] clause or for facts in unnumbered steps that cannot be named. The apparently circular reference <4>42 in the step above refers to the assumption of the current step. References to <4>42 outside of its own proof refer to the entire ASSUME PROVE clause.
By the way, the module attached to this message contains a simpler proof of the theorem: the decompositions introduced in the hyperbook are given for pedagogical purposes.
3) I couldn't get a TLC model to run with the Euclid PlusCal module. It just won't start, no error messages or anything. I had a model running for GCD module just fine.
I cannot reproduce this problem. More specifically, I can run TLC on the module attached to this message. Concretely, I instantiated M and N by 42 and 24 and told TLC to verify the invariants Inv and PartialCorrectness. As expected, TLC complains that it cannot enumerate Int, so I have to override the definition of Int (in Advanced Options -> Definition Override), for example by the interval -100 .. 100.
4) I saw an assertion when I accidentally put a proof step <1>4 in USE DEF <1>4 instead of USE <1>4 DEF .. I assumed it was not surprising this caused weirdness.
Yes, this should eventually be caught by the proof manager instead of raising an assertion ...