# Zulip Chat Archive

## Stream: new members

### Topic: How to use equation compiler

#### Viktoriya Malyasova (Mar 16 2020 at 18:39):

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 (Mar 16 2020 at 18:47):

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 (Mar 16 2020 at 18:48):

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 (Mar 16 2020 at 22:07):

Thank you so much!!!

Last updated: May 11 2021 at 00:31 UTC