mathlib

43e3efe6 - golf(algebra/free_algebra): replace rintros with term-mode proof