Zulip Chat Archive

Stream: general

Topic: show in conv mode

view this post on Zulip Kevin Buzzard (Mar 10 2018 at 17:24):

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?

Last updated: May 14 2021 at 04:22 UTC