Inline type hints

Stream: Is there code for X?

[Chase Norman]

I'm having trouble proving the statement ↑a ≤ ↑b - ↑c → a ≤ b where a, b and c are natural numbers and they are lifted to integers. I cannot even create a lemma which states this fact because lean understandably does not know what type to lift to. How can I provide a type hint to this effect? Alternatively, if there was a way to remove lifts from a hypothesis ("unzify") that would be helpful to proceed. Any ideas?

[Alex J. Best]

To make the lemma you can explicitly cast like this

example (a b c : ℕ) : (a : ℤ) ≤ (b : ℤ) - (c : ℤ) → a ≤ b := sorry

[Heather Macbeth]

And you can solve it by explicitly invoking the fact that 0 ≤ c:

import tactic

example (a b c : ℕ) (h : (a:ℤ) ≤ b - c) : a ≤ b :=
begin
  have : (0:ℤ) ≤ c := int.coe_zero_le c,
  linarith,
end

[Alex J. Best]

unzify would be tactic#lift I think, there is also tactic#norm_cast which is very useful in this sort of situation.