rw fails lin alg game

Stream: new members

[Andrea Bourque]

Hi, I'm doing the linear algebra game and I get this rw failure
image.png

[Andrea Bourque]

I tried specifying (0:K) and it still fails

[Riccardo Brasca]

Can you give a link to the game? VectorSpace is not a mathlib thing, so it's a little bit difficult to answer without being able to modify the code

[Andrea Bourque]

https://adam.math.hhu.de/#/g/zrtmrh/linearalgebragame/world/VectorSpaceWorld/level/1

[Riccardo Brasca]

Can you also provide the code you used to get to your goal?

[Andrea Bourque]

apply add_right_cancel (b := 0•w)
rw [zero_add]

[Riccardo Brasca]

The problem is the line add_right_cancel (b := 0•w)

[Riccardo Brasca]

Lean thinks that 0 is the natural number 0

[Riccardo Brasca]

So after apply add_right_cancel (b := 0•w) the goal is

0 • w + 0 • w = 0 + 0 • w

but the first 0 is in K and the second one is in ℕ, and now Lean is confused.

[Riccardo Brasca]

If you write

  apply add_right_cancel (b := (0 : K)•w)
  rw [zero_add, ← smul_add]

it works

[Andrea Bourque]

thanks!