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. 2 added clarifications 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. Edit: (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$then$y(*i)\in *(X_i)$. Since$X_i$is compact there is some$x(i)\in st(y(*i))$and we can take$x\in X$to be the product of the points of$x(i)$. By construction$*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}}\$th

1

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.