Theorem: Languages.thm_6 (FOL/Parsing/Text.lean)

State before:
α : Type
L : Language α
⊢ kleene_closure α L = {[]} ∪ concat L (kleene_closure α L)
Tactic:
apply Set.eq_of_subset_of_subset
State after:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ {[]} ∪ concat L (kleene_closure α L)

case a
α : Type
L : Language α
⊢ {[]} ∪ concat L (kleene_closure α L) ⊆ kleene_closure α L

State before:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp only [Set.subset_def]
State after:
case a
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ {[]} ∪ concat L (kleene_closure α L)

State before:
case a
α : Type
L : Language α
⊢ ∀ x ∈ kleene_closure α L, x ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
intro s a1
State after:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)

State before:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp only [thm_5 L] at a1
State after:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)

State before:
case a
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp at a1
State after:
case a
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)

State before:
case a
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
cases a1
State after:
case a.intro
α : Type
L : Language α
s : Str α
w✝ : ℕ
h✝ : s ∈ exp L w✝
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)

State before:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
case _ i a2 =>
  simp
  sorry
State after:
no goals

State before:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s ∈ {[]} ∪ concat L (kleene_closure α L)
Tactic:
simp
State after:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s = [] ∨ s ∈ concat L (kleene_closure α L)

State before:
α : Type
L : Language α
s : Str α
i : ℕ
a2 : s ∈ exp L i
⊢ s = [] ∨ s ∈ concat L (kleene_closure α L)
Tactic:
sorry
State after:
no goals

State before:
case a
α : Type
L : Language α
⊢ {[]} ∪ concat L (kleene_closure α L) ⊆ kleene_closure α L
Tactic:
simp only [Set.subset_def]
State after:
case a
α : Type
L : Language α
⊢ ∀ x ∈ {[]} ∪ concat L (kleene_closure α L), x ∈ kleene_closure α L

State before:
case a
α : Type
L : Language α
⊢ ∀ x ∈ {[]} ∪ concat L (kleene_closure α L), x ∈ kleene_closure α L
Tactic:
intro x a1
State after:
case a
α : Type
L : Language α
x : Str α
a1 : x ∈ {[]} ∪ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L

State before:
case a
α : Type
L : Language α
x : Str α
a1 : x ∈ {[]} ∪ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
simp at a1
State after:
case a
α : Type
L : Language α
x : Str α
a1 : x = [] ∨ x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L

State before:
case a
α : Type
L : Language α
x : Str α
a1 : x = [] ∨ x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
cases a1
State after:
case a.inl
α : Type
L : Language α
x : Str α
h✝ : x = []
⊢ x ∈ kleene_closure α L

case a.inr
α : Type
L : Language α
x : Str α
h✝ : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L

State before:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ x ∈ kleene_closure α L
Tactic:
case _ a1_left =>
  simp only [a1_left]
  exact kleene_closure.eps L
State after:
no goals

State before:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
case _ a1_right =>
  simp only [thm_5 L] at a1_right
  sorry
State after:
no goals

State before:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ x ∈ kleene_closure α L
Tactic:
simp only [a1_left]
State after:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ [] ∈ kleene_closure α L

State before:
α : Type
L : Language α
x : Str α
a1_left : x = []
⊢ [] ∈ kleene_closure α L
Tactic:
exact kleene_closure.eps L
State after:
no goals

State before:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (kleene_closure α L)
⊢ x ∈ kleene_closure α L
Tactic:
simp only [thm_5 L] at a1_right
State after:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (⋃ n, exp L n)
⊢ x ∈ kleene_closure α L

State before:
α : Type
L : Language α
x : Str α
a1_right : x ∈ concat L (⋃ n, exp L n)
⊢ x ∈ kleene_closure α L
Tactic:
sorry
State after:
no goals