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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ↑i < s.count
⊢ s.dense[i] ∈ s
Tactic:
simp [mem, sparse_dense, h]
State after:
no goals