Zulip Chat Archive

Stream: new members

Topic: Idiomatic rw of equality


view this post on Zulip Marc Masdeu (Oct 01 2020 at 17:44):

A pattern that I keep encountering is:

by_cases h : A = B,
rw h at *
...

Is there an idiom that does this at once? Thanks, and sorry all for the many questions...

view this post on Zulip Mario Carneiro (Oct 01 2020 at 17:47):

It's not much shorter, but I would suggest subst h instead if possible

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:51):

obtain (rfl|h) : A = B  A  B := by tauto,

view this post on Zulip Johan Commelin (Oct 01 2020 at 17:51):

Not saying that is nice solution

view this post on Zulip Mario Carneiro (Oct 01 2020 at 17:54):

You can get that down to obtain rfl|h := em (A=B)

view this post on Zulip Marc Masdeu (Oct 01 2020 at 18:46):

Thanks, from all your answers I guess the short answer to my question is NO, and the longer one is what @Mario Carneiro first replied...

view this post on Zulip Kevin Buzzard (Oct 01 2020 at 18:50):

The subst doesn't do the cases though, it's just a better way of doing the rewrite. The obtain trick does everything.

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 19:03):

rcases eq_or_lt_of_le (nat.zero_le x) with rfl|H is something I do sometimes.

view this post on Zulip Yakov Pechersky (Oct 01 2020 at 19:03):

But of course with more complicated les


Last updated: May 11 2021 at 00:31 UTC