simp [f, ←eq, s.sparse_dense i (Nat.lt_of_lt_of_le i.isLt h)]
n : Nat
s : SparseSet n
i✝ j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
inj : Regex.Data.SparseSet.Bijection.inj f
surj : Regex.Data.SparseSet.Bijection.surj f
i : Fin n
eq : f i = j
⊢ s.dense[s.sparse[j]] = j
no goals