unfold SparseSet.insert at h
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : ¬i = j
⊢ i ∈ s
n : Nat
s : SparseSet n
i j : Fin n
h :
  i ∈
    if mem : j ∈ s then s
    else
      match s, mem 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 }
heq : ¬i = j
⊢ i ∈ s