have inj : inj f := by
  intro x y eq
  exact dense_inj (Nat.lt_of_lt_of_le x.isLt h) (Nat.lt_of_lt_of_le y.isLt h) eq
n : Nat
s : SparseSet n
i j : Fin n
h : n ≤ s.count
f : Fin n → Fin n := fun i => s.dense[i]
⊢ s.dense[s.sparse[j]] = j
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
⊢ s.dense[s.sparse[j]] = j