show in conv mode

Stream: general

[Kevin Buzzard]

I have some goal of the form X = Y where Y is one of these annoying terms that I can't cut and paste from pretty printer output (in this case, I believe, because it has replaced a proof with _). I want to use show to rewrite X as X' but I can't write show X'=Y because my problems with Y. I could prove X=X' using rfl and then use a rewrite. But it would be cool to use conv mode, use to_lhs to restrict to X and then use some conv version of show to replace X with X'. Can this be done?