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

State before:
α : Type u_1
⊢ ∀ (L : Language α), L ⊆ (Σ)∗
Tactic:
intro _ w _
State after:
α : Type u_1
L✝ : Language α
w : Word α
a✝ : w ∈ L✝
⊢ w ∈ (Σ)∗

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