TLA+ comes with a fairly minimal standard library, so to make it somewhat easier, I’ve written some operators that you might find useful. These all assume the context of model checking: you’re using finite sets, you’re okay with things crashing if you get them wrong, etc. Many of them assume other operators in other sections; I’ll note these as they come up.