Do dependent types give you everything subtyping does? Types and Programming Languages focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types do? Working with dependent types is bound to be more work, so I can understand why subtypes might be useful in practice. However, I am more interested in type theory as a foundation for mathematics than as a basis for programming languages, should I pay much attention to subtyping?
Subtyping and dependent types are orthogonal concepts. 

Subtyping is typically equipped with a notion of subsumption, whereby an expression of one type can appear in place where a supertype is expected.

Subtyping is more likely to be decidable and is more simply to manage in implementation.

Dependent typing is vastly more expressive. But if you ever want to consider a group to also be a monoid, then you need a notion of subsumption to forget the extra structure. Often, such as when using Coq, a trivial proof obligation is generated to deal with this kind of coercion, so in practice subtyping may not add anything. What's more important is having ways of packaging together various theories to make them reusable, such as reusing the theory of monoids when talking about groups. Type classes in Coq are a recent innovation for doing such things. Modules are an older approach.

If you do a quick google of "subtyping dependent types" you find a bunch of work adding subtyping to dependent types, mostly from around the year 2000. I imagine that the meta-theory is really challenging, so no subtyping of dependent types appears in proof assistants.