But is it a valid proof?

Stream: new members

[Dan Piponi]

I have this code

#check sub_self

example (x : ℤ) : x * 0 = 0 :=
calc
  x * 0 = x * (1 - 1)   : by rw sub_self
  ...   = x * 1 - x * 1 : mul_sub x 1 1
  ...   = 0             : sub_self (x * 1)

I run lean filename.lean

And get

sub_self : ∀ (a : ?M_1), a - a = 0

I can't tell if this is telling my attempted proof has failed. Normally I get error or similar if my proof is incorrect. Is this merely an informative message?