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

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

State before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
⊢ s.count < n
Tactic:
by_contra nlt
State after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
⊢ False

State before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
⊢ False
Tactic:
have ge := Nat.le_of_not_lt nlt
State after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ False

State before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ False
Tactic:
apply h (Nat.lt_of_lt_of_le s.sparse[i].isLt ge)
State after:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ s.dense[↑s.sparse[↑i]] = i

State before:
n : Nat
s : SparseSet n
i✝ j i : Fin n
h : ↑s.sparse[↑i] < s.count → ¬s.dense[↑s.sparse[↑i]] = i
nlt : ¬s.count < n
ge : n ≤ s.count
⊢ s.dense[↑s.sparse[↑i]] = i
Tactic:
exact dense_sparse_of_full ge
State after:
no goals