An `nify` tactic?

Stream: Is there code for X?

[Terence Tao]

I recently had need of the following lemma regarding subsets of Fin (N+1):

import Mathlib

example (N : ℕ) (n: Fin N) : (Finset.Iio n.succ).erase n.castSucc = Finset.Iio n.castSucc := by
      rw [<-Finset.map_inj (f := Fin.valEmbedding)]
      simp only [Fin.map_valEmbedding_Iio, Fin.coe_castSucc, Finset.map_erase, Fin.val_succ]
      exact Finset.Iic_erase _

Perhaps one could add this lemma to Mathlib, but that's not my main concern here (I imagine this particular lemma might only have a niche use). I was wondering instead if it is worth developing some general nify tactic (similar to rify, zify, or qify, that converts statements concerning elements (as well as sets and Finsets) in Fin types into equivalent statements regarding their analogues in ℕ; in the example above, this hypothetical tactic would basically automatically perform the first two lines of the given proof. I'm not sure if this would be widely useful though. (I needed it because I chose to work with various sums over Fin N, which I was using to index a finite sequence of objects. It's possible that I could have avoided some technicalities by indexing over a more general Finset instead, but the Fin API was reasonably adequate for my purposes, except for missing the above lemma. My initial attempt to prove the lemma from first principles was absolutely disgusting; it was only after realizing that one should map everything through Fin.valEmbedding that the above short proof became apparent. So I was wondering whether one could formalize this general strategy as a tactic.)

EDIT: okay, it turns out for my example that actually the conversions were unnecessary, so maybe the suggestion is not a good one...

import Mathlib

lemma Iio_of_succ_eq_Iic_of_castSucc {N : ℕ} (n: Fin N) : Finset.Iio n.succ = Finset.Iic n.castSucc := rfl

example {N : ℕ} (n: Fin N) : (Finset.Iio n.succ).erase n.castSucc = Finset.Iio n.castSucc := by
      rw [Iio_of_succ_eq_Iic_of_castSucc n] -- this line seems necessary despite being proven by `rfl`
      exact Finset.Iic_erase _

It can also be golfed to a one-line proof:

import Mathlib

example {N : ℕ} (n: Fin N) : (Finset.Iio n.succ).erase n.castSucc = Finset.Iio n.castSucc := by
      convert Finset.Iic_erase n.castSucc using 1

[Kyle Miller]

My first reaction is that this would make sense to have, though it would be good to figure out what nify should be expected to do. With zify and qify, the main obstructions they work with are (1) turning nat subtraction into int subtraction and (2) turning int division into rational division. What hypotheses could nify work with to turn Fin operations into Nat operations? I suppose it could the obvious ones, for example if a * b < n then you can "nify" the *.