[Merged by Bors] - chore(*): use `gcongr`/`grw`#30561

urkud wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

urkud:use-gcongrurkud/mathlib4:use-gcongrCopy head branch name to clipboard