is there a version of convert_to that tries simp?

Stream: new members

[Matt Diamond]

I often find myself using the following pattern:

convert_to [some cleaned up statement] at h; simp

the idea being that I want the result of calling simp on a hypothesis, but I also don't want a non-terminal simp, so this allows me to simplify in a controlled fashion. Is there an easier way to do this with a single tactic? (I know I could also just write simp? and use the simp only result, but sometimes it's a bit long.) It might be nice to have a convert_to! tactic that automatically calls simp for you.

I know another option is

replace h : [some cleaned up statement] := simpa using h

[Kyle Miller]

Maybe convert_to ...e... at h <;> try (simp; done)?

This might be technically a non-terminal simp, but at least it's more controlled.