cases heq
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
i✝ : Nat
hi : i✝ < m + 1
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
heq : ⟨i✝, hi⟩ = ⟨i.succ, hi✝⟩
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i✝, hi⟩
case refl
n m : Nat
ih : ∀ (k : Fin (n ^ m)) (x : Fin m → Fin n), k.decodeFun = x ↔ encodeFun x = k
k✝ : Fin (n ^ (m + 1))
x : Fin (m + 1) → Fin n
ih1 : (encodeFun fun k => x k.succ).decodeFun = fun k => x k.succ
k : Nat
hk : k < n ^ (m + 1)
hnpos : n > 0
h : n * ↑(encodeFun fun k => x k.succ) + ↑(x 0) = k
x✝ : Fin (m + 1)
i : Nat
hi✝ : i + 1 < m + 1
hi : i.succ < m + 1
⊢ ⟨k / n, ⋯⟩.decodeFun ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