if heq : i = j then
  exact Or.inl heq
else
  suffices i ∈ s from Or.inr this
  unfold SparseSet.insert at h
  split at h
  next => exact h
  next hmem =>
    have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
    simp [mem, Vec.get_set, ne] at h
    split at h
    case inl heq' => simp [h] at heq
    case inr heq' =>
      have : s.sparse[i.val] < s.count := by
        have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
        exact Nat.lt_of_le_of_ne this (Ne.symm heq')
      simp [mem, this, h]
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
⊢ i = j ∨ i ∈ s
no goals