how to use the pow_add theorem

Stream: maths

[Truong Nguyen]

Dear Alls,
The pow_add theorem is as follow:

#check pow_add
pow_add : ∀ (a : ?M_1) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n

By why can't I prove the consequence theorem:

theorem th01 (a: ℕ ): ∀ m n:ℕ, a ^ (m + n) = (a ^ m) * (a ^ n) :=
begin
rw pow_add (a:ℕ)
end

Here is the error that I got:

rewrite tactic failed, did not find instance of the pattern in the target expression
a ^ (?m_1 + ?m_2)
Thank you,

[Kenny Lau]

(deleted)

[Chris Hughes]

It's because you need to use nat.pow_add

[Kenny Lau]

because the ^ are different

[Mario Carneiro]

nat has a different instance for the power function, so it has its own theorems to go with it, like nat.pow_add

[Chris Hughes]

This is a very annoying feature of current lean. There are two definitions of pow on the naturals.

[Mario Carneiro]

If nat.pow_add was not proven, you could also use by simpa using pow_add a to prove it

[Truong Nguyen]

Dear Mario,
can you be more specific, what is by simpa using pow_add a.

[Truong Nguyen]

I changed to this:

theorem th01 (a: ℕ ): ∀ m n:ℕ, a ^ (m + n) = (a ^ m) * (a ^ n) :=
begin
rw [nat.pow_add (a:ℕ )]
end

But, it did not work neither.

[Mario Carneiro]

import algebra.group_power

theorem th01 (a m n : ℕ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
by simpa using pow_add a m n

[Mario Carneiro]

theorem th01 (a m n : ℕ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
by rw nat.pow_add

[Mario Carneiro]

theorem th01 (a m n : ℕ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
nat.pow_add _ _ _

[Mario Carneiro]

note that you need to have all the variables left of the colon for rw to work here

[Truong Nguyen]

Oh, great
Do you know how can I find the tutorial of using "simpa".

I have the following issue as well. I think it can be done in similar way.

How to use the theorem:
#check cardinal.mul_power
cardinal.mul_power : (?M_1 * ?M_2) ^ ?M_3 = ?M_1 ^ ?M_3 * ?M_2 ^ ?M_3

To prove that:
theorem th07 (a b n: \N): (a * b)^n = a ^n*b^n.

[Mario Carneiro]

That is an unrelated use of power; although it is possible it would be a weird way to prove that theorem for natural numbers

[Mario Carneiro]

the theorem itself is nat.mul_pow

[Truong Nguyen]

when I run the command:
#check nat.mul_pow

it gave me nothing.

[Patrick Massot]

you need to import https://github.com/leanprover/mathlib/blob/dd0c0aeefcaf6a438ab4273d7a1f42e1b8225847/data/nat/basic.lean

[Patrick Massot]

import data.nat.basic

[Truong Nguyen]

Hello,
do you know where can I find the tutorial of using "simpa".

[Patrick Massot]

I think we don't have anything better than https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#simpa

[Truong Nguyen]

Oh, thank you