Unsure about proper use of cast tactics

Stream: new members

[Walter Moreira]

I'm not sure I'm properly using the tactics that deal with casting. The following example looks like it should be simpler that what I'm doing, since I had to apply twice the casting. Any ideas about what I'm doing inefficiently? (There might also be a lemma with this fact, but I couldn't find it with the combination apply? + loogle + leansearch.)

import Mathlib

example (x y : ℝ) (n : ℕ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : 0 < n) (h : x ^ ((n : ℝ)⁻¹) ≤ y) :
    x ≤ y ^ n := by
  exact_mod_cast (Real.rpow_inv_le_iff_of_pos hx hy (by norm_cast)).mp h

[Daniel Weber]

There's docs#Real.rpow_inv_natCast_pow that you can use with docs#le_of_pow_le_pow_left', which avoids done casts, but I don't think that this proof is inefficient

[Walter Moreira]

Thank you! At some point I used some combination of the theorems you mention, but I wasn't getting as short of a proof. After your comment, I'm kind of happy with this proof.

This lemma about moving the natural exponent across the inequality seems useful, and I couldn't find anything closer than the purely real version, with the search tools. Could it be a potential addition to Mathlib? (maybe somewhere in Mathlib.Analysis.SpecialFunctions.Pow.Real?)