feat(tactic/simps): trace with @[simps?] (#6995)
feat(tactic/simps): trace with @[simps?] (#6995)

also trace with initialize_simps_projections?
trace when to_additive is applied to generated lemmas
with @[simps?] projection information is not printed (since that is often not as useful)







leanprover-community/mathlib,leanprover-community/mathlib