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

State before:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
⊢ s[i] ∈ s
Tactic:
have isLt : i < n := Nat.lt_of_lt_of_le h s.le_count
State after:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
⊢ s[i] ∈ s

State before:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
⊢ s[i] ∈ s
Tactic:
have : s[i] = s.dense[i] := rfl
State after:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this : s[i] = s.dense[i]
⊢ s[i] ∈ s

State before:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this : s[i] = s.dense[i]
⊢ s[i] ∈ s
Tactic:
simp [mem, this]
State after:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this : s[i] = s.dense[i]
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]

State before:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this : s[i] = s.dense[i]
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]
Tactic:
have := s.sparse_dense ⟨i, isLt⟩ h
State after:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this✝ : s[i] = s.dense[i]
this : s.sparse[↑s.dense[↑⟨i, isLt⟩]] = ⟨i, isLt⟩
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]

State before:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this✝ : s[i] = s.dense[i]
this : s.sparse[↑s.dense[↑⟨i, isLt⟩]] = ⟨i, isLt⟩
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]
Tactic:
simp at this
State after:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this✝ : s[i] = s.dense[i]
this : s.sparse[↑s.dense[i]] = ⟨i, isLt⟩
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]

State before:
n : Nat
s : SparseSet n
i : Nat
h : i < s.count
isLt : i < n
this✝ : s[i] = s.dense[i]
this : s.sparse[↑s.dense[i]] = ⟨i, isLt⟩
⊢ ↑s.sparse[↑s.dense[i]] < s.count ∧ s.dense[↑s.sparse[↑s.dense[i]]] = s.dense[i]
Tactic:
simp [this, h]
State after:
no goals