Whoops, you're right. Here's what Fields medalist Terence Tao has to say about it: https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-... "...sometimes, after a proposition has been proven, someone in the project realizes that in order to apply the proposition neatly in some other part of the project, one has to slightly modify a hypothesis ... Often one can just modify that hypothesis and watch what the compiler does. ... [W]ith well-designed proofs, the process of modifying a proposition is often substantially easier than writing a proof from scratch. (Indeed it is this aspect of formalization where I think we really have a chance in the future of being in a situation where the task is faster to perform in a formal framework than in traditional pen-and-paper (and LaTeX) framework.)"
> And if they explain that you are misunderstanding the system
I don't think that's a fair description of the sibling threads. If a mathlib maintainer says "no, we're not going to avoid LEM/by-contradiction everywhere in our proof library, that would be silly" because that's what most mathematicians today think constructivism means, as in rejecting the bulk of existing math entirely as meaningless - and then they add "but yes, there are places where we want to work with our own assertions about decidability, and not let classical reasoning mess that up" I think it's entirely fair to call the latter pretty close to a constructivism-friendly approach.
(Keep in mind that most practicing mathematicians don't work with foundations, so the fact that misconceptions like the above would be widespread is not surprising. The remaining argument is about the increased complexity of constructive reasoning, and it's entirely fair for a practical development to want to avoid that, and just work with classical statements. After all, most of the mathematical literature is indeed classical; it does not bother with the computational aspect or with the perceived messiness of numerical analysis.)