17.2. What is grind?

A proof‑automation tactic inspired by modern SMT solvers. Picture a virtual white‑board: every time grind discovers a new equality, inequality, or Boolean literal it writes that fact on the board, merges equivalent terms into buckets, and invites each engine to read from—and add back to—the same workspace. The cooperating engines are: congruence closure, constraint propagation, E‑matching, guided case analysis, and a suite of satellite theory solvers (linear integer arithmetic, commutative rings, …). Lean supports dependent types and a powerful type‑class system, and grind produces ordinary Lean proof terms for every fact it adds.