simp only and term mode

Stream: general

[Stuart Presnell]

I have a tactic mode proof of the form simp only, exact ..., where the simp only is simplifying a λ application. I want to turn this into a term mode proof. Is there an obvious way to do this that I'm missing?