Theorem: equiv_language_of_closure (FOL/Parsing/RegExp.lean)

State before:
α : Type
R : RegExp α
⊢ RegExp.languageOf α R.closure = RegExp.languageOf α (RegExp.epsilon.union (R.concat R.closure))
Tactic:
ext cs
State after:
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ RegExp.languageOf α R.closure ↔ cs ∈ RegExp.languageOf α (RegExp.epsilon.union (R.concat R.closure))

State before:
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ RegExp.languageOf α R.closure ↔ cs ∈ RegExp.languageOf α (RegExp.epsilon.union (R.concat R.closure))
Tactic:
simp only [RegExp.languageOf]
State after:
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = l} ↔
    cs ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α R,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = l}, r ++ s = x}

State before:
case h
α : Type
R : RegExp α
cs : List α
⊢ cs ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = l} ↔
    cs ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α R,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = l}, r ++ s = x}
Tactic:
simp
State after:
case h
α : Type
R : RegExp α
cs : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs) ↔
    cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

State before:
case h
α : Type
R : RegExp α
cs : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs) ↔
    cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
constructor
State after:
case h.mp
α : Type
R : RegExp α
cs : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs) →
    cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

case h.mpr
α : Type
R : RegExp α
cs : List α
⊢ (cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs) →
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
case h.mp
α : Type
R : RegExp α
cs : List α
⊢ (∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs) →
    cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
intro a1
State after:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

State before:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
apply Exists.elim a1
State after:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ a.join = cs →
      cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

State before:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ a.join = cs →
      cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
intro xs a2
State after:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

State before:
case h.mp
α : Type
R : RegExp α
cs : List α
a1 : ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
clear a1
State after:
case h.mp
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

State before:
case h.mp
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2 : (∀ r ∈ xs, r ∈ RegExp.languageOf α R) ∧ xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
cases a2
State after:
case h.mp.intro
α : Type
R : RegExp α
cs : List α
xs : List (List α)
left✝ : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
right✝ : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs

State before:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
case _ a2_left a2_right =>
  simp only [← a2_right]
  cases xs
  case nil =>
    left
    simp
  case cons hd tl =>
    right
    simp at a2_left
    cases a2_left
    case _ a2_left_left a2_left_right =>
      apply Exists.intro hd
      tauto
State after:
no goals

State before:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
Tactic:
simp only [← a2_right]
State after:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ xs.join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = xs.join

State before:
α : Type
R : RegExp α
cs : List α
xs : List (List α)
a2_left : ∀ r ∈ xs, r ∈ RegExp.languageOf α R
a2_right : xs.join = cs
⊢ xs.join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = xs.join
Tactic:
cases xs
State after:
case nil
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join

case cons
α : Type
R : RegExp α
cs head✝ : List α
tail✝ : List (List α)
a2_left : ∀ r ∈ head✝ :: tail✝, r ∈ RegExp.languageOf α R
a2_right : (head✝ :: tail✝).join = cs
⊢ (head✝ :: tail✝).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (head✝ :: tail✝).join

State before:
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join
Tactic:
case nil =>
  left
  simp
State after:
no goals

State before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ (hd :: tl).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
case cons hd tl =>
  right
  simp at a2_left
  cases a2_left
  case _ a2_left_left a2_left_right =>
    apply Exists.intro hd
    tauto
State after:
no goals

State before:
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = [].join
Tactic:
left
State after:
case h
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = []

State before:
case h
α : Type
R : RegExp α
cs : List α
a2_left : ∀ r ∈ [], r ∈ RegExp.languageOf α R
a2_right : [].join = cs
⊢ [].join = []
Tactic:
simp
State after:
no goals

State before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ (hd :: tl).join = [] ∨
    ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
right
State after:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join

State before:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_left : ∀ r ∈ hd :: tl, r ∈ RegExp.languageOf α R
a2_right : (hd :: tl).join = cs
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
simp at a2_left
State after:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left : hd ∈ RegExp.languageOf α R ∧ ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join

State before:
case h
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left : hd ∈ RegExp.languageOf α R ∧ ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
cases a2_left
State after:
case h.intro
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
left✝ : hd ∈ RegExp.languageOf α R
right✝ : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join

State before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
case _ a2_left_left a2_left_right =>
  apply Exists.intro hd
  tauto
State after:
no goals

