Theorem: DFA.fromNFA.RunFromRestricted_final (FormalSystems/Chomsky/Regular/PowersetConstruction.lean)

State before:
α 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 }
r : Run (fromNFA M) a✝¹ a✝
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h : NFA.Run.last r ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted r h') ∈ (fromNFA M).F
Tactic:
cases r
State after:
case final
α 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 : NFA.Run.last (NFA.Run.final a✝¹ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F

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

State before:
case final
α 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 : NFA.Run.last (NFA.Run.final a✝¹ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F

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 [NFA.Run.last, fromNFA] at h
  rw [Finset.mem_filter] at h
  dsimp [RunFromRestricted, NFA.Run.last, fromNFA]
  apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id); simp
  constructor
  rw [Finset.attach_eq_univ]; dsimp [Finset.univ]
  apply Fintype.complete
  have ⟨_, q, _, _⟩ := h
  exists q; constructor; constructor
  apply Finset.mem_of_subset
  repeat { assumption }
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 (NFA.Run.step a✝² x✝ r✝ h✝) h') ∈ (fromNFA M).F

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]
  apply RunFromRestricted_final
  dsimp [NFA.Run.last] at h
  assumption
State after:
no goals

State before:
case final
α 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 : NFA.Run.last (NFA.Run.final a✝¹ h✝) ∈ (fromNFA M).F
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Tactic:
dsimp [NFA.Run.last, fromNFA] at h
State after:
case final
α 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.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F

State before:
case final
α 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.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Tactic:
rw [Finset.mem_filter] at h
State after:
case final
α 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
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F

State before:
case final
α 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
⊢ NFA.Run.last (RunFromRestricted (NFA.Run.final a✝¹ h✝) h') ∈ (fromNFA M).F
Tactic:
dsimp [RunFromRestricted, NFA.Run.last, fromNFA]
State after:
case final
α 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
⊢ self✝ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)

State before:
case final
α 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
⊢ self✝ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
Tactic:
apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id)
State after:
case final
α 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
⊢ id (self✝ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑self✝, q ∈ M.F)

State before:
case final
α 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
⊢ id (self✝ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑self✝, q ∈ M.F)
Tactic:
simp
State after:
case final
α 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
⊢ self✝ ∈ Finset.attach Finset.univ ∧
    ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F

State before:
case final
α 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
⊢ self✝ ∈ Finset.attach Finset.univ ∧
    ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
constructor
State after:
case final.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
⊢ self✝ ∈ Finset.attach Finset.univ

case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F

State before:
case final.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
⊢ self✝ ∈ Finset.attach Finset.univ

case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
rw [Finset.attach_eq_univ]
State after:
case final.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
⊢ self✝ ∈ Finset.univ

case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F

State before:
case final.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
⊢ self✝ ∈ Finset.univ

case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
dsimp [Finset.univ]
State after:
case final.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
⊢ self✝ ∈ Finset.attach Fintype.elems

case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F

State before:
case final.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
⊢ self✝ ∈ Finset.attach Fintype.elems

case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
apply Fintype.complete
State after:
case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F

State before:
case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
have ⟨_, q, _, _⟩ := h
State after:
case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F

State before:
case final.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
⊢ ∃ a, ∃ (b : a ∈ M.Q), { val := a, property := b } ∈ ↑self✝ ∧ { val := a, property := b } ∈ M.F
Tactic:
exists q
State after:
case final.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
⊢ ∃ (b : ↑q ∈ M.Q), { val := ↑q, property := b } ∈ ↑self✝ ∧ { val := ↑q, property := b } ∈ M.F

State before:
case final.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
⊢ ∃ (b : ↑q ∈ M.Q), { val := ↑q, property := b } ∈ ↑self✝ ∧ { val := ↑q, property := b } ∈ M.F
Tactic:
constructor
State after:
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

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
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

State before:
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
Tactic:
apply Finset.mem_of_subset
State after:
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

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 }
State after:
no goals

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
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals