apply Fin.eq
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)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩ = x ⟨i.succ, hi⟩
case a
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)
x✝ : Fin (n + 1)
i : Nat
hi : i + 1 < n + 1
k : Nat
hk : k < prod f
h : ⟨f 0 * ↑(encodePi (f ∘ succ) fun x_1 => x ⟨↑x_1 + 1, ⋯⟩) + ↑(x 0), ⋯⟩ = ⟨k, hk⟩
⊢ ↑(decodePi (f ∘ succ) ⟨↑⟨k, hk⟩ / f 0, ⋯⟩ ⟨i, ⋯⟩) = ↑(x ⟨i.succ, hi⟩)