## 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):

docs#real.rpow_nat_cast

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

Shing Tak Lam said:

docs#real.rpow_nat_cast

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