proof assistant automation tactics

Stream: general

[Julian Berman]

Is there a good resource for an overview of the "classes" of automation that exist in proof assistants? E.g. often folks ask things like "does Lean have sledgehammer", or "auto", or "a SAT solver", or a groebner basis tactic or etc. Presumably there are both mathematics-specific classes of tactic automation as well as pure CS ones, but curious to hear about whichever or both.

So -- how are pieces of automation (perhaps ones Lean indeed has, like simp, cc, etc.) categorized, and what's a good high level overview of the different uses of them?

[Julian Berman]

(Something hopefully more efficient than "read the tactics docs for Lean, Isabelle, Agda & Coq" :D)

[Jason Rute]

This might be a good question for the proof assistant stack exchange also.

[Jason Rute]

Also, there is always John Harrison’s massive tomb: Handbook of Practical Logic and Automated Reasoning

[Jason Rute]

(deleted)

[Eric Wieser]

Do you mean "tome"?