The example involving quotient in sec.7.3 needs more detailed explanations

[ctchou]

The last example in sec.7.3 is the first time that the quotient construction appears in the book. But the explanation preceding it is rather terse and does not explain what the quotient construction is, how it works, and what sort of tactics are useful in dealing with it. Also, though the given solution works, it is not clear how the tactics in the solution are related to the proof states or even how some of the proof states should be read; see:

https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Reasoning.20about.20quotients

It would be great if more detailed explanations can be given.

[benjaminfjones]

The key thing I got hung up on in this exercise was the use of Quotient.sound. I think if that was explained in the paragraph above the exercise it would be more straightforward.

Also,

simp only [Relator.LiftFun]  -- removes the confusing ⇒ notation

is useful in the proof obligation for mul.