## Stream: Is there code for X?

### Topic: Inline type hints

#### Chase Norman (Nov 15 2020 at 00:56):

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 (Nov 15 2020 at 01:02):

To make the lemma you can explicitly cast like this

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


#### Heather Macbeth (Nov 15 2020 at 01:03):

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 (Nov 15 2020 at 01:03):

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

Last updated: May 16 2021 at 05:21 UTC