So is homotopic type theory just another way to look at the same thing or is it more expressive than type and set theory?
In other words, does homotopic type theory really help theorem checkers/provers?
Well, adding consistent axioms often allows proving more thing, but that in itself does not necessarily mean it's more useful, and certainly not that proofs are easier -- that, I believe, was the question. For example, adding the axiom 1/0 = 0 is consistent with ordinary arithmetics, and also allows you to prove more things (e.g. that 1/0 = 0), but is not necessarily useful and not necessarily helpful.
Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.