internlm/Lean-Github huggingface dataset:
Theorem: language_of_delta
Proof state before:
case h.mp
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1 : ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
⊢ ∀ (a : List α),
    ((r.is_nullable ∧ a = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ a ++ s_1 = cs) →
      (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
intro xs a2
Proof state after:
case h.mp
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1 : ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
xs : List α
a2 : (r.is_nullable ∧ xs = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
case h.mp
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1 : ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
xs : List α
a2 : (r.is_nullable ∧ xs = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
clear a1
Proof state after:
case h.mp
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2 : (r.is_nullable ∧ xs = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
case h.mp
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2 : (r.is_nullable ∧ xs = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
cases a2
Proof state after:
case h.mp.intro
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
left✝ : r.is_nullable ∧ xs = []
right✝ : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left : r.is_nullable ∧ xs = []
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
case _ a2_left a2_right =>
  cases a2_left
  case _ a2_left_left a2_left_right =>
    apply Exists.elim a2_right
    intro ys a3
    clear a2_right
    cases a3
    case _ a3_left a3_right =>
      cases a3_left
      case _ a3_left_left a3_left_right =>
        simp only [a2_left_left]
        simp only [a3_left_left]
        simp only [a2_left_right] at a3_right
        simp only [a3_left_right] at a3_right
        simp at a3_right
        tauto
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left : r.is_nullable ∧ xs = []
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
cases a2_left
Proof state after:
case intro
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
left✝ : r.is_nullable
right✝ : xs = []
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
case _ a2_left_left a2_left_right =>
  apply Exists.elim a2_right
  intro ys a3
  clear a2_right
  cases a3
  case _ a3_left a3_right =>
    cases a3_left
    case _ a3_left_left a3_left_right =>
      simp only [a2_left_left]
      simp only [a3_left_left]
      simp only [a2_left_right] at a3_right
      simp only [a3_left_right] at a3_right
      simp at a3_right
      tauto
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
apply Exists.elim a2_right
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
⊢ ∀ (a : List α), (s.is_nullable ∧ a = []) ∧ xs ++ a = cs → (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
⊢ ∀ (a : List α), (s.is_nullable ∧ a = []) ∧ xs ++ a = cs → (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
intro ys a3
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3 : (s.is_nullable ∧ ys = []) ∧ xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_right : ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ xs ++ s_1 = cs
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3 : (s.is_nullable ∧ ys = []) ∧ xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
clear a2_right
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3 : (s.is_nullable ∧ ys = []) ∧ xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3 : (s.is_nullable ∧ ys = []) ∧ xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
cases a3
Proof state after:
case intro
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
left✝ : s.is_nullable ∧ ys = []
right✝ : xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left : s.is_nullable ∧ ys = []
a3_right : xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
case _ a3_left a3_right =>
  cases a3_left
  case _ a3_left_left a3_left_right =>
    simp only [a2_left_left]
    simp only [a3_left_left]
    simp only [a2_left_right] at a3_right
    simp only [a3_left_right] at a3_right
    simp at a3_right
    tauto
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left : s.is_nullable ∧ ys = []
a3_right : xs ++ ys = cs
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
cases a3_left
Proof state after:
case intro
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
left✝ : s.is_nullable
right✝ : ys = []
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
a3_left_left : s.is_nullable
a3_left_right : ys = []
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
case _ a3_left_left a3_left_right =>
  simp only [a2_left_left]
  simp only [a3_left_left]
  simp only [a2_left_right] at a3_right
  simp only [a3_left_right] at a3_right
  simp at a3_right
  tauto
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
a3_left_left : s.is_nullable
a3_left_right : ys = []
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
simp only [a2_left_left]
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
a3_left_left : s.is_nullable
a3_left_right : ys = []
⊢ (True ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
a3_left_left : s.is_nullable
a3_left_right : ys = []
⊢ (True ∧ s.is_nullable) ∧ cs = []
Tactic:
simp only [a3_left_left]
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
a3_left_left : s.is_nullable
a3_left_right : ys = []
⊢ (True ∧ True) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_right : xs ++ ys = cs
a3_left_left : s.is_nullable
a3_left_right : ys = []
⊢ (True ∧ True) ∧ cs = []
Tactic:
simp only [a2_left_right] at a3_right
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] ++ ys = cs
⊢ (True ∧ True) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] ++ ys = cs
⊢ (True ∧ True) ∧ cs = []
Tactic:
simp only [a3_left_right] at a3_right
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] ++ [] = cs
⊢ (True ∧ True) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] ++ [] = cs
⊢ (True ∧ True) ∧ cs = []
Tactic:
simp at a3_right
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] = cs
⊢ (True ∧ True) ∧ cs = []
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs xs : List α
a2_left_left : r.is_nullable
a2_left_right : xs = []
ys : List α
a3_left_left : s.is_nullable
a3_left_right : ys = []
a3_right : [] = cs
⊢ (True ∧ True) ∧ cs = []
Tactic:
tauto
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
case h.mpr
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = [] →
    ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Tactic:
intro a1
Proof state after:
case h.mpr
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1 : (r.is_nullable ∧ s.is_nullable) ∧ cs = []
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Theorem: language_of_delta
Proof state before:
case h.mpr
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1 : (r.is_nullable ∧ s.is_nullable) ∧ cs = []
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Tactic:
cases a1
Proof state after:
case h.mpr.intro
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
left✝ : r.is_nullable ∧ s.is_nullable
right✝ : cs = []
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1_left : r.is_nullable ∧ s.is_nullable
a2_right : cs = []
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Tactic:
case _ a1_left a2_right =>
  cases a1_left
  case _ a1_left_left a1_left_right =>
    simp only [a1_left_left]
    simp only [a1_left_right]
    simp
    simp only [a2_right]
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a1_left : r.is_nullable ∧ s.is_nullable
a2_right : cs = []
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Tactic:
cases a1_left
Proof state after:
case intro
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
left✝ : r.is_nullable
right✝ : s.is_nullable
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Tactic:
case _ a1_left_left a1_left_right =>
  simp only [a1_left_left]
  simp only [a1_left_right]
  simp
  simp only [a2_right]
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs
Tactic:
simp only [a1_left_left]
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ ∃ r, (True ∧ r = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r ++ s_1 = cs
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ ∃ r, (True ∧ r = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r ++ s_1 = cs
Tactic:
simp only [a1_left_right]
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ ∃ r, (True ∧ r = []) ∧ ∃ s, (True ∧ s = []) ∧ r ++ s = cs
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ ∃ r, (True ∧ r = []) ∧ ∃ s, (True ∧ s = []) ∧ r ++ s = cs
Tactic:
simp
Proof state after:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ [] = cs
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
s_ih : RegExp.languageOf α s.delta = if s.is_nullable then {[]} else ∅
cs : List α
a2_right : cs = []
a1_left_left : r.is_nullable
a1_left_right : s.is_nullable
⊢ [] = cs
Tactic:
simp only [a2_right]
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
e : RegExp α
a_ih✝ :
  RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α e.closure.delta =
    if e.closure.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
e : RegExp α
a_ih✝ :
  RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ {[]} = if e.closure.is_nullable then {[]} else ∅
Theorem: language_of_delta
Proof state before:
α : Type
e : RegExp α
a_ih✝ :
  RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ {[]} = if e.closure.is_nullable then {[]} else ∅
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
e : RegExp α
a_ih✝ :
  RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ {[]} = if True then {[]} else ∅
Theorem: language_of_delta
Proof state before:
α : Type
e : RegExp α
a_ih✝ :
  RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ {[]} = if True then {[]} else ∅
Tactic:
simp
Proof state after:
no goals
Theorem: derivative_def
Proof 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
Proof 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