mathlib

4f5d6acf - refactor(tactic/interactive): rename tactic.interactive.triv to tactic.interactive.trivial' (#11643)

refactor(tactic/interactive): rename tactic.interactive.triv to tactic.interactive.trivial' (#11643) The difference between `tactic.interactive.trivial` and `tactic.interactive.triv` is that the latter expands only reducible constants; the first uses `tactic.triv` and the latter uses `tactic.triv'`. This name change is to improve consistency. Also (slipping in a new feature) add `tactic.interactive.triv`, which is the old `tactic.interactive.triv` but does not run `contradiction`. This is useful for teaching.