Theorem: Regex.NFA.pathIn.castLE (RegexCorrectness/NFA/Transition/Path/Basic.lean)

State before:
cs : List Char
nfa : NFA
start start' i i' : ℕ
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
path : nfa.pathIn start i i' cs
⊢ nfa.pathIn start' i i' cs
Tactic:
induction path with
| base _ => exact .base assm
| @step i j k cs cs' step rest ih =>
  have h₂ := step.h₂
  have : start' ≤ j := by
    cases step with
    | charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
    | εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
  exact .step (step.castStart' assm) (ih this)
State after:
no goals

State before:
case base
cs : List Char
nfa : NFA
start start' i i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i✝ : ℕ
h✝ : start ≤ i✝
assm : start' ≤ i✝
⊢ nfa.pathIn start' i✝ i✝ []
Tactic:
exact .base assm
State after:
no goals

State before:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
⊢ nfa.pathIn start' i k (cs ++ cs')
Tactic:
have h₂ := step.h₂
State after:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ nfa.pathIn start' i k (cs ++ cs')

State before:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ nfa.pathIn start' i k (cs ++ cs')
Tactic:
have : start' ≤ j := by
  cases step with
  | charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
  | εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
State after:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
this : start' ≤ j
⊢ nfa.pathIn start' i k (cs ++ cs')

State before:
case step
cs✝ : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
this : start' ≤ j
⊢ nfa.pathIn start' i k (cs ++ cs')
Tactic:
exact .step (step.castStart' assm) (ih this)
State after:
no goals

State before:
cs✝ : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn start i j cs
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
⊢ start' ≤ j
Tactic:
cases step with
| charStep _ _ step => exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
| εStep _ _ step => exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
State after:
no goals

State before:
case charStep
cs : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs' : List Char
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ start' ≤ j
Tactic:
exact inBounds i j assm h₂ (.inl ⟨_, step⟩) (le_of_pathIn_left rest)
State after:
no goals

State before:
case εStep
cs : List Char
nfa : NFA
start start' i✝ i' : ℕ
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
i j k : ℕ
cs' : List Char
rest : nfa.pathIn start j k cs'
ih : start' ≤ j → nfa.pathIn start' j k cs'
assm : start' ≤ i
h₂ : i < nfa.nodes.size
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ start' ≤ j
Tactic:
exact inBounds i j assm h₂ (.inr step) (le_of_pathIn_left rest)
State after:
no goals