diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index 4c8a2c8a17..373a9e3f53 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -353,6 +353,9 @@ meta def add_lemmas_from_facts_core : list expr → smt_tactic unit
 meta def add_lemmas_from_facts : smt_tactic unit :=
 get_facts >>= add_lemmas_from_facts_core
 
+meta def induction (e : expr) (rec : name) (ids : list name) : smt_tactic unit :=
+slift (tactic.induction e rec ids)
+
 end smt_tactic
 
 open smt_tactic