internlm/Lean-Github huggingface dataset:
Theorem: RegularProduction.eq_eps_from_isEps
Proof state before:
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
lhs✝ : { x // x ∈ V }
h : isEps (eps lhs✝)
⊢ eps lhs✝ = eps (lhs (eps lhs✝))
Tactic:
rfl
Proof state after:
no goals
Theorem: DFA.accepted_lang_eq
Proof state before:
α qs : Type
M : DFA α qs
⊢ AcceptedLanguage M = NFA.AcceptedLanguage (toNFA M)
Tactic:
unfold AcceptedLanguage
Proof state after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = NFA.AcceptedLanguage (toNFA M)
Theorem: DFA.accepted_lang_eq
Proof state before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = NFA.AcceptedLanguage (toNFA M)
Tactic:
unfold toNFA
Proof state after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) =
    NFA.AcceptedLanguage { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }
Theorem: DFA.accepted_lang_eq
Proof state before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) =
    NFA.AcceptedLanguage { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }
Tactic:
unfold NFA.AcceptedLanguage
Proof state after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w =>
    ∃ q₀ ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.Q₀,
      ∃ run, NFA.Run.last run ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.F
Theorem: DFA.accepted_lang_eq
Proof state before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w =>
    ∃ q₀ ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.Q₀,
      ∃ run, NFA.Run.last run ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.F
Tactic:
simp
Proof state after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w => ∃ run, NFA.Run.last run ∈ M.F
Theorem: DFA.accepted_lang_eq
Proof state before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w => ∃ run, NFA.Run.last run ∈ M.F
Tactic:
rfl
Proof state after:
no goals
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star_curried M w q = some (NFA.Run.last r)
Tactic:
cases r
Proof state after:
case final
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h✝ : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h✝))

case step
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r✝ : NFA.Run (toNFA M) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA M).δ (q, a✝)
h✝ : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q x✝ r✝ h✝))
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h))
Tactic:
case final h =>
  simp_rw [h, del_star_curried, NFA.Run.last]
Proof state after:
no goals
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q incl r' w_cast))
Tactic:
case step r' incl w_cast =>
  unfold NFA.Run.last
  rw [w_cast]
  unfold del_star_curried
  simp_rw [toNFA, Function.comp_apply] at incl
  rw [Option.mem_toFinset, Option.mem_iff] at incl
  rw [incl, Option.bind_eq_bind, Option.some_bind]
  apply last_state_eq_del_star_curried
