Explicit zeta and beta reductions

Stream: Is there code for X?

[Nikolas Kuhn]

This is a basic question, so I already apologize for probably missing something fundamental.
Suppose that in a tactic block, I have a definition of the form
'let g:= ...'
and that my goal explicitly involves g. Is it possible to change the goal by substituting the definition of g (doing a zeta reduction)? The only way I see how to do this is by calling 'simp only [g],' but I'd hope that it wouldn't be necessary to invoke the simplifier, both since it seems more costly and since it might do some additional simplification.
The same question came up for beta reduction: Suppose that 'f' is a function, and that my goal involves '(λ x, f x) y'. What is the best way to explicitly modify this term to f y in the goal?

[Notification Bot]

Nikolas Kuhn has marked this topic as resolved.