Theorem: derivative_def (FOL/Parsing/Brzozowski.lean)

State before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
e : RegExp α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
Tactic:
induction e generalizing w
State after:
case char
α : Type
inst✝ : DecidableEq α
a a✝ : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (RegExp.char a✝)) ↔ a :: w ∈ RegExp.languageOf α (RegExp.char a✝)

case epsilon
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.epsilon) ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon

case zero
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a RegExp.zero) ↔ a :: w ∈ RegExp.languageOf α RegExp.zero

case union
α : Type
inst✝ : DecidableEq α
a : α
a✝¹ a✝ : RegExp α
a_ih✝¹ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝¹) ↔ a :: w ∈ RegExp.languageOf α a✝¹
a_ih✝ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝) ↔ a :: w ∈ RegExp.languageOf α a✝
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (a✝¹.union a✝)) ↔ a :: w ∈ RegExp.languageOf α (a✝¹.union a✝)

case concat
α : Type
inst✝ : DecidableEq α
a : α
a✝¹ a✝ : RegExp α
a_ih✝¹ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝¹) ↔ a :: w ∈ RegExp.languageOf α a✝¹
a_ih✝ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝) ↔ a :: w ∈ RegExp.languageOf α a✝
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a (a✝¹.concat a✝)) ↔ a :: w ∈ RegExp.languageOf α (a✝¹.concat a✝)

case closure
α : Type
inst✝ : DecidableEq α
a : α
a✝ : RegExp α
a_ih✝ : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a a✝) ↔ a :: w ∈ RegExp.languageOf α a✝
w : List α
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a a✝.closure) ↔ a :: w ∈ RegExp.languageOf α a✝.closure

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

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

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

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

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

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

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

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

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]
State after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ RegExp.languageOf α RegExp.epsilon ↔ b :: w ∈ RegExp.languageOf α (RegExp.char b)

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]
State after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ {[]} ↔ b :: w ∈ {[b]}

State before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : a = b
⊢ w ∈ {[]} ↔ b :: w ∈ {[b]}
Tactic:
simp
State after:
no goals

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]
State after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ ∅ ↔ a :: w ∈ {[b]}

State before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ w ∈ ∅ ↔ a :: w ∈ {[b]}
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ a = b → ¬w = []

State before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
⊢ a = b → ¬w = []
Tactic:
intro a1
State after:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
a1 : a = b
⊢ ¬w = []

State before:
α : Type
inst✝ : DecidableEq α
a b : α
w : List α
c1 : ¬a = b
a1 : a = b
⊢ ¬w = []
Tactic:
contradiction
State after:
no goals

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]
State after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon

State before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.epsilon
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ {[]}

State before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ {[]}
Tactic:
simp
State after:
no goals

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]
State after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.zero

State before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ RegExp.languageOf α RegExp.zero ↔ a :: w ∈ RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
State after:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ ∅

State before:
α : Type
inst✝ : DecidableEq α
a : α
w : List α
⊢ w ∈ ∅ ↔ a :: w ∈ ∅
Tactic:
simp
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 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:
cases a2
State after:
case mp.intro
α : Type
inst✝ : DecidableEq α
a : α
e : RegExp α
ih : ∀ (w : List α), w ∈ RegExp.languageOf α (RegExp.derivative a e) ↔ a :: w ∈ RegExp.languageOf α e
w xs : List α
left✝ : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
right✝ : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
case _ a2_left a2_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    apply Exists.intro [(a :: w)]
    simp
    simp only [← ih]
    sorry
State after:
no goals

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
apply Exists.elim a2_right
State after:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∀ (a_1 : List (List α)),
    (∀ r ∈ a_1, r ∈ RegExp.languageOf α e) ∧ xs ++ a_1.join = w →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
⊢ ∀ (a_1 : List (List α)),
    (∀ r ∈ a_1, r ∈ RegExp.languageOf α e) ∧ xs ++ a_1.join = w →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
intro ys a3
State after:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α e) ∧ xs ++ a.join = w
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
clear a2_right
State after:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α e) ∧ xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
cases a3
State after:
case intro
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
left✝ : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
right✝ : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
case _ a3_left a3_right =>
  apply Exists.intro [(a :: w)]
  simp
  simp only [← ih]
  sorry
State after:
no goals

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = a :: w
Tactic:
apply Exists.intro [(a :: w)]
State after:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ (∀ r ∈ [a :: w], r ∈ RegExp.languageOf α e) ∧ [a :: w].join = a :: w

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ (∀ r ∈ [a :: w], r ∈ RegExp.languageOf α e) ∧ [a :: w].join = a :: w
Tactic:
simp
State after:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ a :: w ∈ RegExp.languageOf α e

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ a :: w ∈ RegExp.languageOf α e
Tactic:
simp only [← ih]
State after:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e)

State before:
α : 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_left : xs ∈ RegExp.languageOf α (RegExp.derivative a e)
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α e
a3_right : xs ++ ys.join = w
⊢ w ∈ RegExp.languageOf α (RegExp.derivative a e)
Tactic:
sorry
State after:
no goals