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

State before:
α : Type u_1
⊢ univ = (Σ)∗
Tactic:
apply Set.ext
State after:
case h
α : Type u_1
⊢ ∀ (x : Word α), x ∈ univ ↔ x ∈ (Σ)∗

State before:
case h
α : Type u_1
⊢ ∀ (x : Word α), x ∈ univ ↔ x ∈ (Σ)∗
Tactic:
intro w
State after:
case h
α : Type u_1
w : Word α
⊢ w ∈ univ ↔ w ∈ (Σ)∗

State before:
case h
α : Type u_1
w : Word α
⊢ w ∈ univ ↔ w ∈ (Σ)∗
Tactic:
constructor
State after:
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗

case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ

State before:
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗

case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Tactic:
. intros; exact Sigma.kleene_contains_all w
State after:
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ

State before:
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Tactic:
. intros; simp [Language.univ, Set.mem_univ]
State after:
no goals

State before:
case h.mp
α : Type u_1
w : Word α
⊢ w ∈ univ → w ∈ (Σ)∗
Tactic:
intros
State after:
case h.mp
α : Type u_1
w : Word α
a✝ : w ∈ univ
⊢ w ∈ (Σ)∗

State before:
case h.mp
α : Type u_1
w : Word α
a✝ : w ∈ univ
⊢ w ∈ (Σ)∗
Tactic:
exact Sigma.kleene_contains_all w
State after:
no goals

State before:
case h.mpr
α : Type u_1
w : Word α
⊢ w ∈ (Σ)∗ → w ∈ univ
Tactic:
intros
State after:
case h.mpr
α : Type u_1
w : Word α
a✝ : w ∈ (Σ)∗
⊢ w ∈ univ

State before:
case h.mpr
α : Type u_1
w : Word α
a✝ : w ∈ (Σ)∗
⊢ w ∈ univ
Tactic:
simp [Language.univ, Set.mem_univ]
State after:
no goals