Natural Number Game

Stream: new members

[Olonbayar Temuulen]

image.png
What is the best way to solve this, without relying on simp?

[Kevin Buzzard]

Is an acceptable reply "you shouldn't be in this state in the first place"? Are you trying to prove $(x+y)^2=x^2+2xy+y^2$ by induction instead of just multiplying it out?

[Kevin Buzzard]

The Pow.pow is a bit miserable in the hypotheses, how did that end up there? The user is supposed to never see that.

[Jon Eugster]

Kevin Buzzard said:

The Pow.pow is a bit miserable in the hypotheses, how did that end up there? The user is supposed to never see that.

That's been a "fix" in the new mathlib version turning a ^ b into Pow.pow a b. I pushed a fix for this a couple days ago, but haven't updated the live version yet. I'll do that now.

[Olonbayar Temuulen]

Via "being a bit overly adventurous with induction and trying to pin down exactly how add_assoc , add_mul, mul_assoc, mul_comm and to slightly lesser extent add_mul" worked, since the documentation felt a big vague. The notes on the left mention the user to check the targeting function comments of "rw", but i felt that the explanation there was lacking too.