using sub_eq_add_neg in calc

Stream: new members

[Pradana Aumars]

Hello everyone,

I'm just getting started with Lean by proving 0x = 0 for any real x. Here's the code:

lemma prop1a (x : ℝ) : 0*x = 0 :=
begin
  apply eq.symm,
  calc 0 = 0*x - 0*x : by rw sub_self
  ... = 0*x + (-0*x) : by rw sub_eq_add_neg
  ... = (0 + 0)*x  + (-0*x) : by rw add_zero
  ... = 0*x + 0*x + (-0*x) : by rw right_distrib
  ... = 0*x + (0*x + (-0*x)) : by rw add_assoc
  ... = 0*x : by rw sub_self
end

I do not understand why
rw sub_eq_add_neg
returns two different states: 0 * x + -(0 * x) = 0 * x + -0 * x and 0 = 0 * x

What's going on here?

Thank you

[Eric Wieser]

Does realizing -0 * x is interpreted as (-0)*x help?

[Pradana Aumars]

I got it now, thanks!