Theorem: Regex.NFA.mem_εStep_iff_εClosure_sub (RegexCorrectness/NFA/Transition/Closure/Basic.lean)

State before:
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) ↔ ∀ i ∈ S, nfa.εClosure i ⊆ S
Tactic:
apply Iff.intro
State after:
case mp
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S

case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S

State before:
case mp
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S

case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
. intro assm i mem
  intro k cls
  induction cls with
  | base => exact mem
  | @step i j k step _ ih =>
    cases Nat.decLt i nfa.nodes.size with
    | isTrue lt =>
      simp [εStep, lt] at step
      exact ih (assm i mem lt j step)
    | isFalse nlt => simp [εStep, nlt] at step
State after:
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S

State before:
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
. intro assm i mem _ j step
  apply Set.mem_of_mem_of_subset _ (assm i mem)
  exact εClosure.step (εStep_of_εStep step) .base
State after:
no goals

State before:
case mp
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S
Tactic:
intro assm i mem
State after:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
⊢ nfa.εClosure i ⊆ S

State before:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
⊢ nfa.εClosure i ⊆ S
Tactic:
intro k cls
State after:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
k : ℕ
cls : k ∈ nfa.εClosure i
⊢ k ∈ S

State before:
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
k : ℕ
cls : k ∈ nfa.εClosure i
⊢ k ∈ S
Tactic:
induction cls with
| base => exact mem
| @step i j k step _ ih =>
  cases Nat.decLt i nfa.nodes.size with
  | isTrue lt =>
    simp [εStep, lt] at step
    exact ih (assm i mem lt j step)
  | isFalse nlt => simp [εStep, nlt] at step
State after:
no goals

State before:
case mp.base
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i k i✝ : ℕ
mem : i✝ ∈ S
⊢ i✝ ∈ S
Tactic:
exact mem
State after:
no goals

State before:
case mp.step
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
⊢ k ∈ S
Tactic:
cases Nat.decLt i nfa.nodes.size with
| isTrue lt =>
  simp [εStep, lt] at step
  exact ih (assm i mem lt j step)
| isFalse nlt => simp [εStep, nlt] at step
State after:
no goals

State before:
case mp.step.isTrue
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
lt : i < nfa.nodes.size
⊢ k ∈ S
Tactic:
simp [εStep, lt] at step
State after:
case mp.step.isTrue
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ k ∈ S

State before:
case mp.step.isTrue
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
lt : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ k ∈ S
Tactic:
exact ih (assm i mem lt j step)
State after:
no goals

State before:
case mp.step.isFalse
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i✝ k✝ i j k : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k
ih : j ∈ S → k ∈ S
mem : i ∈ S
nlt : ¬i < nfa.nodes.size
⊢ k ∈ S
Tactic:
simp [εStep, nlt] at step
State after:
no goals

State before:
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
Tactic:
intro assm i mem _ j step
State after:
case mpr
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ S

State before:
case mpr
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ S
Tactic:
apply Set.mem_of_mem_of_subset _ (assm i mem)
State after:
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εClosure i

State before:
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εClosure i
Tactic:
exact εClosure.step (εStep_of_εStep step) .base
State after:
no goals