Appearance of proof relevance in "ordinary mathematics?"

Proof mining (which even has a short Wikipedia article!), and area in large part developed by Kohlenbach, is mentioned briefly in the comments, and I thought it deserves a bigger mention. Roughly speaking, proof mining is the idea that from non-constructive proofs of existence one can often extract effective bounds. For example, from the standard proof of the irrationality of $sqrt{2}$ it is not hard to show that for any irreducible rational $frac{a}{b} > 1$ we must have that $|frac{a}{b} - sqrt{2}| > frac{1}{2b^2}$ (try it yourself!). This ties in with the irrationality measure of a real number.

Especially in its applications to functional analysis, such as in [Kohlenbach, U.; Leuştean, L.; Nicolae, A.; Quantitative results on Fejér monotone sequences. Commun. Contemp. Math. 20 (2018), no. 2], proof mining really shines through as a powerful set of techniques.

I attended a summer school in 2016 in which Kohlenbach presented these slides -- they are a gold mine of information, but can be rather dense at times. However, they provide an excellent overview for many important concepts in the area (such as Herbrand normal forms) and highlight many applications. A good introductory text is also this text by Kohlenbach and Oliva.

Some proof relevance in classical mathematics is going to be quite hard to see. While in HoTT, which proof of equality you choose may matter, it classical mathematics all proofs of equality are the same, so you won't be able to leverage them.

Take a slightly less trivial situation: proofs of $n leq m$. Well, it turns out that the canonical such proof is (unsuprisingly) isomorphic to $m-n$. Classically, if you needed the 'content' of $n leq m$, you'd just use $m-n$ and move on. Note that any member of $textsf{Fin}(m-n+1)$ is a witness for $n leq m$. The point is that the set of all proofs is $textsf{Fin}(m-n+1)$, of cardinality $m-n+1$. If you are proof-relevant, then any of those witnesses will do, not just the "tightest" one. And your results will then depend on that choice. Because it is "too easy" to see what the best choice is, it is thus rare to not pick it.

Moving up a tiny bit more: when you say let $X$ be a finite set of size $n$, you definitely don't care about what is in $X$ but you might still find something odd: if you leverage all the information from the premise, in a proof-relevant setting, you get a full isomorphism between $X$ and $textsf{Fin}(n)$; but $textsf{Fin}(n)$ is canonically ordered, so you can induce an ordering on $X$. Which ordering? Well, the one that's in your proof! There are $n!$ such possibilities. In a classical setting, one usually assumes, silently, that you don't depend on the proof, so you assume that $X$ is unordered. [Constructively, you can't blithely assume this, which is explained very well in Brent Yorgey's PhD Thesis.] In other words, this might be a source of proof-relevance, if you're not careful! Some code I wrote for Species in Haskell ended up being accidentally proof-relevant because of exactly this.

It is worth remembering that a bijection between $textsf{Fin}(m)$ and $textsf{Fin}(n)$ is a witness that $m=n$. Some theorems about permutations, when de-categorified, are theorems about set cardinality. Which set isomorphism you pick matters, because it gives you a different permutation. This has non-trivial implications for reversible programming (see my work with Amr Sabry if you're curious).

My feeling is that there is in fact a lot of "proof relevant" statements in classical mathematics, they just have not yet been recognized as being such.