You might find the article "A proof of two fundamental theorems on linear transformations in Hilbert space, without use of the axiom of choice" by Iacopo Barsotti interesting.

Michael Hardy Thank you for the tip!

There is also this new proof of the straightening equivalence by Hebestreit, Heuts and Ruit which is much shorter than the one in HTT.

Thank you for your answer! I planned to rectify my question and include some of this information (which had been kindly communicated to me by Alessandra Bertapelle), but having been very busy I have not managed to do so quickly enough; I apologise for this.

@Jason Starr Thank you for pointing this out; none of this features in the paywalled text. However, I am a bit confused about the argument in the ArXiv version: it relies on Corollary 11.8 (of the ArXiv version; it does not appear in the published one), in whose proof a lemma which is valid only for a morphism of group schemes is applied to the change of ring morphism between two schemes which are Greenberg spaces of a smooth scheme, and need not be group schemes in general (I think). Maybe I am missing something trivial here.

@Jason Starr I hope I am not sounding polemic, but I disagree with you: I now see what you mean, but I do not agree with your interpretation of their sentence. With regard to the misleading accusation: if apologise I have mislead anyone; also notice that I did add some additional properties of such morphism which I thought might be relevant (affineness); of course I might have missed some others.

@Jason Starr Sorry, but I do not get your objection: if I write "$f$ is flat since it satisfies property P", then either P implies flatness or it does not and my argument is wrong, irregardless of whether $f$ is flat for other reasons. Also, notice that $f$ is not a morphism between spectra of discrete valuation rings, but between schemes over a field.