MIL section 2.1

Stream: general

[Anna Brosowsky]

A group of us our reading through MIL this semester, and I'm posting this question on behalf of someone without zulip:

I was following the textbook Mathematics in Lean, and in Section 2.1. Calculating, there is an exercise that asked me to prove that (a + b) * (a - b) = a ^ 2 - b ^ 2. It says, "The following exercise is a little more challenging. You can use the theorems listed underneath", and it lists the theorems pow_two, mul_sub, add_mul, add_sub, sub_sub, and add_zero. The wording for the exercise makes it seem like that it should be possible to complete the proof with only the listed theorems, but I was unable to find a proof that didn't use mul_comm and sub_self. (In particular, it isn't clear how to simplify b * a - a * b without these rules.)

Is there a solution to this problem that doesn't use mul_comm and sub_self, or should these theorems be added to the list?

P.S. Is this the right channel for us to post future MIL questions to?

[Patrick Massot]

I don’t think we intended to mean “only the theorems listed underneath”, I think it was meant as a list of extra theorems.

[Patrick Massot]

And it’s weird we didn’t include this in the solution files. This was written five years ago so I don’t remember if there was a specific reason for this, sorry.

[Anna Brosowsky]

Okay, thanks!