Theorem: Regex.Data.SparseSet.mem_insert_of_mem (RegexCorrectness/Data/SparseSet.lean)

State before:
n : Nat
s : SparseSet n
i j : Fin n
⊢ i ∈ s → i ∈ s.insert j
Tactic:
intro h
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
⊢ i ∈ s.insert j

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

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

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

State before:
case inl
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : j ∈ s
⊢ i ∈ s

case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ 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 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 }
Tactic:
next => exact h
State after:
case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ 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 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 }

State before:
case inr
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
h✝ : ¬j ∈ 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 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 }
Tactic:
next hmem =>
  simp [mem, Vec.get_set]
  if heq : j.val = i.val then
    simp [heq]
    exact Fin.eq_of_val_eq heq
  else
    simp [mem] at h
    simp [heq]
    have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
    simp [this, h]
    exact Nat.lt_trans h.left (Nat.lt_succ_self _)
State after:
no goals

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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ 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 }
Tactic:
simp [mem, Vec.get_set]
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
if heq : j.val = i.val then
  simp [heq]
  exact Fin.eq_of_val_eq heq
else
  simp [mem] at h
  simp [heq]
  have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
  simp [this, h]
  exact Nat.lt_trans h.left (Nat.lt_succ_self _)
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
simp [heq]
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ j = i

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ↑j = ↑i
⊢ j = i
Tactic:
exact Fin.eq_of_val_eq heq
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
simp [mem] at h
State after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i

State before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) < s.count + 1 ∧
    (if s.count = ↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i]) then j
      else s.dense[↑(if ↑j = ↑i then ⟨s.count, ⋯⟩ else s.sparse[↑i])]) =
      i
Tactic:
simp [heq]
State after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i

State before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
Tactic:
have : s.count ≠ s.sparse[i.val].val := Nat.ne_of_gt h.left
State after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i

State before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1 ∧ (if s.count = ↑s.sparse[↑i] then j else s.dense[↑s.sparse[↑i]]) = i
Tactic:
simp [this, h]
State after:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1

State before:
n : Nat
s : SparseSet n
i j : Fin n
hmem : ¬j ∈ s
heq : ¬↑j = ↑i
h : ↑s.sparse[↑i] < s.count ∧ s.dense[↑s.sparse[↑i]] = i
this : s.count ≠ ↑s.sparse[↑i]
⊢ ↑s.sparse[↑i] < s.count + 1
Tactic:
exact Nat.lt_trans h.left (Nat.lt_succ_self _)
State after:
no goals