Forget definition

Stream: lean4

[Uni Marx]

If I introduce some f in tactic mode via let f := ..., how can I at some point "forget" the definition of f without changing any further statements in context associated with it? it's fairly complicated and gets unfolded by simp even if it's not useful at all

[Eric Wieser]

clear_value f

[Uni Marx]

thanks! is there an overall list of somewhat commonly used lean4 tactics somewhere in general?

[Bhakti Shah]

At least for basic tactics, I've been looking here, and with some searching you can get to the more refined mathlib tactics too. Personally I've just been using the menu on the left hand side to navigate, and making an educated guess on what the tactic im looking for could be called. Not the most efficient, but it has worked for me :)