mathlib

69d41da5 - feat(tactic/dependencies): add tactics to compute (reverse) dependencies (#4602)

feat(tactic/dependencies): add tactics to compute (reverse) dependencies (#4602) These are the beginnings of an API about dependencies between expressions. For now, we only deal with dependencies and reverse dependencies of hypotheses, which are easy to compute. Breaking change: `tactic.revert_deps` is renamed to `tactic.revert_reverse_dependencies_of_hyp` for consistency. Its implementation is completely new, but should be equivalent to the old one except for the order in which hypotheses are reverted. (But the old implementation made no particular guarantees about this order anyway.)