internlm/Lean-Github huggingface dataset:
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ ↑self✝ ∧ { val := ↑q, property := ?final.right.w } ∈ M.F

case final.right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ↑q ∈ M.Q
Tactic:
constructor
Proof state after:
case final.right.h.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ ↑self✝

case final.right.h.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ M.F

case final.right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ↑q ∈ M.Q
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right.h.left.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ?final.right.h.left.s₁ ⊆ ↑self✝

case final.right.h.left.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ ?final.right.h.left.s₁

case final.right.h.left.s₁
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ Finset { x // x ∈ M.Q }

case final.right.h.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ M.F

case final.right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ↑q ∈ M.Q
Tactic:
repeat { assumption }
Proof state after:
no goals
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right.h.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ⋯ } ∈ M.F
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.step a✝² x✝ r✝ h✝) h') ∈ (fromNFA M).F
Tactic:
dsimp [RunFromRestricted, NFA.Run.last]
Proof state after:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted r✝ ⋯) ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted r✝ ⋯) ∈ (fromNFA M).F
Tactic:
apply RunFromRestricted_final
Proof state after:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last r✝ ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step a✝² x✝ r✝ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last r✝ ∈ (fromNFA M).F
Tactic:
dsimp [NFA.Run.last] at h
Proof state after:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
⊢ NFA.Run.last r✝ ∈ (fromNFA M).F
Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝² : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝² ⊆ ↑self✝
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA (fromNFA M)).δ (a✝², a✝)
h✝ : a✝¹ = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
⊢ NFA.Run.last r✝ ∈ (fromNFA M).F
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
r : NFA.Run M q w
h : NFA.Run.last r ∈ M.F
⊢ NFA.Run.last (NFARunToRun r) ∈ (fromNFA M).F
Tactic:
cases r
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ (fromNFA M).F

case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ (fromNFA M).F

case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Tactic:
. dsimp [fromNFA]
  apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id); simp
  constructor
  dsimp [Finset.univ]
  apply Fintype.complete
  exists q; simp
  dsimp [NFA.Run.last] at h
  simp [NFARunToRun, NFA.Run.last]
  assumption
Proof state after:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Tactic:
. dsimp [NFARunToRun, NFA.Run.last]
  apply RunFromRestricted_final
  apply NFARunToRun_final_imp_final
  dsimp [NFA.Run.last] at h
  assumption
Proof state after:
no goals
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ (fromNFA M).F
Tactic:
dsimp [fromNFA]
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈
    Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈
    Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
Tactic:
apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id)
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ id
    (NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
      ∃ q_1 ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))), q_1 ∈ M.F)
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ id
    (NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
      ∃ q_1 ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))), q_1 ∈ M.F)
Tactic:
simp
Proof state after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
    ∃ a,
      ∃ (b : a ∈ M.Q),
        { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
          { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
    ∃ a,
      ∃ (b : a ∈ M.Q),
        { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
          { val := a, property := b } ∈ M.F
Tactic:
constructor
Proof state after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Tactic:
dsimp [Finset.univ]
Proof state after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Fintype.elems

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Fintype.elems

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Tactic:
apply Fintype.complete
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Tactic:
exists q
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ (b : ↑q ∈ M.Q),
    { val := ↑q, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
      { val := ↑q, property := b } ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ (b : ↑q ∈ M.Q),
    { val := ↑q, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
      { val := ↑q, property := b } ∈ M.F
Tactic:
simp
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F
Tactic:
dsimp [NFA.Run.last] at h
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F
Tactic:
simp [NFARunToRun, NFA.Run.last]
Proof state after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ M.F
Theorem: DFA.fromNFA.NFARunToRun_final_imp_final
Proof state before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ M.F
Tactic:
assumption
Proof state after:
no goals