simplify a `Fin` constant

Stream: general

[Jeremy Avigad]

Is there a generic way to simplify an expression like ↑3, where 3 : Fin 10, to 3? For example, I'd like a way of using ring in the example below without having to get rid of the cast manually.

import Mathlib.Tactic.Ring

theorem foo : @Fin.val 10 3 = 3 := rfl

example (x : ℕ) : x + @Fin.val 10 3 = 3 + x := by rw [foo]; ring

-- fails
example (x : ℕ) : x + @Fin.val 10 3 = 3 + x := by simp; ring

[Eric Wieser]

docs#Fin.coe_ofNat_eq_mod is a lemma you can use to make progress without foo

[Eric Wieser]

We could consider tagging it norm_cast

[Jeremy Avigad]

Yup, that's exactly what I needed. Thanks!