# Zulip Chat Archive

## Stream: new members

### Topic: Proving 64 = (4:ℝ) ^ (3:ℝ)

#### Kunhao Zheng (May 03 2021 at 09:51):

Hi! I've been in difficulty when I tried to prove this equality, I've browsed through the other topics and found some subtlety in type theory, but I think this one is provable as they are both of type ℝ, but I don't know exactly how when `norm_cast`

failed.

```
import tactic.basic
import data.real.basic
import analysis.special_functions.pow
import data.nat.basic
example : ↑ ( 1 * 2 ) = (1:ℝ) * 2 :=
begin
norm_cast,
end
example : ↑ ( 1 ^ 2 ) = (1:ℝ) ^ 2 :=
begin
norm_cast,
end
example : ↑ ( 1 ^ 2 ) = (1:ℝ) ^ (2:ℝ) :=
begin
simp,
end
```

These simple examples above work magically( The 3rd one will panic when I use `norm_cast`

), but when it comes to

```
import tactic.basic
import data.real.basic
import analysis.special_functions.pow
import data.nat.basic
example : ↑ ( 4 ^ 3 ) = (4:ℝ) ^ (3:ℝ) :=
begin
nth_rewrite 0 [pow_succ'],
simp,
simp [pow_succ],
sorry
end
example : (64:ℝ) = 4^(3:ℝ) :=
begin
suffices : (64:ℝ) = 4^3, {
rw this,
norm_cast,
sorry
},
linarith,
end
```

Cheating like `norm_cast`

or `simp`

won't work...

If possible, how can I see what's going on under the hood when I apply `norm_cast`

or `simp`

? I think maybe that helps to inspect how it succeeds in the simple ones.

#### Mario Carneiro (May 03 2021 at 09:54):

My suggestion: rewrite it to `4^((3:nat):real)`

with norm_cast, use a lemma to turn it into `4^(3:nat)`

and then norm_num

#### Kunhao Zheng (May 03 2021 at 11:11):

I've found some lemma which lift the first argument of pow, like `nat.cast_pow`

, but I didn't find what I need that can lift the exponent.

#### Shing Tak Lam (May 03 2021 at 11:13):

#### Kunhao Zheng (May 03 2021 at 11:16):

Shing Tak Lam said:

Thank you! @Shing Tak Lam and @Mario Carneiro, that saved my day. I managed to finish this proof by following the hint.

```
import tactic.basic
import data.real.basic
import analysis.special_functions.pow
import data.nat.basic
example : (64:ℝ) = 4^(3:ℝ) :=
begin
suffices : (64:ℝ) = 4^((3:ℕ):ℝ), {
rw this,
norm_cast,
},
suffices : (64:ℝ) = 4^(3:ℕ), {
rw this,
rw eq_comm,
exact real.rpow_nat_cast (4:ℝ) 3,
},
norm_num,
end
```

#### Eric Wieser (May 03 2021 at 15:19):

This is a nice opportunity to use `calc`

blocks:

```
example : (64 : ℝ) = 4^(3 : ℝ) :=
calc (64 : ℝ) = 4^(3 : ℕ) : by norm_num
... = 4^((3 : ℕ) : ℝ) : by rw real.rpow_nat_cast
... = 4^(3 : ℝ) : by norm_cast
```

Last updated: Dec 20 2023 at 11:08 UTC