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

State before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
⊢ i = j
Tactic:
have : s.sparse[s.dense[i]] = s.sparse[s.dense[j]] := by rw [eq]
State after:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : s.sparse[s.dense[i]] = s.sparse[s.dense[j]]
⊢ i = j

State before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : s.sparse[s.dense[i]] = s.sparse[s.dense[j]]
⊢ i = j
Tactic:
simp [s.sparse_dense i hi, s.sparse_dense j hj] at this
State after:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : i = j
⊢ i = j

State before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
this : i = j
⊢ i = j
Tactic:
exact this
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
hi : ↑i < s.count
hj : ↑j < s.count
eq : s.dense[i] = s.dense[j]
⊢ s.sparse[s.dense[i]] = s.sparse[s.dense[j]]
Tactic:
rw [eq]
State after:
no goals