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.)

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.

I wrote an introduction to pro-objects (in general) in a set of notes available via my nLab page: https://ncatlab.org/timporter/files/ProfAlgHomotopy.pdf You only need the first few pages of the main text, although you may find some useful ideas later on in the first chapter.

The definition of morphism in a procategory can possibly be best understood by looking at pro-representable functors. Left exact functors will be pro-representable (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. There are also some old notes of Duskin based on ideas of Verdier, who wrote a note J.-L. Verdier, Équivalence essentielle des syst`emes projectifs, C. R. Acad. Sci. Paris, 261, (1965), 4950–4953.)