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

State before:
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L
Tactic:
simp only [Set.subset_def]
State after:
α : Type
L : Language α
⊢ ∀ x ∈ ⋃ n, exp L n, x ∈ kleene_closure α L

State before:
α : Type
L : Language α
⊢ ∀ x ∈ ⋃ n, exp L n, x ∈ kleene_closure α L
Tactic:
intro s a1
State after:
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : s ∈ ⋃ n, exp L n
⊢ s ∈ kleene_closure α L
Tactic:
simp at a1
State after:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ s ∈ kleene_closure α L
Tactic:
apply Exists.elim a1
State after:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ ∀ (a : ℕ), s ∈ exp L a → s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
⊢ ∀ (a : ℕ), s ∈ exp L a → s ∈ kleene_closure α L
Tactic:
intro n a2
State after:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
n : ℕ
a2 : s ∈ exp L n
⊢ s ∈ kleene_closure α L

State before:
α : Type
L : Language α
s : Str α
a1 : ∃ i, s ∈ exp L i
n : ℕ
a2 : s ∈ exp L n
⊢ s ∈ kleene_closure α L
Tactic:
exact Set.mem_of_subset_of_mem (thm_4 L n) a2
State after:
no goals