Theorem: totalDFA_lang_eq (FormalSystems/Chomsky/Regular/TotalDFA.lean)

State before:
α qs : Type
M : DFA α qs
⊢ DFA.AcceptedLanguage M = DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
apply Set.ext
State after:
case h
α qs : Type
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ M.Z }), x ∈ DFA.AcceptedLanguage M ↔ x ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA

State before:
case h
α qs : Type
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ M.Z }), x ∈ DFA.AcceptedLanguage M ↔ x ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
intro w
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ DFA.AcceptedLanguage M ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
rw [DFA.in_language_iff_del_star_final]
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
let w': Word M.toTotalDFA.Z := w
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
have w_cast : w = w' := rfl
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
Tactic:
rw [w_cast, TotalDFA.in_language_iff_del_star_final]
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ((DFA.toTotalDFA M).q₀, w') ∈ (DFA.toTotalDFA M).F

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ((DFA.toTotalDFA M).q₀, w') ∈ (DFA.toTotalDFA M).F
Tactic:
conv =>
  right; congr;
  right; simp [DFA.toTotalDFA]; rfl
  simp [DFA.toTotalDFA]
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w') ∈
      Finset.map { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } M.F

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w') ∈
      Finset.map { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } M.F
Tactic:
rw [Finset.mem_map]
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ a ∈ M.F,
      { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } a =
        TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w')

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ a ∈ M.F,
      { toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } a =
        TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some M.q₀, property := ⋯ }, w')
Tactic:
conv =>
  right; congr; intro;
  simp [Subtype.eq_iff, <-totalDFA_del_star_eq];
  rw [And.comm];
State after:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ x, ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

State before:
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w'), qf ∈ M.F) ↔
    ∃ x, ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
constructor <;> intro ⟨x, l, r⟩ <;> exists x
State after:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

State before:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
. simp [r, Option.mem_iff.mp l]; rfl
State after:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F

State before:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
. simp [l, r]; exact l.symm
State after:
no goals

State before:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
simp [r, Option.mem_iff.mp l]
State after:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = some x

State before:
case h.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : x ∈ DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = some x
Tactic:
rfl
State after:
no goals

State before:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
Tactic:
simp [l, r]
State after:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ DFA.del_star M (M.q₀, w') = some x

State before:
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ DFA.del_star M (M.q₀, w') = some x
Tactic:
exact l.symm
State after:
no goals