Commit 2024-07-20 01:12 58e38c45

feat: interactive unfold? tactic (#12016) This PR defines an interactive unfolding tactic. It suggests a list of unfolds, and when you select one, it pastes a rewrite tactic of the form rw [show current = unfolded from rfl]. This is part of #11768, which is a library rewrite tactic that also suggests the unfolds from this PR.