mathlib documentation

core / init.meta.backward

meta constant tactic.back_lemmas  :
Type

meta def tactic.back_chaining_core (pre_tactic leaf_tactic : tactic unit) (extra_lemmas : list expr) :