I'll have to agree with this. In particular, there always seems to be some stage where you'll have to think carefully about how the simplifier works exactly, about different types of equality (syntactic vs. definitional vs. provable), etc. And changing internal representations of objects will also mean that old proofs might not compile anymore. And tactics are often rather opaque blackboxes.

I say this as a non-expert who has been enjoying writing some Lean recently and has previously also written some Coq and Idris.