Are weakly étale ring homomorphisms of finite presentation étale? Following [Stacks, 092A], say a ring homomorphism $A \to B$ is weakly étale if both $A \to B$ and $B \otimes_A B \to B$ are flat.
Question. Are weakly étale ring homomorphisms of finite presentation étale?
According to Proposition 2.3.3 here, the answer is yes. Unfortunately, the proof cites some results in a monograph on generalised commutative algebra, which seems to be overkill. I am looking for a more self-contained proof, or at least one that could reasonably be said to be purely commutative algebra (possibly including homological algebra).
Looking around in [Stacks], I found the following: 


*

*By 092M, weakly étale ring homomorphisms are formally unramified.

*By 00UU, a formally unramified ring homomorphism of finite presentation is unramified.

*By 08WD, a flat unramified ring homomorphism of finite presentation is étale.


This seems to be a complete proof that weakly étale ring homomorphisms of finite presentation are indeed étale. Did I miss anything? I'm surprised that this statement does not appear outright in [Stacks].
 A: This is actually fairly easy. Indeed, if $f \colon A \to B$ is of finite presentation, then so is $B \otimes_A B \to B$ by Tag 00F4 (4). Moreover, the latter is flat by assumption, and it is always a surjective ring map (i.e., closed immersion). Thus, by Tag 0819, it is an open immersion onto a clopen subset.
Thus, the diagonal is an open immersion, which means that $f$ is unramified (Tag 02GE). Since it is also flat of finite presentation, this proves that $f$ is étale (Tag 02GV). (In the Stacks project, G-unramified means unramified and locally of finite presentation.) $\square$

Edit: I just noticed that this is the same as the explanation that the Stacks project gives, spread over the various tags you linked. Thus, the answer is: yes, it works, and no, you didn't miss anything.
My guess is that the first tag you gave is Johan's idea of including the result in the Stacks project; the statement you are interested in follows immediately from it. Another contributing factor is the observation that the finitely presented case is not typically what one is interested in when studying the pro-étale topology.
This section seems to be mostly written to include Olivier's theorem, given in Tag 092Z. Certainly for that theorem, the étale case is not very interesting.
A: This is kind of useless at this point, but since I was able to get a copy of one of Olivier's original articles on weakly étale/absolutely flat morphisms, I thought I'd share what I found.
The article

Ferrand, Daniel. "Epimorphismes d'anneaux et algèbres séparables." C. R. Acad. Sci. Paris Sér. A-B 265 1967 A411–A414. MR0244313 (39 #5628)

is cited as to having introduced the notion, but I can't spot it explicitly. The article that I was referring to above is

Olivier, Jean Pierre. "Montée des propriétés par morphismes absolument plats." Comptes-Rendus des Journées d'Algèbre Pure et Appliquée (Univ. Sci. Tech. Languedoc, Montpellier, 1971), pp. 86–109. Univ. Sci. Tech. Languedoc, Montpellier, 1971. MR0342509 (49 #7255)

The definition there is:
Definition. Let $f\colon X \to Y$ be a morphism of schemes. We say $f$ is diagonally flat if $\Delta_f\colon X \to X \times_Y X$ is flat. We say $f$ is absolutely flat if $f$ is flat and diagonally flat.
Olivier mentions that it is easy to see that a diagonally flat morphism is locally of finite type if and only if it is net, that is, formally unramified and locally of finite type as in Raynaud's Anneaux locaux henséliens, using (a modification of) the proof in Ch. III, §4, Prop. 9 (which is basically [Stacks, Tag 092M]). Strengthening this to locally of finite presentation, and then using that flat and unramified morphisms are étale gives you your statement.
In later papers Ferrand and Olivier just state that the statement you want is true without much comment, as do recent papers like Picavet's. What's also fun is that Paxia cites course notes by S. Greco for this result. 
