This repository provides a Lean 4 tactic `smt` that automates theorem proving by delegating goals to the cvc5 SMT solver and reconstructing the resulting proof in Lean. It supports a range of theories including uninterpreted functions, linear integer and real arithmetic, bitvectors, strings, and quantifiers. The codebase is organized into preprocessing (normalization, monomorphization, embedding), translation to SMT-LIB, solver communication, and proof reconstruction for each theory. The project is in beta but actively developed, with extensive test coverage across supported domains. While the primary interface is a tactic, the architecture reveals multiple reusable components such as an S-expression DSL, SMT term representation, graph data structure, and a configurable WHNF reduction engine. The main entry point is `Smt/Tactic/Smt.lean`, and the library is distributed as a Lean package. The code is tightly integrated with the cvc5 FFI and Lean's metaprogramming infrastructure, making it primarily a library rather than a standalone application, but it fits the 'application' category as a tool for interactive theorem proving.