An introduction to actor-critic algorithms as dynamical systems: featuring hand-computable examples, fast-slow reductions, and machine-checked Lean 4 proofs