I think #Agda is by far the nicest purely at the language level (I'd probably consider Agda the prettiest language after Scheme), but 2gb is a lot of space, especially for someone like me that has lots of large 3D scene files, with massive textures, and am constantly making space on my laptop. #Coq is smaller then Lean, but a lot of OCaml also bleeds through, which is a great language, but not the most elegant, and I'm just trying to grill.
#Idris is really great and the one I've spent the most time with; I was even split between diving deep into either Idris or #Scheme a few years ago and chose the latter, as Edwin Brady's book is one of the best general introductions to FP I have read. But what I'm ultimately interested in exploring is Lean's hygienic macro system, and I'm overall really digging the lispyness hiding within Lean's mixfix notation