extract let in subexpression

Stream: lean4

[James Gallicchio]

I have this hypothesis in context:

h : (let vMap := ls_pre.vMap;  ...) = ls_post_pair

is there a tactic or clean way to extract this let as its own hypothesis?

[James Gallicchio]

extract_lets in particular expects hypotheses to have the let on the outside of the proposition/equality

[Eric Wieser]

Can you make a #mwe?

[Eric Wieser]

(does lift_lets exist?)

[Eric Wieser]

docs#Mathlib.Tactic.lift_lets !

[James Gallicchio]

that is perfect! thank you eric :)