fix(analysis/special_functions/pow): fix norm_num extension (#14099)

As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/kernel.20slow.20to.20accept.20refl.20proof/near/282043840).

Author: digama0

src/analysis/special_functions/pow.lean

@@ -1864,11 +1864,11 @@ lemma filter.tendsto.ennrpow_const {α : Type*} {f : filter α} {m : α → ℝ
 namespace norm_num
 open tactic
 
-theorem rpow_pos (a b : ℝ) (b' : ℕ) (c : ℝ) (hb : b = b') (h : a ^ b' = c) : a ^ b = c :=
-by rw [← h, hb, real.rpow_nat_cast]
+theorem rpow_pos (a b : ℝ) (b' : ℕ) (c : ℝ) (hb : (b':ℝ) = b) (h : a ^ b' = c) : a ^ b = c :=
+by rw [← h, ← hb, real.rpow_nat_cast]
 theorem rpow_neg (a b : ℝ) (b' : ℕ) (c c' : ℝ)
-  (a0 : 0 ≤ a) (hb : b = b') (h : a ^ b' = c) (hc : c⁻¹ = c') : a ^ -b = c' :=
-by rw [← hc, ← h, hb, real.rpow_neg a0, real.rpow_nat_cast]
+  (a0 : 0 ≤ a) (hb : (b':ℝ) = b) (h : a ^ b' = c) (hc : c⁻¹ = c') : a ^ -b = c' :=
+by rw [← hc, ← h, ← hb, real.rpow_neg a0, real.rpow_nat_cast]
 
 /-- Evaluate `real.rpow a b` where `a` is a rational numeral and `b` is an integer.
 (This cannot go via the generalized version `prove_rpow'` because `rpow_pos` has a side condition;

test/norm_num_ext.lean

@@ -9,6 +9,7 @@ import data.int.gcd
 import data.nat.fib
 import data.nat.prime
 import data.nat.sqrt_norm_num
+import analysis.special_functions.pow
 
 /-!
 # Tests for `norm_num` extensions
@@ -257,6 +258,10 @@ example : nat.fib 37 = 24157817 := by norm_num
 example : nat.fib 64 = 10610209857723 := by norm_num
 example : nat.fib 100 + nat.fib 101 = nat.fib 102 := by norm_num
 
+example : (2 : ℝ) ^ (3 : ℝ) = 8 := by norm_num
+example : (1 : ℝ) ^ (20 : ℝ) = 1 := by norm_num
+example : (2 : ℝ) ^ (-3 : ℝ) = 1/8 := by norm_num
+
 section big_operators
 
 variables {α : Type*} [comm_ring α]