How to use equation compiler

Stream: new members

[Viktoriya Malyasova]

I have a proof of zero_mult theorem:
--theorem zero_mult (n : nat) : 0 * n = 0 :=
--nat.rec_on n
--(show 0 * 0 = 0, by refl)
--(assume n,
-- assume ih: 0 * n = 0,
-- show 0 * succ n = 0, from
-- calc
-- 0 * succ n = 0 * n: by refl
-- ... = 0 : by rw ih
--)
And I am trying to rewrite it using equation compiler:
theorem zero_mult (n : nat) : 0 * n = 0
| 0 := rfl
|(succ n) :=
calc
0 * succ n = 0 * n: by refl
... = 0 : by rw (zero_mult n)

Lean says:
function expected at
zero_mult
term has type
0 * n = 0
Why? How am I supposed to do this?

[Wojciech Nawrocki]

The equation compiler will only match arguments to the right of the colon (:), so to make it work your declaration should look like: theorem zero_mult : ∀ (n : nat), 0 * n = 0.

[Wojciech Nawrocki]

By the way, when posting Lean code here you can wrap it in three backticks on both sides to have it pretty-printed, like so (you can click "View source" on my message to see what I typed in):

theorem zero_mult : ∀ (n : nat), 0 * n = 0
| 0 := rfl
| (nat.succ n) :=
  calc
    0 * (nat.succ n) = 0 * n : by refl
    ...              = 0     : by rw (zero_mult n)

[Viktoriya Malyasova]

Thank you so much!!!