internlm/Lean-Github huggingface dataset:
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (RegExp.char b)) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
case char b =>
  simp only [RegExp.derivative]
  split_ifs
  case pos c1 =>
    simp only [c1]
    simp only [RegExp.languageOf]
    simp
  case neg c1 =>
    simp only [RegExp.languageOf]
    simp
    intro a1
    contradiction
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.epsilon) ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
case epsilon =>
  simp only [RegExp.derivative]
  simp only [RegExp.languageOf]
  simp
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α RegExp.zero
Tactic:
case zero =>
  simp only [RegExp.derivative]
  simp only [RegExp.languageOf]
  simp
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 α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (r.union s)) ↔ a :: w ∈ RegExp.languageOf α (r.union s)
Tactic:
case union r s r_ih s_ih =>
  simp only [RegExp.derivative]
  simp only [RegExp.languageOf]
  specialize r_ih w
  specialize s_ih w
  simp
  tauto
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (RegExp.char b)) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
simp only [RegExp.derivative]
Proof state after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (if a = b then RegExp.epsilon else RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
⊢ w ∈ RegExp.languageOf α (if a = b then RegExp.epsilon else RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
split_ifs
Proof state after:
case pos
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
h✝ : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)

case neg
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
h✝ : ¬a = b
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
case pos c1 =>
  simp only [c1]
  simp only [RegExp.languageOf]
  simp
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
case neg c1 =>
  simp only [RegExp.languageOf]
  simp
  intro a1
  contradiction
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
simp only [c1]
Proof state after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ b :: w ∈ RegExp.languageOf α (RegExp.char b)
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ b :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ {[]} ↔ b :: w ∈ {[b]}
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ {[]} ↔ b :: w ∈ {[b]}
Tactic:
simp
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α (RegExp.char b)
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ ∅ ↔ a :: w ∈ {[b]}
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ ∅ ↔ a :: w ∈ {[b]}
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ a = b → ¬w = []
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ a = b → ¬w = []
Tactic:
intro a1
Proof state after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
a1 : a = b
⊢ ¬w = []
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
a1 : a = b
⊢ ¬w = []
Tactic:
contradiction
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.epsilon) ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
simp only [RegExp.derivative]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ {[]}
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ {[]}
Tactic:
simp
Proof state after:
no goals
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.derivative]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.zero
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ ∅
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ ∅
Tactic:
simp
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 α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (r.union s)) ↔ a :: w ∈ RegExp.languageOf α (r.union s)
Tactic:
simp only [RegExp.derivative]
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 α
⊢ w ∈ RegExp.languageOf α ((RegExp.derivative a r).union (RegExp.derivative a s)) ↔
    a :: w ∈ RegExp.languageOf α (r.union s)
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 α
⊢ w ∈ RegExp.languageOf α ((RegExp.derivative a r).union (RegExp.derivative a s)) ↔
    a :: w ∈ RegExp.languageOf α (r.union 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 α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∪ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
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 α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∪ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
specialize r_ih w
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
r_ih : w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∪ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
s_ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
w : List α
r_ih : w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∪ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
specialize s_ih w
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
w : List α
r_ih : w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∪ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
w : List α
r_ih : w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∪ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∪ RegExp.languageOf α s
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
w : List α
r_ih : w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∨ w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∨ a :: w ∈ RegExp.languageOf α s
Theorem: derivative_def
Proof state before:
α : Type
inst✝ : DecidableEq α
a : α
r s : RegExp α
w : List α
r_ih : w ∈ RegExp.languageOf α (RegExp.derivative a r) ↔ a :: w ∈ RegExp.languageOf α r
s_ih : w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔ a :: w ∈ RegExp.languageOf α s
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a r) ∨ w ∈ RegExp.languageOf α (RegExp.derivative a s) ↔
    a :: w ∈ RegExp.languageOf α r ∨ a :: w ∈ RegExp.languageOf α s
Tactic:
tauto
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 α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (r.concat s)) ↔ a :: w ∈ RegExp.languageOf α (r.concat s)
Tactic:
simp only [RegExp.derivative]
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 α
⊢ w ∈
      RegExp.languageOf α
        (if r.is_nullable then (RegExp.derivative a r).concat s else r.delta.concat (RegExp.derivative a s)) ↔
    a :: w ∈ RegExp.languageOf α (r.concat s)
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 α
⊢ w ∈
      RegExp.languageOf α
        (if r.is_nullable then (RegExp.derivative a r).concat s else r.delta.concat (RegExp.derivative a s)) ↔
    a :: w ∈ RegExp.languageOf α (r.concat s)
Tactic:
split_ifs
Proof state after:
case pos
α : 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 α
h✝ : r.is_nullable
⊢ w ∈ RegExp.languageOf α ((RegExp.derivative a r).concat s) ↔ a :: w ∈ RegExp.languageOf α (r.concat s)

case neg
α : 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 α
h✝ : ¬r.is_nullable
⊢ w ∈ RegExp.languageOf α (r.delta.concat (RegExp.derivative a s)) ↔ a :: w ∈ RegExp.languageOf α (r.concat s)
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 α ((RegExp.derivative a r).concat 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α (RegExp.derivative a r) ∧ ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
⊢ ∀ (a_1 : List α),
    (a_1 ∈ RegExp.languageOf α (RegExp.derivative a r) ∧ ∃ s_1 ∈ RegExp.languageOf α 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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a r) ∧ ∃ 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
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 α (RegExp.derivative a r), ∃ s_1 ∈ RegExp.languageOf α s, r_1 ++ s_1 = w
xs : List α
a2 : xs ∈ RegExp.languageOf α (RegExp.derivative a r) ∧ ∃ 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:
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 α (RegExp.derivative a r) ∧ ∃ 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
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 α (RegExp.derivative a r) ∧ ∃ 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:
cases a2
Proof state after:
case mp.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 α (RegExp.derivative a r)
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