Theorem: Regex.VM.εClosure_subset_lower_inv (RegexCorrectness/VM/Auxiliary.lean)

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
let S := { j | ∃ isLt : j < nfa.nodes.size, ⟨j, isLt⟩ ∈ next }
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have : ∀ i ∈ S, (_ : i < nfa.nodes.size) → ∀ j ∈ nfa[i].εStep, j ∈ S := by
  intro i hi iLt j hj
  have ⟨_, hi⟩ := hi
  have jLt : j < nfa.nodes.size := lt_of_εStep hj
  have hj : j ∈ nfa.εStep i := by
    simp [εStep, iLt, hj]
  have := inv ⟨i, iLt⟩ ⟨j, jLt⟩ hi hj
  simp at this
  refine ⟨jLt, this⟩
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have := mem_εStep_iff_εClosure_sub.mp this
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
intro i hi j hj
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have : nfa.εClosure i ⊆ S := this i ⟨i.isLt, hi⟩
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝¹ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this : nfa.εClosure ↑i ⊆ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝¹ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this : nfa.εClosure ↑i ⊆ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
have : j ∈ S := this hj
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝² : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝¹ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this✝ : nfa.εClosure ↑i ⊆ S
this : j ∈ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝² : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this✝¹ : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this✝ : nfa.εClosure ↑i ⊆ S
this : j ∈ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
Tactic:
exact this
State after:
no goals

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
intro i hi iLt j hj
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
⊢ j ∈ S

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
⊢ j ∈ S
Tactic:
have ⟨_, hi⟩ := hi
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
⊢ j ∈ S

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
⊢ j ∈ S
Tactic:
have jLt : j < nfa.nodes.size := lt_of_εStep hj
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
⊢ j ∈ S

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
⊢ j ∈ S
Tactic:
have hj : j ∈ nfa.εStep i := by
  simp [εStep, iLt, hj]
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
⊢ j ∈ S

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
⊢ j ∈ S
Tactic:
have := inv ⟨i, iLt⟩ ⟨j, jLt⟩ hi hj
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : ⟨j, jLt⟩ ∈ next ∨ StackEntry.explore ⟨j, jLt⟩ ∈ #[]
⊢ j ∈ S

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : ⟨j, jLt⟩ ∈ next ∨ StackEntry.explore ⟨j, jLt⟩ ∈ #[]
⊢ j ∈ S
Tactic:
simp at this
State after:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : next.mem ⟨j, jLt⟩ = true
⊢ j ∈ S

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : next.mem ⟨j, jLt⟩ = true
⊢ j ∈ S
Tactic:
refine ⟨jLt, this⟩
State after:
no goals

State before:
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
⊢ j ∈ nfa.εStep i
Tactic:
simp [εStep, iLt, hj]
State after:
no goals