Disclaimer: I know very little about Lean, so I would be happy to be proved wrong.
There is no escape from setoid hell. Lean simply gives a different way of doing the same thing one does in Coq.
In Lean, given a type $X$ with a relation $\sim$, we obtain a new type $\tilde X = X/\sim$ such that if $x\sim y$ then $[x] = [y]$. In Coq, $\tilde X$ is not allowed to be a type because we can no longer decide whether two elements of $\tilde X$ are equal (there is a way around this if your relation is decidable, say using SSReflect, and Lean probably has similar functionality).
In Lean, if you want to define a function $f : \tilde X\to Y$ (or a proposition on $\tilde X$), you need to use
quot.lift which requires you to prove that whenever $x \sim y$ then $f([x]) = f([y])$. In Coq, you simply define a function $f : X\to Y$, then prove a congruence lemma
f_eq saying that $x\sim y$ implies $f(x) = f(y)$.
Now the difference is that in Lean, given $x\sim y$ and $f : \tilde X\to Y$, you can rewrite $f([x])$ to $f([y])$ automatically using elimination for equality, whereas in Coq, you have to invoke the congruence lemma
So in summary, Lean keeps track of the congruence rule in the definition of $f$, whereas in Coq you have to keep track of $f$ and
I don't actually know exactly what setoid hell refers to, but if it refers to keeping track of congruence rules within the term then I suppose you could say Lean avoids this, but the amount of work you need to do is the same.
I am nethertheless going to quote Jacques Carette
Setoid hell arises not because some coherences must be proven. It arises when you're forced to prove these coherences again and again when defining functions that can't possibly "go wrong". So Setoid hell is actually caused by a failure to provide proper abstraction mechanisms.
As Jason Rute points out, this means that in Coq, if we want to prove nested equalities of the form $f(g(x)) = f(g(y))$ given $x\sim y$, we would need to first apply
g_eq, then apply
f_eq, which can be cumbersome. However, Coq supports generalized rewriting, where $f$ and $g$ can be declared as
Parametric Morphism's (given $\sim$ is declared a
Parametric Relation) which allows directly rewriting in this setting.