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 α (RegExp.derivative a r)
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
apply Exists.elim a2_right
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = w
⊢ ∀ (a_1 : List α),
    a_1 ∈ RegExp.languageOf α s ∧ xs ++ a_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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = w
⊢ ∀ (a_1 : List α),
    a_1 ∈ RegExp.languageOf α s ∧ xs ++ a_1 = w →
      ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
intro ys a3
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = w
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = 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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = w
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
clear a2_right
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = 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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
cases a3
Proof state after:
case intro
α : 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 α (RegExp.derivative a r)
ys : List α
left✝ : ys ∈ RegExp.languageOf α s
right✝ : xs ++ ys = 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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
Tactic:
apply Exists.intro (a :: xs)
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, a :: xs ++ 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
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, a :: xs ++ s_1 = a :: 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ∈ RegExp.languageOf α 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ∃ s_1 ∈ RegExp.languageOf α s, a :: xs ++ s_1 = a :: 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ∈ RegExp.languageOf α r
Tactic:
simp only [← r_ih]
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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ xs ∈ 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ xs ∈ RegExp.languageOf α (RegExp.derivative a r)
Tactic:
exact a2_left
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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ∃ s_1 ∈ RegExp.languageOf α s, a :: xs ++ s_1 = a :: w
Tactic:
apply Exists.intro ys
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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ys ∈ RegExp.languageOf α s ∧ a :: xs ++ ys = a :: 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ys ∈ RegExp.languageOf α s ∧ a :: xs ++ ys = a :: w
Tactic:
constructor
Proof state after:
case right.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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ys ∈ RegExp.languageOf α s

case right.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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ++ ys = a :: w
Theorem: derivative_def
Proof state before:
case right.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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ ys ∈ RegExp.languageOf α s
Tactic:
exact a3_left
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
case right.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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ++ ys = a :: w
Tactic:
simp only [← a3_right]
Proof state after:
case right.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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ++ ys = a :: (xs ++ ys)
Theorem: derivative_def
Proof state before:
case right.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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α (RegExp.derivative a r)
ys : List α
a3_left : ys ∈ RegExp.languageOf α s
a3_right : xs ++ ys = w
⊢ a :: xs ++ ys = a :: (xs ++ ys)
Tactic:
simp
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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
intro a1
Proof state after:
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
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
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
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
apply Exists.elim a1
Proof state after:
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
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, a_1 ++ s_1 = a :: w) →
      ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
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
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, a_1 ++ s_1 = a :: w) →
      ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
intro xs a2
Proof state after:
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
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
xs : List α
a2 : xs ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
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
a1 : ∃ r_1 ∈ RegExp.languageOf α r, ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = a :: w
xs : List α
a2 : xs ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
clear a1
Proof state after:
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
xs : List α
a2 : xs ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
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
xs : List α
a2 : xs ∈ RegExp.languageOf α r ∧ ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
cases a2
Proof state after:
case mpr.intro
α : 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 α
left✝ : xs ∈ RegExp.languageOf α r
right✝ : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∃ 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
apply Exists.elim a2_right
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∀ (a_1 : List α),
    a_1 ∈ RegExp.languageOf α s ∧ xs ++ a_1 = a :: w →
      ∃ 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
⊢ ∀ (a_1 : List α),
    a_1 ∈ RegExp.languageOf α s ∧ xs ++ a_1 = a :: w →
      ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
intro ys a3
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = a :: w
⊢ ∃ 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
a2_right : ∃ s_1 ∈ RegExp.languageOf α s, xs ++ s_1 = a :: w
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
clear a2_right
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
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = a :: w
⊢ ∃ 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 : List α
c1 : r.is_nullable
xs : List α
a2_left : xs ∈ RegExp.languageOf α r
ys : List α
a3 : ys ∈ RegExp.languageOf α s ∧ xs ++ ys = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
Tactic:
cases a3
Proof state after:
case intro
α : 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 α
left✝ : ys ∈ RegExp.languageOf α s
right✝ : xs ++ ys = a :: w
⊢ ∃ r_1 ∈ RegExp.languageOf α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w