## Stream: new members

### Topic: Idiomatic rw of equality

#### 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...

#### Mario Carneiro (Oct 01 2020 at 17:47):

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

#### Johan Commelin (Oct 01 2020 at 17:51):

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


#### Johan Commelin (Oct 01 2020 at 17:51):

Not saying that is nice solution

#### Mario Carneiro (Oct 01 2020 at 17:54):

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

#### 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...

#### 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.

#### 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.

#### Yakov Pechersky (Oct 01 2020 at 19:03):

But of course with more complicated les

Last updated: May 11 2021 at 00:31 UTC