internlm/Lean-Github huggingface dataset:
Theorem: is_nullable_def
Proof state before:
α : Type
r s : RegExp α
r_ih : r.is_nullable ↔ [] ∈ RegExp.languageOf α r
s_ih : s.is_nullable ↔ [] ∈ RegExp.languageOf α s
⊢ [] ∈ RegExp.languageOf α r ∧ s.is_nullable ↔ [] ∈ RegExp.languageOf α r ∧ [] ∈ RegExp.languageOf α s
Tactic:
simp only [s_ih]
Proof state after:
no goals
Theorem: is_nullable_def
Proof state before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α e.closure
Tactic:
simp only [equiv_language_of_closure]
Proof state after:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.epsilon.union (e.concat e.closure))
Theorem: is_nullable_def
Proof state before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔ [] ∈ RegExp.languageOf α (RegExp.epsilon.union (e.concat e.closure))
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
Theorem: is_nullable_def
Proof state before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ e.closure.is_nullable ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ True ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
Theorem: is_nullable_def
Proof state before:
α : Type
e : RegExp α
a_ih✝ : e.is_nullable ↔ [] ∈ RegExp.languageOf α e
⊢ True ↔
    [] ∈
      {[]} ∪
        {x |
          ∃ r ∈ RegExp.languageOf α e,
            ∃ s ∈ {l | ∃ rs, (∀ r ∈ rs, r ∈ RegExp.languageOf α e) ∧ rs.join = l}, r ++ s = x}
Tactic:
simp
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
e : RegExp α
⊢ RegExp.languageOf α e.delta =
    if e.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
induction e
Proof state after:
case char
α : Type
a✝ : α
⊢ RegExp.languageOf α (RegExp.char a✝).delta =
    if (RegExp.char a✝).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case epsilon
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if RegExp.epsilon.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case zero
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if RegExp.zero.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case union
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ :
  RegExp.languageOf α a✝¹.delta =
    if a✝¹.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
a_ih✝ :
  RegExp.languageOf α a✝.delta =
    if a✝.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (a✝¹.union a✝).delta =
    if (a✝¹.union a✝).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case concat
α : Type
a✝¹ a✝ : RegExp α
a_ih✝¹ :
  RegExp.languageOf α a✝¹.delta =
    if a✝¹.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
a_ih✝ :
  RegExp.languageOf α a✝.delta =
    if a✝.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (a✝¹.concat a✝).delta =
    if (a✝¹.concat a✝).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

case closure
α : Type
a✝ : RegExp α
a_ih✝ :
  RegExp.languageOf α a✝.delta =
    if a✝.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α a✝.closure.delta =
    if a✝.closure.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Theorem: language_of_delta
Proof state before:
α : Type
a : α
⊢ RegExp.languageOf α (RegExp.char a).delta =
    if (RegExp.char a).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
case char a =>
  simp only [RegExp.is_nullable]
  simp only [RegExp.languageOf]
  simp
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if RegExp.epsilon.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
case epsilon =>
  simp only [RegExp.is_nullable]
  simp only [RegExp.languageOf]
  simp
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if RegExp.zero.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
case zero =>
  simp only [RegExp.is_nullable]
  simp only [RegExp.languageOf]
  simp
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 RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
case union r s r_ih s_ih =>
  simp only [RegExp.languageOf] at r_ih
  simp only [RegExp.languageOf] at s_ih
  simp only [RegExp.languageOf]
  simp only [r_ih]
  simp only [s_ih]
  simp only [RegExp.is_nullable]
  ext cs
  simp
  tauto
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:
case closure e _ =>
  simp only [RegExp.languageOf]
  simp only [RegExp.is_nullable]
  simp
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
a : α
⊢ RegExp.languageOf α (RegExp.char a).delta =
    if (RegExp.char a).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
a : α
⊢ RegExp.languageOf α (RegExp.char a).delta =
    if False then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Theorem: language_of_delta
Proof state before:
α : Type
a : α
⊢ RegExp.languageOf α (RegExp.char a).delta =
    if False then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
