The same can be done also with Coq[1], it is easy to learn[2], actively developed[3], and better documented[4]. You can also visit their discussion board[5]. Regarding the usual Lean vs Coq "war" and so-called "setoid hell" you can read a lengthy discussion on their GitHub[6].
[1] http://coq.inria.fr/
[2] https://learnxinyminutes.com/docs/coq/
[3] https://github.com/coq/coq
[4] https://softwarefoundations.cis.upenn.edu/
[5] https://coq.discourse.group/
[6] https://github.com/coq/coq/issues/10871