next => rfl
case mp.a.left.e_a.h_1
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 : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
isLt✝ : 0 < m + 1
heq✝ : 0 = ⟨0, isLt✝⟩
⊢ ↑⟨k % n, ⋯⟩ = k % n

case mp.a.left.e_a.h_2
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 : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n
case mp.a.left.e_a.h_2
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 : ⟨k, hk⟩.decodeFun = x
x✝ : Fin (m + 1)
i✝ : Nat
hi✝ : i✝ + 1 < m + 1
heq✝ : 0 = ⟨i✝.succ, hi✝⟩
⊢ ↑(⟨k / n, ⋯⟩.decodeFun ⟨i✝, ⋯⟩) = k % n