Theorem: Regex.NFA.lt_of_inBounds_of_εStep (RegexCorrectness/NFA/Basic.lean)

State before:
node : Node
j k : ℕ
inBounds : node.inBounds k
mem : j ∈ node.εStep
⊢ j < k
Tactic:
unfold Node.εStep at mem
State after:
node : Node
j k : ℕ
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.epsilon next => {next}
    | Node.split next₁ next₂ => {next₁, next₂}
    | Node.save offset next => {next}
    | x => ∅
⊢ j < k

State before:
node : Node
j k : ℕ
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.epsilon next => {next}
    | Node.split next₁ next₂ => {next₁, next₂}
    | Node.save offset next => {next}
    | x => ∅
⊢ j < k
Tactic:
split at mem <;>
  try simp [Node.inBounds] at * <;>
  try cases mem <;>
  simp [*]
State after:
no goals

State before:
case h_4
node : Node
j k : ℕ
inBounds : node.inBounds k
n✝ : Node
x✝² : ∀ (next : ℕ), node = Node.epsilon next → False
x✝¹ : ∀ (next₁ next₂ : ℕ), node = Node.split next₁ next₂ → False
x✝ : ∀ (offset next : ℕ), node = Node.save offset next → False
mem : j ∈ ∅
⊢ j < k
Tactic:
simp [Node.inBounds] at * <;>
try cases mem <;>
simp [*]
State after:
no goals

State before:
case h_3
j k : ℕ
n✝ : Node
offset✝ next✝ : ℕ
inBounds : next✝ < k
mem : j = next✝
⊢ j < k
Tactic:
cases mem <;>
simp [*]
State after:
no goals