Casting from N to R

Stream: new members

[Luke Mantle]

I've been working with some functions of the type ℕ → ℕ → ℝ and polynomial ℝ → ℕ → ℝ. In some lemmas, I end up with an equality between two long expressions, involving the ↑ symbol for casting. What should be a simple applicaiton of a few arithmetic lemmas, or even simp, suddenly doesn't work anymore, and I find myself using nat.cast_id and other similar lemmas for each little step. Is there a better way of dealing with this? Here's an example below, starting from an equality I might run into partway through a proof:

import analysis.special_functions.exp
example (f : ℕ → ℝ) (k : ℕ) :
f (2*k) - (4*↑k + 5) * f (2 * (k+1)) + (2*↑k + 3) * (2*↑k + 4) * f (2 * (k+2)) =
f (2*k) - (2 * ↑(2*k) + 5) * f (2*k + 2) + (↑(2*k) + 3) * (↑(2*k) + 4) * f (2*k + 4) := sorry

[Eric Wieser]

Does norm_cast help from there?

[Luke Mantle]

Eric Wieser said:

Does norm_cast help from there?

Yes, that helped, thanks! Either of norm_cast or norm_num, followed by ring, did the trick here.