[gunnihinn]

As the post points out this involves some claims about infinite sets that are maybe not super obvious to laypeople (every infinite set of natural numbers has a least element). But we can rephrase this to avoid mentioning sets:

For any rational number p/q (with q > 0) there exists a smallest positive natural number k such that k * p/q is natural: Clearly q works, so we check the finitely many numbers 1, ..., q and pick the smallest.

Suppose the square root of 2 is rational. Let k be this smallest number for \sqrt 2, and proceed with the rest of the proof to find 0 < k' < k that also works.

[phkahler]

Fermat did several proofs by infinite descent without bringing set theory into it ;-)

[henrydark]

Actually he did use set theory, but there wasn't enough space in the margins

[bombcar]

There's a large body of math that can be proved simply, or proved complexly using set theory ;)

[zeroonetwothree]

You don’t have to pick the smallest, just start with q and then find you can keep decreasing it forever.