simp [mem, Vec.get_set, ne] at h
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
h :
  i ∈
    match s, hmem with
    | { count := count, dense := dense, sparse := sparse, sparse_dense := sparse_dense, le_count := le_count }, mem =>
      let_fun isLt := ⋯;
      let dense' := dense.set count isLt j;
      let sparse' := sparse.set ↑j ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
ne : ↑j ≠ ↑i
⊢ i ∈ s
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
h : ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
⊢ i ∈ s