mathlib

89e18376 - fix(tactic/core): add subst' (#8129)

fix(tactic/core): add subst' (#8129) `tactic.subst'` gives a better error message when the substituted variable is a local definition. It is hard to fix this in core (without touching C++ code), since `tactic.is_local_def` is in mathlib