Limit of partially defined functions

Stream: Is there code for X?

[Peter Nelson]

Say I define a limiting sequence in terms of a sequence of partially defined n-tuples as follows:

def limitOf {β : Type*} (fs : (n : ℕ) → Fin n → β) (i : ℕ) : β := fs (i+1) (Fin.last i)

Then I should be able to prove the following, saying that my limit function agrees with the input sequence provided I have some local consistency hypothesis.

import Mathlib.Tactic

def limitOf {β : Type*} (fs : (n : ℕ) → Fin n → β) (i : ℕ) : β := fs (i+1) (Fin.last i)

lemma limitOf_consistent {β : Type*} {fs : (n : ℕ) → Fin n → β}
    (hfs : ∀ (m : ℕ) (i : Fin m), fs m i = fs (m+1) (Fin.castSucc i)) {n : ℕ} (i : Fin n) :
    limitOf fs i = fs n i := by
  sorry

(Provided I haven't overlooked something) this isn't too hard to prove, but I find myself reinventing this particular wheel in a few different contexts where I am defining some sort of infinite limit of a sequence of 'nested' finite objects. Is there machinery for this already in mathlib somewhere?