Not sure if this is what you are looking for but Tychonoff's theorem has a snappy two line proof in the non-standard setting once the non-standard characterization of compact is established. The non-standard characterization of compactness says that $X$ is compact if and only if every $x\in X^*$ is infinitely close to some standard point in $X$ and infinitely close is defined in terms of the monads of the topology.
Edit: (Tychonoff) Tychonoff) $X := \prod_{i\in I}X_i$ is compact if and only if each $X_i$ is compact.
The forward direction is easy and does not require any non-standard analysis. Simply use the projection maps.
Now suppose all the $X_i$ are compact and let $y\in *X$ X^*$ then $y(*i)\in *(X_i)$. y(i^*)\in (X_i)^*$. Since $X_i$ is compact there is some $x(i)\in st(y(*i))$ st(y(i^*))$ and we can take $x\in X$ to be the product of the points of $x(i)$. By construction $*x\approx x^*\approx y$ and this establishes the backward direction.
The above theorem along with its non-standard proof can be found in "Nonstandard Analysis" by Martin V$\ddot{\mbox{a}}$thV$\ddot{a}$th on page 166 but I'm sure any other book on the subject will include a proof of the theorem using pretty much the same terminology and concepts.
Notation: $(-)^*$ is the extension map, $st(-)$ is the standard part map, and $\approx$ is the relation defined in terms of the monads of the topology.
