I should add that something like FStar [0] combines the capabilities of automated theorem proving and a more manual-proof-based dependent type system like that in Idris.

It doesn’t have some of the power of Idris’ elaborator reflection, for example, but it can eliminate many long-winded manual proofs via the SMT solver.

[0] https://www.fstar-lang.org/