Lean tool references Documentation home · Tool surface Lean declaration discovery Lean formal intermediates Replayable Lean proof-state transitions Lean residual proof-state contracts Lean statement proposal and direct elaboration