## Stream: new members

### Topic: Lifting results

#### Eric Astor (Feb 15 2021 at 05:10):

I'm not sure how to lift results across a cast. For example, if I have n : ℕ and want to establish the goal 0 ≤ (n : ℝ), how can I prove it? I know zero_le n : 0 ≤ n, but I'm not sure how to establish this 0 ≤ ↑n.

#### Damiano Testa (Feb 15 2021 at 05:26):

There are a lot of norm_num type results that can do this. In this case, norm_num works, but is a little slow, and library_search also works.

lemma nat_to_real_nonneg {n : ℕ} : (0 : ℝ) ≤ n :=
begin
--library_search finds this
exact nat.cast_nonneg n,
end


#### Johan Commelin (Feb 15 2021 at 05:40):

Another useful lemma is norm_cast. It will try to remove as many \u up-arrows as it can.

#### Mario Carneiro (Feb 15 2021 at 05:46):

I don't think norm_num knows anything about this, you are probably seeing the result of simp

#### Mario Carneiro (Feb 15 2021 at 05:47):

but this sort of thing is generally norm_cast's job

Last updated: May 13 2021 at 06:15 UTC