[Merged by Bors] - feat(tactic/simps): trace with @[simps?]

[fpvandoorn]

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)

---

@semorrison

Example:

@[simps?] protected def rfl {α} : α ≃ α :=
⟨id, λ x, x, λ x, rfl, λ x, rfl⟩

gives

[simps] > adding projection foo.rfl_to_fun:
        > ∀ {α : Sort u_1} (a : α), foo.rfl.to_fun a = id a
[simps] > adding projection foo.rfl_inv_fun:
        > ∀ {α : Sort u_1} (x : α), foo.rfl.inv_fun x = x

related Zulip thread

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests