I don't really buy this argument because we can all read the code with the Lean LSP.

Also, after using a tactic enough you can guess why it's used.

Agda and Idris are more beautiful for sure, but a proof is a proof (according to the law of the excluded middle)