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

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.isEmpty = true
⊢ ¬i ∈ s
Tactic:
intro m
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.isEmpty = true
m : i ∈ s
⊢ False

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.isEmpty = true
m : i ∈ s
⊢ False
Tactic:
simp [isEmpty] at h
State after:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
h : s.count = 0
⊢ False

State before:
n : Nat
s : SparseSet n
i j : Fin n
m : i ∈ s
h : s.count = 0
⊢ False
Tactic:
simp [mem, h] at m
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ False

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
⊢ False
Tactic:
have := m.left
State after:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < 0
⊢ False

State before:
n : Nat
s : SparseSet n
i j : Fin n
h : s.count = 0
m : ↑s.sparse[↑i] < 0 ∧ s.dense[↑s.sparse[↑i]] = i
this : ↑s.sparse[↑i] < 0
⊢ False
Tactic:
contradiction
State after:
no goals