How to do n_pow in the both side of the inequality?

Stream: new members

[Wenrong Zou]

Hi, everyone !
I don't know how to do 'n_pow' in the both side of the inequality. I don't know how to solve this sorry.

import Mathlib.Analysis.SpecialFunctions.Pow.Real
theorem th1 {a b : ℝ} {m : ℤ} {n : ℕ} (hn : n ≠ 0) (ha: 0 < a)
(hb : 0 < b) (h : a < b ^ (m / n)) :
  a ^ n < b ^ m := by sorry

I noticed that there are some Type coercion in the goal, which make m, n to \R. Does this coercion lose the information that n is \N and m is \Z.
Thanks in advance!

[Yaël Dillies]

This is a bug. There's a fix somewhere on Zulip but I don't know how to find it :grimacing:

[Xavier Roblot]

The fix is to add

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

See issue lean4#2220

[Wenrong Zou]

Xavier Roblot 发言道：

The fix is to add

local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

See issue lean4#2220

Thank you very much! I have fixed this bug.