Idiomatic rw of equality

Stream: new members

[Marc Masdeu]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Not saying that is nice solution

[Mario Carneiro]

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

[Marc Masdeu]

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]

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]

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

[Yakov Pechersky]

But of course with more complicated les