Suggestion: add illustration of trace.Meta.Tactic.simp.rewrite

I just came across an illustration of trace.Meta.Tactic.simp.rewrite here: https://leanprover-community.github.io/extras/simp.html

I wanted to suggest including mention of this, and maybe other trace options like it, either in chapter 9 or in earlier or later discussions of simp (and maybe other tactics?).

Bacground: While reading FPIL chapter 9, I started to want to know more about what simp is doing. It does so much that its capabilities are necessarily mysterious, but that makes it difficult to know when it would be useful--without just throwing it into code and seeing what happens. The remark concerning <;> that it allowed tactics like simp to be applied to multiple goals simultaneously especially pushed me to want to know more about what simp was doing. If simp is doing different things with different goals, I'd like to have some idea of what it's doing. I recognize that the remarks about <;> might be intended only as flagging an advanced technique that a beginner might grow into 😄, but this still pushed me to want to get more insight into simp.

The trace output is a little bit hard to read at first, but I think I mostly understand it for the plusR_zero_left example using <;>, and It's very illuminating for me. If FPIL introduced tactic tracing, it could also clarify what's potentially confusing about the trace output.

Start with chapter 9 of FPIL and review its discussion of simp and the <;> combinator alongside the suggested trace.Meta.Tactic.simp.rewrite example. Done means adding a clear, appropriately scoped introduction to tactic tracing and explaining enough of the trace output to help readers understand what simp is doing.