Külshammer's list

[PatrickMassot]

Copy-pasting from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/MIL.20comments to make sure we don't forget

2.2: In the example at the end if one "feels cocky": Normally I would prove mul_right_inv before proving mul_one. Maybe this is just me and maybe it is a good lesson for "cocky" people. 2.3 As a beginner in Lean I was very confused over le_trans that addition and multiplication are by default left associated while implication is right associated. I feel like, this could be pointed out at this point (it is at least stated in Chapter 3. 2.3 "however we will use that fact that" should be "however we will use the fact that", small typo I think. 2.3 In the exercise to prove 0\le a^2, if I follow the advice and use library_search, then it replies "failed" for me. If I tell it that it has e^a\le e^b, then library_search does work, but also linarith works (with the same "amount of help"), so I didn't quite get the sentence below the exercise. 2.4 In the example where one should prove x | y * (x * z) + x^2 + w^2 could one put the lemma x | x^2 in the code that was proved before, so that one can use that instead of duplicating this part of the goal? 2.5 Small typo: "algebraic structures likes" should be "algebraic structures like" 2.5 You write that "It is a good exercise to prove that not every lattice is distributive by constructing one", unfortunately, what this tutorial seems to be missing is an explanation how to set up such a structure, i.e. how does one give an example of a group, a vector space, etc. Maybe this is worth another section/chapter to explain how to define a mathematical object and how to give an instance of a mathematical object.

[avigad]

I think I addressed all these... I'll close next time I come back, if there are no objections.