Yes I've played with Agda before Lean. I found documentation for Agda to be sparse, maybe it's improved since then. Also, it was kind of a pain to get it setup. Lean was extremely easy to get running, works beautifully with VSCode, has great documentation and a helpful community. It's a "sexy" language and set of tooling compared to Agda and Coq (and I'm of the opinion aesthetics matter). It also feels more well-supported with the backing of Microsoft Research behind it.