problem at using rw tactic

Stream: new members

[Esteban Estupinan]

Hi all, I dont know why lean flagged an error when I trying to using rw tactic with conmutativaProducto definition if it is a equality apparently . Im trying to use m n implicit and explicit arguments like integers and error persists despite p and (m+n) are integers too. Where is the error and how can it be corrected? I know that this definition is already in mathlib but I would prefer to demonstrate this example using this simple definition that I think is not bad. your help please

\lean
def conmutativaProducto (m n : ℤ) := m * n = n * m
example (m n p : ℤ) : (m + n) * p = m * p + n * p :=
begin
calc (m + n) * p = p * (m + n) : by {rw conmutativaProducto (m + n) p}
... = p * m + p * n : by
end

[Esteban Estupinan]

when I change the word def by lemma it worked but why with def not? definitions are sentences that no need be proved or rw only works with theorems and lemmas and if need works rw with def is there a way?

[Scott Morrison]

Please read #mwe. :-)

[Scott Morrison]

Note that your conmutativaProducto is the statement the multiplication is commutative on the integers, not a proof of this fact! So you certainly can't rewrite by it (or use it for anything useful.)

[Scott Morrison]

You need to write something like:

lemma conmutativaProducto (m n : ℤ) : m * n = n * m := <proof-goes-here>

[Scott Morrison]

notice the different position of : and := relative to what you have written!