How do 'tactics' work in proof assistants?
The basic tactics either run an inference rule forwards or backwards (for example, convert hypotheses $A$ and $B$ into $A\wedge B$ or convert goal $A\wedge B$ into two goals $A$ and $B$ with same hypotheses), apply a lemma (~ function application), split up a lemma about some inductive type into a case for each constructor, and so on. Basic tactics may succeed or fail depending upon the context in which they are applied. More advanced tactics are like little functional programs that run the basic tactics, perform pattern matching over the terms in the goal and/or assumptions, make choices based on the success or failure of tactics, and so forth. More advanced tactics deal with arithmetic and other specific kinds of theories. The key paper on Coq's tactic language is the following:


D. Delahaye. A Tactic Language for the System Coq. In Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island, volume 1955 of Lecture Notes in Computer Science, pages 85–95. Springer-Verlag, November 2000.


The formal rules which form the essence of the basic tactics are defined in the Coq users guide here or in Chapter 4 of the pdf.

A quite instructive paper on implementing tactics and tacticals (essentially tactics that take other tactics as arguments) is:


Amy Felty. Implementing Tactics and Tacticals in a Higher-order Programming Language Journal of Automated Reasoning, 11(1):43-81, August 1993.


Coq's tactic language has the limitation that the proofs written using it hardly resemble proofs one does by hand. Several attempts have been made to enable clearer proofs. These include Isar (for Isabelle/HOL) and Mizar's proof language.

Aside:
Did you also know that the programming language ML was originally designed to implement tactics for the LCF theorem prover? Many ideas developed for ML, such as type inference, have influenced modern programming languages.