Where to direct you to learn about pro-objects depends on how general a form you need and, to some extent, your background. If you look at inverse systems/sequences of modules (as in the case you cite), then look at the nLab entry on towers, and also on profinite groups. Pro-objects provide a sense of approximation to a limit object that may not be in the category you are looking at, e.g. a pro-finite group is an inverse system of finite groups.  If you take its limit the result will often not be a finite group. The finite quotients of a group form a profinite group in this sense. There is also a topological approach which comes in in your pro-A-module setting as well. Nice systems of cofinite submodules will form a pro-module in an analogous way.

The definition of morphism in a procategory can possibly   be best  understood by looking at pro-representable functors. Left exact functors will be pro-represntable (check again on the nlab for the definition) and natural transformations between pro-representable functors give exactly that definition of pro-morphism. An approach that will perhaps help you understand Bhatt's second statement is to work when a pro-module (in general) will be isomorphic to a zero pro-module.(Some ideas relating to this can be found in a book by Cordier and myself that you may find answers some of the basic points, see the nLab page on pro-objects for the details of the book.)