Lifting results

Stream: new members

[Eric Astor]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

but this sort of thing is generally norm_cast's job