I am hoping for a reference which discusses how tactics automatically eliminates, say, 990 cases out of 1000, so that a proof becomes manageable by a human.
For more background, in https://www.cse.chalmers.se/~abela/lehre/WS05-06/CAFR/4colproof.pdf, the author actually claimed that they did not need sophisticated tactics. They actually took advantage of definitional equality to do the main work, and it was in fact more difficult to use tactics to control the proof assistant, in their opinion, in section 4.
I believe that now, it has become the other way, where sophisticated automation is implemented as tactics and is responsible for killing more goals than exploiting computation, but I hope that someone actually wrote that down. I would like to know if anyone else shared the same opinion and provided some insight.