have := m.left
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
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