rfl
case refl.a
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
j : Nat
hge✝ : ¬k < f 0
hge : k ≥ f 0
hpos : 0 < sum (f ∘ succ)
hk' : k - f 0 < sum (f ∘ succ)
hi : ↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1 < n + 1
hj : j < f ⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1 + 1, hi⟩
h2 : (decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).snd ≅ ⟨j, hj⟩
⊢ (decodeSigma (f ∘ succ) ⟨k - f 0, hk'⟩).fst = ⟨⟨↑(decodeSigma (f ∘ succ) ⟨k - f 0, ⋯⟩).1, ⋯⟩, ⟨j, hj⟩⟩.fst
no goals