rw [Nat.add_sub_cancel_left]
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)
i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j < f ⟨i + 1, hi⟩
hpos : 0 < sum (f ∘ succ)
hk : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < sum f
hge✝ : ¬f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) < f 0
hge : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) ≥ f 0
hk' : f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0 < sum (f ∘ succ)
⊢ ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) = f 0 + ↑(encodeSigma (f ∘ succ) ⟨⟨i, ⋯⟩, ⟨j, hj⟩⟩) - f 0
no goals