mathlib

8a617238 - fix(algebra/punit_instance): punit.smul_eq is marked simp and can be proved by simp (#2291)