I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical.

It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)

I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.

You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think

Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop.

[1] https://arxiv.org/abs/1911.08174

There is also a problem of HoTT and equality reflection incompatibility[1].

[1] https://www2.mathematik.tu-darmstadt.de/~streicher/barc_corr...