Setoids are also very relevant in constructive math, for similar reasons. Quotient types/sets basically conflate cases where one can easily normalize the elements of some equivalent class vs. cases where this cannot be done effectively, and that's not a good approach at all.
Lean's maths library development is essentially completely focussed on classical mathematics, which is why it has been so successful in drawing "working mathematicians" in. Such people do not care at all about the issues involving quotients, indeed quotients in Lean work just fine for them, and they don't care about constructibility either, because this is the prevailing culture in maths departments (although it is not, I am well aware, the prevailing culture in computer science departments). If you are interested in constructivism I would not recommend Lean. Many of the developments in mathlib are classical. That's why it's moving so quickly -- classical mathematics is much easier.