Stream: math-comp users

Topic: Concise way to rewrite without intro & revert back?

view this post on Zulip abab9579 (Aug 27 2022 at 05:55):

Currently, I have loads of

move=> x y. rewrite Eq. move: x y.

Is there more concise way to do this?

view this post on Zulip Pierre Roux (Aug 27 2022 at 07:02):

Maybe move=> + + /[1!Eq]. or just rewrite Eq if it doesn't appear in x and y or something like rewrite [in X in _ -> _ -> X]Eqotherwise.

Last updated: Feb 02 2023 at 15:04 UTC