[ratmice]

Indeed, most of the book https://leanprover.github.io/logic_and_proof/ is entirely term mode proofs, with tactics largely absent.