mathlib

8729fe21 - feat(tactic/simps): option `trace.simps.verbose` prints generated lemmas (#3121)