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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬i ∈ s
⊢ (s.insert i).measure = s.measure - 1
Tactic:
simp at h
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.mem i = false
⊢ (s.insert i).measure = s.measure - 1

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.mem i = false
⊢ (s.insert i).measure = s.measure - 1
Tactic:
simp [measure, insert, h, Nat.sub_add_eq]
State after:
no goals