mathlib documentation

core.init.meta.backward

meta constant tactic.back_lemmas  :
Type