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

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

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

State before:
α : Type
L : Language α
s : Str α
a1 : s ∈ kleene_closure α L
⊢ s ∈ ⋃ n, exp L n
Tactic:
induction a1
State after:
case eps
α : Type
L : Language α
s : Str α
⊢ [] ∈ ⋃ n, exp L n

case succ
α : Type
L : Language α
s s✝ t✝ : Str α
a✝¹ : s✝ ∈ kleene_closure α L
a✝ : t✝ ∈ L
a_ih✝ : s✝ ∈ ⋃ n, exp L n
⊢ s✝ ++ t✝ ∈ ⋃ n, exp L n

State before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ ⋃ n, exp L n
Tactic:
case eps =>
  simp
  apply Exists.intro 0
  simp only [exp]
  simp
State after:
no goals

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

State before:
α : Type
L : Language α
s : Str α
⊢ ∃ i, [] ∈ exp L i
Tactic:
apply Exists.intro 0
State after:
α : Type
L : Language α
s : Str α
⊢ [] ∈ exp L 0

State before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ exp L 0
Tactic:
simp only [exp]
State after:
α : Type
L : Language α
s : Str α
⊢ [] ∈ {[]}

State before:
α : Type
L : Language α
s : Str α
⊢ [] ∈ {[]}
Tactic:
simp
State after:
no goals

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : xs ∈ ⋃ n, exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
simp at ih_3
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ xs ++ ys ∈ ⋃ n, exp L n

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
apply Exists.elim ih_3
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ ∀ (a : ℕ), xs ∈ exp L a → xs ++ ys ∈ ⋃ n, exp L n

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
⊢ ∀ (a : ℕ), xs ∈ exp L a → xs ++ ys ∈ ⋃ n, exp L n
Tactic:
intro n a2
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
ih_3 : ∃ i, xs ∈ exp L i
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
clear ih_3
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ ⋃ n, exp L n
Tactic:
simp
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ i, xs ++ ys ∈ exp L i

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ i, xs ++ ys ∈ exp L i
Tactic:
apply Exists.intro (n + 1)
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ exp L (n + 1)

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ exp L (n + 1)
Tactic:
simp only [exp]
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ concat (exp L n) L

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ concat (exp L n) L
Tactic:
simp only [concat]
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ++ ys ∈ {x | ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = x}
Tactic:
simp
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = xs ++ ys

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ s ∈ exp L n, ∃ t ∈ L, s ++ t = xs ++ ys
Tactic:
apply Exists.intro xs
State after:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = xs ++ ys

State before:
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n ∧ ∃ t ∈ L, xs ++ t = xs ++ ys
Tactic:
constructor
State after:
case left
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n

case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ t ∈ L, xs ++ t = xs ++ ys

State before:
case left
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ xs ∈ exp L n
Tactic:
exact a2
State after:
no goals

State before:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ∃ t ∈ L, xs ++ t = xs ++ ys
Tactic:
apply Exists.intro ys
State after:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L ∧ xs ++ ys = xs ++ ys

State before:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L ∧ xs ++ ys = xs ++ ys
Tactic:
simp
State after:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L

State before:
case right
α : Type
L : Language α
s xs ys : Str α
a✝ : xs ∈ kleene_closure α L
ih_2 : ys ∈ L
n : ℕ
a2 : xs ∈ exp L n
⊢ ys ∈ L
Tactic:
exact ih_2
State after:
no goals