Eliminating `finish`

Stream: new members

[Stuart Presnell]

If I'm trying to eliminate the use of the finish tactic from a proof, is there a variant of it (or an option I can set) to make it spell out explicitly what it's done (like simp has the simp? and squeeze_simp alternatives)? Or more generally, is there a good strategy for how to go about eliminating the use of finish?

[Kevin Buzzard]

Does tidy solve the goal?

[Patrick Massot]

There is no squeeze_finish but you can always use show_term { finish }. And usually there is no surprise with finish, the fastest way to eliminate it is probably to write the proof term by hand.