Theorem: DFA.del_star_curried_isSome_iff_constrRun_isSome (FormalSystems/Chomsky/Regular/DFA.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
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
Tactic:
refine' .intro (.step _ _ r' rfl) ⟨q', hq', _⟩
State after:
case some.mp.refine'_1
α 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'
⊢ q' ∈ (toNFA M).δ (q, x)

case some.mp.refine'_2
α 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'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ?some.mp.refine'_1 r' ⋯)

State before:
case some.mp.refine'_1
α 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'
⊢ q' ∈ (toNFA M).δ (q, x)

case some.mp.refine'_2
α 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'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ?some.mp.refine'_1 r' ⋯)
Tactic:
simp [toNFA]
State after:
case some.mp.refine'_1
α 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'
⊢ M.δ (q, x) = some q'

case some.mp.refine'_2
α 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'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)

State before:
case some.mp.refine'_1
α 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'
⊢ M.δ (q, x) = some q'

case some.mp.refine'_2
α 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'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
Tactic:
assumption
State after:
case some.mp.refine'_2
α 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'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)

State before:
case some.mp.refine'_2
α 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'
⊢ (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some (NFA.Run.step q ⋯ r' ⋯)
Tactic:
simp [bind_eq_bind]
State after:
case some.mp.refine'_2
α 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'
⊢ constrRun xs q' = some r'

State before:
case some.mp.refine'_2
α 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'
⊢ constrRun xs q' = some r'
Tactic:
assumption
State after:
no goals

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⟩
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true
Tactic:
simp [del_star_curried, bind_eq_bind, hq']
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M xs q'✝) = true

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (del_star_curried M xs q'✝) = true
Tactic:
apply del_star_curried_isSome_iff_constrRun_isSome.mpr
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (constrRun xs q'✝) = true

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ Option.isSome (constrRun xs q'✝) = true
Tactic:
rw [isSome_iff_exists]
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ ∃ a, constrRun xs q'✝ = some a

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ' : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
⊢ ∃ a, constrRun xs q'✝ = some a
Tactic:
simp [hq'] at HQ'
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q'✝ = some a

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q'✝ = some a
Tactic:
rw [HQ']
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q' = some a

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
h :
  (do
      let r' ← constrRun xs q'
      some (NFA.Run.step q ⋯ r' ⋯)) =
    some r
HQ' : q'✝ = q'
⊢ ∃ a, constrRun xs q' = some a
Tactic:
simp [bind_eq_bind] at h
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
⊢ ∃ a, constrRun xs q' = some a

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
Tactic:
have ⟨r', _, _⟩ := h
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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
r' : NFA.Run (toNFA M) q' xs
left✝ : constrRun xs q' = some r'
right✝ : NFA.Run.step q ⋯ r' ⋯ = r
⊢ ∃ a, constrRun xs q' = some a

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'✝
r : NFA.Run (toNFA M) q (x :: xs)
q' : { x // x ∈ M.Q }
HQ'✝ : q' ∈ M.δ (q, x)
HQ' : q'✝ = q'
h : ∃ a, constrRun xs q' = some a ∧ NFA.Run.step q ⋯ a ⋯ = r
r' : NFA.Run (toNFA M) q' xs
left✝ : constrRun xs q' = some r'
right✝ : NFA.Run.step q ⋯ r' ⋯ = r
⊢ ∃ a, constrRun xs q' = some a
Tactic:
exists r'
State after:
no goals