lean4

chore: upstream rcases (#3292)

chore: `rwa` tactic macro (#3299)

chore: add `nomatch` tactic (#3294)

fix: `nomatch` regression (#3296)

fix: extended `coe` notation and delaborator (#3295)