Theorem: Language.Sigma.kleene_contains_all (FormalSystems/Preliminaries/Language.lean)

State before:
α : Type u_1
⊢ [] ∈ (Σ)∗
Tactic:
exists 0
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
⊢ x :: xs ∈ (Σ)∗
Tactic:
have ⟨n, hn⟩ := Sigma.kleene_contains_all xs
State after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ)∗

State before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ)∗
Tactic:
exists (1 + n)
State after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) ^ (1 + n)

State before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) ^ (1 + n)
Tactic:
simp [pow_add]
State after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) * (Σ) ^ n

State before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ x :: xs ∈ (Σ) * (Σ) ^ n
Tactic:
exists [x]
State after:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ ∃ v, [x] ∈ (Σ) ∧ v ∈ (Σ) ^ n ∧ x :: xs = [x] * v

State before:
α : Type u_1
x : α
xs : List α
n : ℕ
hn : xs ∈ (Σ) ^ n
⊢ ∃ v, [x] ∈ (Σ) ∧ v ∈ (Σ) ^ n ∧ x :: xs = [x] * v
Tactic:
exists xs
State after:
no goals