State before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = (hd :: tl).join
Tactic:
apply Exists.intro hd
State after:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ hd ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ hd ++ a.join = (hd :: tl).join

State before:
α : Type
R : RegExp α
cs hd : List α
tl : List (List α)
a2_right : (hd :: tl).join = cs
a2_left_left : hd ∈ RegExp.languageOf α R
a2_left_right : ∀ a ∈ tl, a ∈ RegExp.languageOf α R
⊢ hd ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ hd ++ a.join = (hd :: tl).join
Tactic:
tauto
State after:
no goals

State before:
case h.mpr
α : Type
R : RegExp α
cs : List α
⊢ (cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs) →
    ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
intro a1
State after:
case h.mpr
α : Type
R : RegExp α
cs : List α
a1 : cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
case h.mpr
α : Type
R : RegExp α
cs : List α
a1 : cs = [] ∨ ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
cases a1
State after:
case h.mpr.inl
α : Type
R : RegExp α
cs : List α
h✝ : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

case h.mpr.inr
α : Type
R : RegExp α
cs : List α
h✝ : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ left =>
  apply Exists.intro []
  simp
  simp only [left]
State after:
no goals

State before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ right =>
  apply Exists.elim right
  intro xs a2
  clear right
  cases a2
  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 ([xs] ++ ys)
      simp
      tauto
State after:
no goals

State before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.intro []
State after:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ (∀ r ∈ [], r ∈ RegExp.languageOf α R) ∧ [].join = cs

State before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ (∀ r ∈ [], r ∈ RegExp.languageOf α R) ∧ [].join = cs
Tactic:
simp
State after:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ [] = cs

State before:
α : Type
R : RegExp α
cs : List α
left : cs = []
⊢ [] = cs
Tactic:
simp only [left]
State after:
no goals

State before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.elim right
State after:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∀ (a : List α),
    (a ∈ RegExp.languageOf α R ∧ ∃ a_1, (∀ r ∈ a_1, r ∈ RegExp.languageOf α R) ∧ a ++ a_1.join = cs) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
⊢ ∀ (a : List α),
    (a ∈ RegExp.languageOf α R ∧ ∃ a_1, (∀ r ∈ a_1, r ∈ RegExp.languageOf α R) ∧ a ++ a_1.join = cs) →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
intro xs a2
State after:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs : List α
right : ∃ r ∈ RegExp.languageOf α R, ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ r ++ a.join = cs
xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
clear right
State after:
α : Type
R : RegExp α
cs xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2 : xs ∈ RegExp.languageOf α R ∧ ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
cases a2
State after:
case intro
α : Type
R : RegExp α
cs xs : List α
left✝ : xs ∈ RegExp.languageOf α R
right✝ : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
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 ([xs] ++ ys)
    simp
    tauto
State after:
no goals

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.elim a2_right
State after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
⊢ ∀ (a : List (List α)),
    (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs →
      ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
intro ys a3
State after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
a2_right : ∃ a, (∀ r ∈ a, r ∈ RegExp.languageOf α R) ∧ xs ++ a.join = cs
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
clear a2_right
State after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3 : (∀ r ∈ ys, r ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
cases a3
State after:
case intro
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
left✝ : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
right✝ : xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
case _ a3_left a3_right =>
  apply Exists.intro ([xs] ++ ys)
  simp
  tauto
State after:
no goals

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α R) ∧ rs.join = cs
Tactic:
apply Exists.intro ([xs] ++ ys)
State after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (∀ r ∈ [xs] ++ ys, r ∈ RegExp.languageOf α R) ∧ ([xs] ++ ys).join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (∀ r ∈ [xs] ++ ys, r ∈ RegExp.languageOf α R) ∧ ([xs] ++ ys).join = cs
Tactic:
simp
State after:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (xs ∈ RegExp.languageOf α R ∧ ∀ a ∈ ys, a ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs

State before:
α : Type
R : RegExp α
cs xs : List α
a2_left : xs ∈ RegExp.languageOf α R
ys : List (List α)
a3_left : ∀ r ∈ ys, r ∈ RegExp.languageOf α R
a3_right : xs ++ ys.join = cs
⊢ (xs ∈ RegExp.languageOf α R ∧ ∀ a ∈ ys, a ∈ RegExp.languageOf α R) ∧ xs ++ ys.join = cs
Tactic:
tauto
State after:
no goals