lifting sub from Q to N?

Stream: Is there code for X?

[Ryan Lahfa]

I am running into a nasty coercion issue with the following MWE:

import data.rat.basic

example (a: ℕ) (b: ℕ) (s: ℕ) (h: a ^ s - b > 0):
  ↑(a ^ s - b) = (a: ℚ) ^ s - (b: ℚ) :=
begin
  admit,
end

Maybe I'm getting something arbitrary wrong, but I had the feeling I could lift to $\Z$ and then finish using int.coe_nat_sub as I had a proof that all of those are integers.

Maybe I could just lift to $\Z$ and prove it there and call it a day, but unsure how to actually do it, I tried many combinations of the zify tactic, lift tactic, manual coercions, norm_cast, push_cast, *_mod_cast variants without success.

Actually it seems like also there is no way to go from $\mathbb{Q}$ to $\N$ directly (can_lift Q N does not exist but I didn't really search diligently)

[Eric Wieser]

A similar example is:

example (a: ℕ) (b: ℕ) (s: ℕ) (h : b ≤ a ^ s):
  ↑(a ^ s - b) = (a: ℚ) ^ s - (b: ℚ) :=
begin
  rw nat.cast_sub h,
  simp,
end

[Eric Wieser]

Using > is only going to make things hard for you, because mathlib lemmas always use <

[Ryan Lahfa]

Indeed and it just works fine on my example (I also had < stuff in my equalities) :>

[Ryan Lahfa]

And I can just factor out the rw in the simp apparently, but I wonder if norm_cast is able to catch local hypothesis in the context and exploit them for this, as cast_sub seems to be marked for normalization of casts?

[Kevin Buzzard]

import tactic
import data.rat.basic

example (a: ℕ) (b: ℕ) (s: ℕ) (h: 0 < a ^ s - b):
  ↑(a ^ s - b) = (a: ℚ) ^ s - (b: ℚ) :=
begin
  rw nat.cast_sub,
  { norm_cast },
  { exact le_of_lt (nat.lt_of_sub_pos h) }
end