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
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s
no goals