simp [heq]
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ j = i