The authors of Lean also wrote a smt solver (Z3). Other proof languages like F* use Z3 to prove its things

Why isn't there a tactic in Lean to prove things by SMT using Z3? This could be integrated to grind