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

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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ↑s.sparse[↑j] < s.count ∧ s.dense[↑s.sparse[↑j]] = j
⊢ ∃ i, ↑i < s.count ∧ s.dense[i] = j
Tactic:
exists s.sparse[j]
State after:
no goals