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

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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
⊢ i = j ∨ i ∈ s
Tactic:
if heq : i = j then
  exact Or.inl heq
else
  suffices i ∈ s from Or.inr this
  unfold SparseSet.insert at h
  split at h
  next => exact h
  next hmem =>
    have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
    simp [mem, Vec.get_set, ne] at h
    split at h
    case inl heq' => simp [h] at heq
    case inr heq' =>
      have : s.sparse[i.val] < s.count := by
        have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
        exact Nat.lt_of_le_of_ne this (Ne.symm heq')
      simp [mem, this, h]
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : i = j
⊢ i = j ∨ i ∈ s
Tactic:
exact Or.inl heq
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : ¬i = j
⊢ i = j ∨ i ∈ s
Tactic:
suffices i ∈ s from Or.inr this
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : i ∈ s.insert j
heq : ¬i = j
⊢ i ∈ s

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

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

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

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

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

State before:
case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
h✝ : ¬j ∈ s
h :
  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 }
⊢ i ∈ s
Tactic:
next hmem =>
  have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
  simp [mem, Vec.get_set, ne] at h
  split at h
  case inl heq' => simp [h] at heq
  case inr heq' =>
    have : s.sparse[i.val] < s.count := by
      have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
      exact Nat.lt_of_le_of_ne this (Ne.symm heq')
    simp [mem, this, h]
State after:
no goals

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

State before:
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
Tactic:
have ne : j.val ≠ i.val := Ne.symm (Fin.val_ne_of_ne heq)
State after:
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

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

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

case inr
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
h✝ : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ j = i
⊢ i ∈ s
Tactic:
case inl heq' => simp [h] at heq
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s
Tactic:
case inr heq' =>
  have : s.sparse[i.val] < s.count := by
    have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
    exact Nat.lt_of_le_of_ne this (Ne.symm heq')
  simp [mem, this, h]
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ j = i
⊢ i ∈ s
Tactic:
simp [h] at heq
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ i ∈ s
Tactic:
have : s.sparse[i.val] < s.count := by
  have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
  exact Nat.lt_of_le_of_ne this (Ne.symm heq')
State after:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < s.count
⊢ i ∈ s

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < s.count
⊢ i ∈ s
Tactic:
simp [mem, this, h]
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ ↑s.sparse[↑i] < s.count
Tactic:
have : s.sparse[i.val] ≤ s.count := Nat.le_of_lt_succ h.left
State after:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] ≤ s.count
⊢ ↑s.sparse[↑i] < s.count

State before:
n : Nat
s : SparseSet n
i j : Fin n
heq : ¬i = j
hmem : ¬j ∈ s
ne : ↑j ≠ ↑i
heq' : ¬s.count = ↑s.sparse[↑i]
h : ↑s.sparse[↑i] < s.count + 1 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] ≤ s.count
⊢ ↑s.sparse[↑i] < s.count
Tactic:
exact Nat.lt_of_le_of_ne this (Ne.symm heq')
State after:
no goals