a : α
⊢ ∅ = if False then {[]} else ∅
Theorem: language_of_delta
Proof state before:
α : Type
a : α
⊢ ∅ = if False then {[]} else ∅
Tactic:
simp
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if RegExp.epsilon.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if True then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Theorem: language_of_delta
Proof state before:
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if True then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
⊢ {[]} = if True then {[]} else ∅
Theorem: language_of_delta
Proof state before:
α : Type
⊢ {[]} = if True then {[]} else ∅
Tactic:
simp
Proof state after:
no goals
Theorem: language_of_delta
Proof state before:
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if RegExp.zero.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.is_nullable]
Proof state after:
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if False then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Theorem: language_of_delta
Proof state before:
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if False then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
Proof state after:
α : Type
⊢ ∅ = if False then {[]} else ∅
Theorem: language_of_delta
Proof state before:
α : Type
⊢ ∅ = if False then {[]} else ∅
Tactic:
simp
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 RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf] at r_ih
Proof state after:
α : Type
r s : RegExp α
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf] at s_ih
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 ∅
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
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 ∅
⊢ RegExp.languageOf α (r.union s).delta =
    if (r.union s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
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 ∅
⊢ RegExp.languageOf α r.delta ∪ RegExp.languageOf α s.delta = if (r.union s).is_nullable then {[]} else ∅
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 ∅
⊢ RegExp.languageOf α r.delta ∪ RegExp.languageOf α s.delta = if (r.union s).is_nullable then {[]} else ∅
Tactic:
simp only [r_ih]
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 ∅
⊢ (if r.is_nullable then {[]} else ∅) ∪ RegExp.languageOf α s.delta = if (r.union s).is_nullable then {[]} else ∅
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 ∅
⊢ (if r.is_nullable then {[]} else ∅) ∪ RegExp.languageOf α s.delta = if (r.union s).is_nullable then {[]} else ∅
Tactic:
simp only [s_ih]
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 ∅
⊢ ((if r.is_nullable then {[]} else ∅) ∪ if s.is_nullable then {[]} else ∅) =
    if (r.union s).is_nullable then {[]} else ∅
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 ∅
⊢ ((if r.is_nullable then {[]} else ∅) ∪ if s.is_nullable then {[]} else ∅) =
    if (r.union s).is_nullable then {[]} else ∅
Tactic:
simp only [RegExp.is_nullable]
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 ∅
⊢ ((if r.is_nullable then {[]} else ∅) ∪ if s.is_nullable then {[]} else ∅) =
    if r.is_nullable ∨ s.is_nullable then {[]} else ∅
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 ∅
⊢ ((if r.is_nullable then {[]} else ∅) ∪ if s.is_nullable then {[]} else ∅) =
    if r.is_nullable ∨ s.is_nullable then {[]} else ∅
Tactic:
ext cs
Proof state after:
case h
α : 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 α
⊢ (cs ∈ (if r.is_nullable then {[]} else ∅) ∪ if s.is_nullable then {[]} else ∅) ↔
    cs ∈ if r.is_nullable ∨ s.is_nullable then {[]} else ∅
Theorem: language_of_delta
Proof state before:
case h
α : 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 α
⊢ (cs ∈ (if r.is_nullable then {[]} else ∅) ∪ if s.is_nullable then {[]} else ∅) ↔
    cs ∈ if r.is_nullable ∨ s.is_nullable then {[]} else ∅
Tactic:
simp
Proof state after:
case h
α : 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 ∧ cs = [] ∨ s.is_nullable ∧ cs = [] ↔ (r.is_nullable ∨ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
case h
α : 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 ∧ cs = [] ∨ s.is_nullable ∧ cs = [] ↔ (r.is_nullable ∨ s.is_nullable) ∧ cs = []
Tactic:
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 RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf] at r_ih
Proof state after:
α : Type
r s : RegExp α
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Theorem: language_of_delta
Proof state before:
α : Type
r s : RegExp α
s_ih :
  RegExp.languageOf α s.delta =
    if s.is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
r_ih : RegExp.languageOf α r.delta = if r.is_nullable then {[]} else ∅
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf] at s_ih
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 ∅
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
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 ∅
⊢ RegExp.languageOf α (r.concat s).delta =
    if (r.concat s).is_nullable then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero
Tactic:
simp only [RegExp.languageOf]
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 ∅
⊢ {x | ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α s.delta, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
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 ∅
⊢ {x | ∃ r_1 ∈ RegExp.languageOf α r.delta, ∃ s_1 ∈ RegExp.languageOf α s.delta, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
Tactic:
simp only [r_ih]
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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ RegExp.languageOf α s.delta, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ RegExp.languageOf α s.delta, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
Tactic:
simp only [s_ih]
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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} =
    if (r.concat s).is_nullable then {[]} else ∅
Tactic:
simp only [RegExp.is_nullable]
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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} =
    if r.is_nullable ∧ s.is_nullable then {[]} else ∅
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 ∅
⊢ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} =
    if r.is_nullable ∧ s.is_nullable then {[]} else ∅
Tactic:
ext cs
Proof state after:
case h
α : 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 α
⊢ cs ∈ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} ↔
    cs ∈ if r.is_nullable ∧ s.is_nullable then {[]} else ∅
Theorem: language_of_delta
Proof state before:
case h
α : 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 α
⊢ cs ∈ {x | ∃ r_1 ∈ if r.is_nullable then {[]} else ∅, ∃ s_1 ∈ if s.is_nullable then {[]} else ∅, r_1 ++ s_1 = x} ↔
    cs ∈ if r.is_nullable ∧ s.is_nullable then {[]} else ∅
Tactic:
simp
Proof state after:
case h
α : 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_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs) ↔
    (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Theorem: language_of_delta
Proof state before:
case h
α : 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_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs) ↔
    (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
constructor
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 α
⊢ (∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs) →
    (r.is_nullable ∧ s.is_nullable) ∧ cs = []

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
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 α
⊢ (∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ s_1 = cs) →
    (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
intro 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 : List α
a1 : ∃ r_1, (r.is_nullable ∧ r_1 = []) ∧ ∃ s_1, (s.is_nullable ∧ s_1 = []) ∧ r_1 ++ 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
⊢ (r.is_nullable ∧ s.is_nullable) ∧ cs = []
Tactic:
apply Exists.elim 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 : 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 = []