mathlib

356447fe - feat(tactic/rcases.lean): `@⟨p1, p2⟩` patterns in `rcases` (#16617)

feat(tactic/rcases.lean): `@⟨p1, p2⟩` patterns in `rcases` (#16617) This PR implements the syntax `@pat` inside rcases patterns, before tuple patterns. It has the effect of making the patterns line up with all arguments to the constructor, rather than just the explicit ones. The original behavior is equivalent to using `@` everywhere.