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

State before:
α : Type
L : Language α
⊢ kleene_closure α L = ⋃ n, exp L n
Tactic:
apply Set.eq_of_subset_of_subset
State after:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ ⋃ n, exp L n

case a
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L

State before:
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ ⋃ n, exp L n
Tactic:
exact thm_5_right L
State after:
no goals

State before:
case a
α : Type
L : Language α
⊢ ⋃ n, exp L n ⊆ kleene_closure α L
Tactic:
exact thm_5_left L
State after:
no goals