To be clear though, all the mentioned languages are built on purely functional programming. Coq and Isabelle are more "procedural" in that they include special proof languages that express proofs in a step-by-step way that feels procedural, but the programs and definitions one proves properties of are still expressed in a functional style.
It's true that one needs to prove a lot of trivial things in all these systems, but the extent of this varies dramatically based on how much automation they provide. For example, Agda includes only minimal, barebones proof automation, while both Isabelle and Coq allow using more sophisticated automation that can take care of a lot of trivial steps automatically (such as "x == x").