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

State before:
n : Nat
i : Fin n
s : SparseSet n
⊢ s ⊆ s.insert i
Tactic:
intro j hj
State after:
n : Nat
i : Fin n
s : SparseSet n
j : Fin n
hj : j ∈ s
⊢ j ∈ s.insert i

State before:
n : Nat
i : Fin n
s : SparseSet n
j : Fin n
hj : j ∈ s
⊢ j ∈ s.insert i
Tactic:
exact mem_insert_of_mem hj
State after:
no goals