Tactic for opposite of beta reduction

Stream: Is there code for X?

[Dylan Ede]

Is there a convenient way to convert a goal subterm e₁ that has a subterm e₂ into an application of e₂ to a function whose body is e₁ with the e₂ "hole" replaced with the argument of the function? Ideally I would only have to type out patterns to find e₁ and e₂, and not have to fully specify them.

[Kenny Lau]

generalize

[Dylan Ede]

I couldn't quite figure out how to apply generalize to this use case. Am I missing something obvious?

[Kyle Miller]

Could you give a #mwe to illustrate?

[Kyle Miller]

(generalize is sort of related, but I don't see how to use it to do exactly what you're asking for)