split
case succ.mpr.h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
i : Fin (n + 1)
⊢ (match i with
    | ⟨0, isLt⟩ => ⟨↑k % f 0, ⋯⟩
    | ⟨i.succ, hi⟩ => decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i, ⋯⟩) =
    x i
case succ.mpr.h.h_1
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
isLt✝ : 0 < n + 1
⊢ ⟨↑k % f 0, ⋯⟩ = x ⟨0, isLt✝⟩

case succ.mpr.h.h_2
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (prod f)) (x : (i : Fin n) → Fin (f i)), decodePi f k = x ↔ encodePi f x = k
f : Fin (n + 1) → Nat
k : Fin (prod f)
x : (i : Fin (n + 1)) → Fin (f i)
h : encodePi f x = k
x✝ : Fin (n + 1)
i✝ : Nat
hi✝ : i✝ + 1 < n + 1
⊢ decodePi (f ∘ succ) ⟨↑k / f 0, ⋯⟩ ⟨i✝, ⋯⟩ = x ⟨i✝.succ, hi✝⟩