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

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

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

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

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

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

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

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]
State after:
α : Type
a : α
⊢ RegExp.languageOf α (RegExp.char a).delta =
    if False then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

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]
State after:
α : Type
a : α
⊢ ∅ = if False then {[]} else ∅

State before:
α : Type
a : α
⊢ ∅ = if False then {[]} else ∅
Tactic:
simp
State after:
no goals

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]
State after:
α : Type
⊢ RegExp.languageOf α RegExp.epsilon.delta =
    if True then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

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]
State after:
α : Type
⊢ {[]} = if True then {[]} else ∅

State before:
α : Type
⊢ {[]} = if True then {[]} else ∅
Tactic:
simp
State after:
no goals

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]
State after:
α : Type
⊢ RegExp.languageOf α RegExp.zero.delta =
    if False then RegExp.languageOf α RegExp.epsilon else RegExp.languageOf α RegExp.zero

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]
State after:
α : Type
⊢ ∅ = if False then {[]} else ∅

State before:
α : Type
⊢ ∅ = if False then {[]} else ∅
Tactic:
simp
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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