Theorem: Regex.NFA.lt_of_inBounds_of_charStep (RegexCorrectness/NFA/Basic.lean)

State before:
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem : j ∈ node.charStep c
⊢ j < k
Tactic:
unfold Node.charStep at mem
State after:
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.char c' next => if (c == c') = true then {next} else ∅
    | Node.sparse cs next => if c ∈ cs then {next} else ∅
    | x => ∅
⊢ j < k

State before:
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.char c' next => if (c == c') = true then {next} else ∅
    | Node.sparse cs next => if c ∈ cs then {next} else ∅
    | x => ∅
⊢ j < k
Tactic:
split at mem <;> try simp [Node.inBounds] at *
State after:
case h_1
j k : ℕ
c : Char
n✝ : Node
c'✝ : Char
next✝ : ℕ
inBounds : next✝ < k
mem : c = c'✝ ∧ j = next✝
⊢ j < k

case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k

State before:
case h_1
j k : ℕ
c : Char
n✝ : Node
c'✝ : Char
next✝ : ℕ
inBounds : next✝ < k
mem : c = c'✝ ∧ j = next✝
⊢ j < k

case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
Tactic:
simp [*]
State after:
case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k

State before:
case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k
Tactic:
cases mem
State after:
case h_2.intro
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
left✝ : c ∈ cs✝
right✝ : j = next✝
⊢ j < k

State before:
case h_2.intro
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
left✝ : c ∈ cs✝
right✝ : j = next✝
⊢ j < k
Tactic:
simp [*]
State after:
no goals

State before:
case h_3
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
n✝ : Node
x✝¹ : ∀ (c' : Char) (next : ℕ), node = Node.char c' next → False
x✝ : ∀ (cs : Data.Classes) (next : ℕ), node = Node.sparse cs next → False
mem : j ∈ ∅
⊢ j < k
Tactic:
simp [Node.inBounds] at *
State after:
no goals