Lean's mostly used for maths, and tactics are much more ergonomic there. For writing correct-by-construction software programs, complex dependently-typed objects can be more ergonomic, as they allow passing a bunch of invariants through a program that are correct by construction, rather than needing to prove them at every stage via tactics.