internlm/Lean-Github huggingface dataset:
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
simp only [is_nullable_def] at c1
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
apply Exists.intro (a :: w)
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ a :: w ∈ RegExp.languageOf α (RegExp.derivative a r) ∧ ∃ s_1 ∈ RegExp.languageOf α s, a :: w ++ s_1 = w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ a :: w ∈ RegExp.languageOf α (RegExp.derivative a r) ∧ ∃ s_1 ∈ RegExp.languageOf α s, a :: w ++ s_1 = w
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ a :: w ∈ RegExp.languageOf α (RegExp.derivative a r)

case right
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ ∃ s_1 ∈ RegExp.languageOf α s, a :: w ++ s_1 = w
Theorem: derivative_def
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ a :: w ∈ RegExp.languageOf α (RegExp.derivative a r)
Tactic:
simp only [← a3_right]
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ xs ++ ys ∈ RegExp.languageOf α (RegExp.derivative a r)
Theorem: derivative_def
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ xs ++ ys ∈ RegExp.languageOf α (RegExp.derivative a r)
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ ∃ s_1 ∈ RegExp.languageOf α s, a :: w ++ s_1 = w
Tactic:
apply Exists.intro []
Proof state after:
case right
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ [] ∈ RegExp.languageOf α s ∧ a :: w ++ [] = w
Theorem: derivative_def
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = a :: w
c1 : [] ∈ RegExp.languageOf α r
⊢ [] ∈ RegExp.languageOf α s ∧ a :: w ++ [] = w
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ w ∈ RegExp.languageOf α (r.delta.concat (RegExp.derivative a s)) ↔ a :: w ∈ RegExp.languageOf α (r.concat s)
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ w ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = x} ↔
    a :: w ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ w ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = x} ↔
    a :: w ∈ {x | ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = x}
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ (∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w) ↔
    ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ (∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w) ↔
    ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ (∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w) →
    ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w

case mpr
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ (∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w) →
    ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ (∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w) →
    ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
intro a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
apply Exists.elim a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α r.delta ∧ ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), a_1 ++ s_1 = w) →
      ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α r.delta ∧ ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), a_1 ++ s_1 = w) →
      ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
intro xs a2
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
xs : List α
a2 : xs ∈ RegExp.languageOf α r.delta ∧ ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), xs ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
a1 : ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
xs : List α
a2 : xs ∈ RegExp.languageOf α r.delta ∧ ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), xs ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
clear a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
xs : List α
a2 : xs ∈ RegExp.languageOf α r.delta ∧ ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), xs ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
xs : List α
a2 : xs ∈ RegExp.languageOf α r.delta ∧ ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), xs ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
r_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
c1 : ¬r.is_nullable
⊢ (∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w) →
    ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α (RegExp.derivative a s), r_1 ++ s_1 = w
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e.closure) ↔ a :: w ∈ RegExp.languageOf α e.closure
Tactic:
simp only [RegExp.derivative]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈ RegExp.languageOf α ((RegExp.derivative a e).concat e.closure) ↔ a :: w ∈ RegExp.languageOf α e.closure
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈ RegExp.languageOf α ((RegExp.derivative a e).concat e.closure) ↔ a :: w ∈ RegExp.languageOf α e.closure
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈
      {x |
        ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e),
          ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x} ↔
    a :: w ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ w ∈
      {x |
        ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e),
          ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x} ↔
    a :: w ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w) ↔
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w) ↔
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w) →
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w

case mpr
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w) →
    ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
Theorem: derivative_def
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w) →
    ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
Tactic:
sorry
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
⊢ (∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w) →
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
intro a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
apply Exists.elim a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α (RegExp.derivative a e) ∧
        ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ a_1 ++ a.join = w) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α (RegExp.derivative a e) ∧
        ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ a_1 ++ a.join = w) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
intro xs a2
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a e) ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Theorem: derivative_def
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w : List α
a1 : ∃ r ∈ RegExp.languageOf α (RegExp.derivative a e), ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ r ++ a.join = w
xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a e) ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
clear a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a e) ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w