Proof state after:
no goals
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h))
Tactic:
simp_rw [h, del_star_curried, NFA.Run.last]
Proof state after:
no goals
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q incl r' w_cast))
Tactic:
unfold NFA.Run.last
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last r')
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last r')
Tactic:
rw [w_cast]
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M (a✝ :: w✝) q = some (NFA.Run.last r')
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M (a✝ :: w✝) q = some (NFA.Run.last r')
Tactic:
unfold del_star_curried
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Tactic:
simp_rw [toNFA, Function.comp_apply] at incl
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ Option.toFinset (M.δ (q, a✝))
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : q₂✝ ∈ Option.toFinset (M.δ (q, a✝))
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Tactic:
rw [Option.mem_toFinset, Option.mem_iff] at incl
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')
Tactic:
rw [incl, Option.bind_eq_bind, Option.some_bind]
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w✝ q₂✝ = some (NFA.Run.last r')
Theorem: DFA.last_state_eq_del_star_curried
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r' : NFA.Run (toNFA M) q₂✝ w✝
incl : M.δ (q, a✝) = some q₂✝
w_cast : w = a✝ :: w✝
⊢ del_star_curried M w✝ q₂✝ = some (NFA.Run.last r')
Tactic:
apply last_state_eq_del_star_curried
Proof state after:
no goals
Theorem: DFA.last_state_eq_del_star
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star M (q, w) = some (NFA.Run.last r)
Tactic:
simp [del_star]
Proof state after:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star_curried M w q = some (NFA.Run.last r)
Theorem: DFA.last_state_eq_del_star
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star_curried M w q = some (NFA.Run.last r)
Tactic:
apply last_state_eq_del_star_curried
Proof state after:
no goals
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Tactic:
cases' hq': M.δ ⟨q, x⟩ with q'
Proof state after:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true

case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true

case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Tactic:
. simp [del_star_curried, hq', Option.bind_eq_bind]
  unfold constrRun
  rw [isNone_iff_eq_none, pbind_eq_none]
  assumption; intros; assumption
Proof state after:
case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Tactic:
. conv =>
    right; rw [isSome_iff_exists]; congr
    intro; unfold constrRun; rw [pbind_eq_some]
  constructor
  . intro h
    rw [del_star_curried, bind_eq_bind, hq', some_bind] at h
    have ⟨r', hr'⟩ := Option.isSome_iff_exists.mp $
      del_star_curried_isSome_iff_constrRun_isSome.mp h
    refine' .intro (.step _ _ r' rfl) ⟨q', hq', _⟩
    simp [toNFA]; assumption
    simp [bind_eq_bind]; assumption
  . intro ⟨r, q', HQ', h⟩
    simp [del_star_curried, bind_eq_bind, hq']
    apply del_star_curried_isSome_iff_constrRun_isSome.mpr
    rw [isSome_iff_exists]; simp [hq'] at HQ'; rw [HQ']
    simp [bind_eq_bind] at h; have ⟨r', _, _⟩ := h
    exists r'
Proof state after:
no goals
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Tactic:
simp [del_star_curried, hq', Option.bind_eq_bind]
Proof state after:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isNone (constrRun (x :: xs) q) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isNone (constrRun (x :: xs) q) = true
Tactic:
unfold constrRun
Proof state after:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isNone
      (Option.pbind (M.δ (q, x)) fun q' hq' => do
        let r' ← constrRun xs q'
        some (NFA.Run.step q ⋯ r' ⋯)) =
    true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isNone
      (Option.pbind (M.δ (q, x)) fun q' hq' => do
        let r' ← constrRun xs q'
        some (NFA.Run.step q ⋯ r' ⋯)) =
    true
Tactic:
rw [isNone_iff_eq_none, pbind_eq_none]
Proof state after:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ M.δ (q, x) = none

case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ ∀ (a : { x // x ∈ M.Q }) (H : a ∈ M.δ (q, x)),
    (do
          let r' ← constrRun xs a
          some (NFA.Run.step q ⋯ r' ⋯)) =
        none →
      M.δ (q, x) = none
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ M.δ (q, x) = none

case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ ∀ (a : { x // x ∈ M.Q }) (H : a ∈ M.δ (q, x)),
    (do
          let r' ← constrRun xs a
          some (NFA.Run.step q ⋯ r' ⋯)) =
        none →
      M.δ (q, x) = none
Tactic:
assumption
Proof state after:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ ∀ (a : { x // x ∈ M.Q }) (H : a ∈ M.δ (q, x)),
    (do
          let r' ← constrRun xs a
          some (NFA.Run.step q ⋯ r' ⋯)) =
        none →
      M.δ (q, x) = none
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ ∀ (a : { x // x ∈ M.Q }) (H : a ∈ M.δ (q, x)),
    (do
          let r' ← constrRun xs a
          some (NFA.Run.step q ⋯ r' ⋯)) =
        none →
      M.δ (q, x) = none
Tactic:
intros
Proof state after:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
a✝¹ : { x // x ∈ M.Q }
H✝ : a✝¹ ∈ M.δ (q, x)
a✝ :
  (do
      let r' ← constrRun xs a✝¹
      some (NFA.Run.step q ⋯ r' ⋯)) =
    none
⊢ M.δ (q, x) = none
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
a✝¹ : { x // x ∈ M.Q }
H✝ : a✝¹ ∈ M.δ (q, x)
a✝ :
  (do
      let r' ← constrRun xs a✝¹
      some (NFA.Run.step q ⋯ r' ⋯)) =
    none
⊢ M.δ (q, x) = none
Tactic:
assumption
Proof state after:
no goals
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
Tactic:
conv =>
  right; rw [isSome_iff_exists]; congr
  intro; unfold constrRun; rw [pbind_eq_some]
Proof state after:
case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔
    ∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔
    ∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1
Tactic:
constructor
Proof state after:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true →
    ∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1

case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ (∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1) →
    Option.isSome (del_star_curried M (x :: xs) q) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true →
    ∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1

case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ (∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1) →
    Option.isSome (del_star_curried M (x :: xs) q) = true
Tactic:
. intro h
  rw [del_star_curried, bind_eq_bind, hq', some_bind] at h
  have ⟨r', hr'⟩ := Option.isSome_iff_exists.mp $
    del_star_curried_isSome_iff_constrRun_isSome.mp h
  refine' .intro (.step _ _ r' rfl) ⟨q', hq', _⟩
  simp [toNFA]; assumption
  simp [bind_eq_bind]; assumption
Proof state after:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ (∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1) →
    Option.isSome (del_star_curried M (x :: xs) q) = true
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ (∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1) →
    Option.isSome (del_star_curried M (x :: xs) q) = true
Tactic:
. intro ⟨r, q', HQ', h⟩
  simp [del_star_curried, bind_eq_bind, hq']
  apply del_star_curried_isSome_iff_constrRun_isSome.mpr
  rw [isSome_iff_exists]; simp [hq'] at HQ'; rw [HQ']
  simp [bind_eq_bind] at h; have ⟨r', _, _⟩ := h
  exists r'
Proof state after:
no goals
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true →
    ∃ x_1 z,
      ∃ (H : z ∈ M.δ (q, x)),
        (do
            let r' ← constrRun xs z
            some (NFA.Run.step q ⋯ r' ⋯)) =
          some x_1
Tactic:
intro h
Proof state after:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M (x :: xs) q) = true
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M (x :: xs) q) = true
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1
Tactic:
rw [del_star_curried, bind_eq_bind, hq', some_bind] at h
Proof state after:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1
Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome
Proof state before:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1
Tactic:
have ⟨r', hr'⟩ := Option.isSome_iff_exists.mp $
  del_star_curried_isSome_iff_constrRun_isSome.mp h
Proof state after:
case some.mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
h : Option.isSome (del_star_curried M xs q') = true
r' : NFA.Run (toNFA M) q' xs
hr' : constrRun xs q' = some r'
⊢ ∃ x_1 z,
    ∃ (H : z ∈ M.δ (q, x)),
      (do
          let r' ← constrRun xs z
          some (NFA.Run.step q ⋯ r' ⋯)) =
        some x_1