Commit 2026-04-21 11:43 f489daf9

feat(gcongr): support rintro patterns (#36314) This PR adds support for rintro patterns in the with clause of gcongr. This makes it consistent with congr!. I've only found one case in mathlib where this could actually be used to shorten a proof. I split the gcongr elab into a separate syntax and elab_rules, which makes it easier to deal with the syntax. I noticed that the implementation of congr! was unnecessarily converting back and forth between rintroPat and rcasesPat, so I changed it to simply only use rintroPat, and then did the same in gcongr.