simp [this, h]
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this✝ : s[i] = s.dense[i]
this : s.sparse[↑s.dense[i]] = ⟨i, isLt⟩
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]
no goals