Theorem: Regex.Data.SparseSet.mem_insert (Regex/Data/SparseSet/Basic.lean)

State before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈ s.insert i
Tactic:
unfold insert
State after:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈
    if mem : i ∈ 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 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 }

State before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈
    if mem : i ∈ 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 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 }
Tactic:
split
State after:
case inl
n : Nat
s : SparseSet n
i j : Fin n
h✝ : i ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
h✝ : ¬i ∈ s
⊢ i ∈
    match s, h✝ 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 }

State before:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
⊢ i ∈ s
Tactic:
case inl m => exact m
State after:
no goals

State before:
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 }
Tactic:
case inr m => simp [mem]
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
⊢ i ∈ s
Tactic:
exact m
State after:
no goals

State before:
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 }
Tactic:
simp [mem]
State after:
no goals