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").
> they include special proof languages that express proofs in a step-by-step way that feels procedural
Serious proof developments don't even use the languages in a procedural way. They use "declarative" idioms/patterns that are structured more like a very detailed human proof. This is because "procedural" interaction with the proof state is extremely fragile (it's like raw assembly code, the slightest change in any part of the proof can break basically everything else in it) plus it actually requires "replaying" the proof in order to have any chance of understanding how it works. Declarative idioms can be read and understood directly, at least to some extent.
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").