simp [mem]
n : Nat
s : SparseSet n
i j : Fin n
m : ¬i ∈ s
⊢ i ∈
    match s, m 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 i;
      let sparse' := sparse.set ↑i ⋯ ⟨count, isLt⟩;
      let_fun sparse_dense' := ⋯;
      { count := count + 1, dense := dense', sparse := sparse', sparse_dense := sparse_dense', le_count := isLt }
no goals