α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ NFA.evalFrom (toNFA M) {start} s = {evalFrom M start s}
change List.foldl M.toNFA.stepSet {start} s = {List.foldl M.step start s}
case nil
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} [] = {List.foldl M.step start []}

case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} (a :: s) = {List.foldl M.step start (a :: s)}
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start : σ
s : List α
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
induction' s with a s ih generalizing start
no goals
case nil
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} [] = {List.foldl M.step start []}
tauto
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {step M start a} s = {List.foldl M.step (step M start a) s}
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {start} (a :: s) = {List.foldl M.step start (a :: s)}
rw [List.foldl, List.foldl,
  show M.toNFA.stepSet {start} a = {M.step start a} by simp [NFA.stepSet] ]
no goals
case cons
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ List.foldl (NFA.stepSet (toNFA M)) {step M start a} s = {List.foldl M.step (step M start a) s}
tauto
no goals
α : Type u
σ σ' : Type v
M✝ : NFA α σ
M : DFA α σ
start✝ : σ
a : α
s : List α
ih : ∀ (start : σ), List.foldl (NFA.stepSet (toNFA M)) {start} s = {List.foldl M.step start s}
start : σ
⊢ NFA.stepSet (toNFA M) {start} a = {step M start a}
simp [NFA.stepSet]