mathlib3

e0656d12 - chore(algebra/module/basic): golf a proof (#8723)