mathlib

02d880b0 - perf(tactic/cache): call `freeze_local_instances` after `reset_instance_cache` (#3128)

perf(tactic/cache): call `freeze_local_instances` after `reset_instance_cache` (#3128) Calling `unfreeze_local_instances` unfreezes the local instances of the main goal, and thereby disables the type-class cache (for this goal). It is therefore advisable to call `freeze_local_instances` afterwards as soon as possible. (The type-class cache will still be trashed when you switch between goals with different local instances, but that's only half as bad as disabling the cache entirely.) To this end this PR contains several changes: * The `reset_instance_cache` function (and `resetI` tactic) immediately call `freeze_local_instances`. * The `unfreezeI` tactic is removed. Instead we introduce `unfreezingI { tac }`, which only temporarily unfreezes the local instances while executing `tac`. Try to keep `tac` as small as possible. * We add `substI h` and `casesI t` tactics (which are short for `unfreezingI { subst h }` and `unfreezingI { casesI t }`, resp.) as abbreviations for the most common uses of `unfreezingI`. * Various other uses of `unfreeze_local_instances` are eliminated. Avoid use of `unfreeze_local_instances` if possible. Use the `unfreezing tac` combinator instead (the non-interactive version of `unfreezingI`). See discussion at https://github.com/leanprover-community/mathlib/pull/3113#issuecomment-647150256 Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>