congr 1
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩, (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd⟩ =
    ⟨⟨i + 1, hi⟩, ⟨j, hj⟩⟩
case h.e_3.h
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, ⋯⟩ = ⟨i + 1, hi⟩

case h.e_4
n : Nat
ih : ∀ (f : Fin n → Nat) (k : Fin (sum f)) (x : (i : Fin n) × Fin (f i)), decodeSigma f k = x ↔ encodeSigma f x = k
f : Fin (n + 1) → Nat
k✝ : Fin (sum f)
x : (i : Fin (n + 1)) × Fin (f i)
k : Nat
hk : k < sum f
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
h : ⟨f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩), ⋯⟩ = ⟨k, hk⟩
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
this : decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩ = ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