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

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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ n - s.count - 1 < n - s.count
Tactic:
apply Nat.sub_lt ?_ (by decide)
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ 0 < n - s.count

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ 0 < n - s.count
Tactic:
apply Nat.zero_lt_sub_of_lt (lt_of_mem i (by simp [h]))
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ 0 < 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : ¬s.mem i = true
⊢ ¬i ∈ s
Tactic:
simp [h]
State after:
no goals