rcases and equations à la `inl x = inl y`

Stream: lean4

[Jakob von Raumer]

Is there a reason that cases can handle targets like inl x = inl y while rcases can't? Would be cool to be able to use a rfl pattern on such equations too, even if it involves a congr application behind the scenes

[Mario Carneiro]

you should use the \<\> pattern on that equation

[Mario Carneiro]

rfl means to use subst, which has slightly different behavior from cases