have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
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 }
⊢ i ∈ s
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