Can a generalize equality hypothesis be converted into a let

Stream: lean4

[Malcolm Langfield]

When you generalize h : _ = x, you get an equality h, which can then be inlined into your proof whenever you like, with subst h. Is it possible to convert h into a let binding? If x occurs in many places in the target, and the LHS of h is quite large, this crowds up the infoview a lot and I'd like to avoid that if possible.

[Yaël Dillies]

Do you know about tactic#set ?

[Malcolm Langfield]

Oh I think maybe that's exactly what I want, thanks!