I agree that you can—I've done that in Coq, though I don't have any experience with Lean. The advantage of Agda is that everyone else does, too. This provides

I agree that you can—I've done that in Coq, though I don't have any experience with Lean. The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have constructed their proof terms which encode best practices and are themselves designed to be as readable as possible, and two, people also build tooling which helps you to make them. In Coq, since tactics are primary, you end up with things like Sledgehammer. This is super practical and useful for tactics management, but it's a whole culture that will take you further and further away from understanding how proof terms work.