if heq : j.val = i.val then
  simp [heq]
  exact Fin.eq_of_val_eq heq
else
  simp [mem] at h
  simp [heq]
  have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
  simp [this, h]
  exact Nat.lt_trans h.left (Nat.lt_succ_self _)
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ ↑(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
no goals