Theorem: Language.kleene_eq_plus_eps (FormalSystems/Preliminaries/Language.lean)

State before:
α : Type u_1
L : Language α
⊢ L⁺ ∪ {ε} = L∗
Tactic:
apply Set.ext
State after:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ L⁺ ∪ {ε} ↔ x ∈ L∗

State before:
case h
α : Type u_1
L : Language α
⊢ ∀ (x : Word α), x ∈ L⁺ ∪ {ε} ↔ x ∈ L∗
Tactic:
intro w
State after:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} ↔ w ∈ L∗

State before:
case h
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} ↔ w ∈ L∗
Tactic:
constructor
State after:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}

State before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗

case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Tactic:
. intro
  | Or.inl h =>
    cases h with
    | intro n r =>
      exists n
      exact r.right
  | Or.inr e => exists 0
State after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}

State before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Tactic:
. simp [KStar.kstar]
  intro
  | Exists.intro nn r =>
    cases nn with
    | succ m =>
      apply Or.inl
      unfold Language.plus
      exists (Nat.succ m)
      exact ⟨Nat.succ_ne_zero m, r⟩
    | zero =>
      apply Or.inr
      exact r
State after:
no goals

State before:
case h.mp
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L⁺ ∪ {ε} → w ∈ L∗
Tactic:
intro
| Or.inl h =>
  cases h with
  | intro n r =>
    exists n
    exact r.right
| Or.inr e => exists 0
State after:
no goals

State before:
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
h : w ∈ L⁺
⊢ w ∈ L∗
Tactic:
cases h with
| intro n r =>
  exists n
  exact r.right
State after:
no goals

State before:
case intro
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
n : ℕ
r : ¬n = 0 ∧ w ∈ L ^ n
⊢ w ∈ L∗
Tactic:
exists n
State after:
case intro
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
n : ℕ
r : ¬n = 0 ∧ w ∈ L ^ n
⊢ w ∈ L ^ n

State before:
case intro
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
n : ℕ
r : ¬n = 0 ∧ w ∈ L ^ n
⊢ w ∈ L ^ n
Tactic:
exact r.right
State after:
no goals

State before:
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ L⁺ ∪ {ε}
e : w ∈ {ε}
⊢ w ∈ L∗
Tactic:
exists 0
State after:
no goals

State before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ L∗ → w ∈ L⁺ ∪ {ε}
Tactic:
simp [KStar.kstar]
State after:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ kstar L → w ∈ L⁺ ∪ {ε}

State before:
case h.mpr
α : Type u_1
L : Language α
w : Word α
⊢ w ∈ kstar L → w ∈ L⁺ ∪ {ε}
Tactic:
intro
| Exists.intro nn r =>
  cases nn with
  | succ m =>
    apply Or.inl
    unfold Language.plus
    exists (Nat.succ m)
    exact ⟨Nat.succ_ne_zero m, r⟩
  | zero =>
    apply Or.inr
    exact r
State after:
no goals

State before:
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
nn : ℕ
r : (fun n => w ∈ L ^ n) nn
⊢ w ∈ L⁺ ∪ {ε}
Tactic:
cases nn with
| succ m =>
  apply Or.inl
  unfold Language.plus
  exists (Nat.succ m)
  exact ⟨Nat.succ_ne_zero m, r⟩
| zero =>
  apply Or.inr
  exact r
State after:
no goals

State before:
case succ
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺ ∪ {ε}
Tactic:
apply Or.inl
State after:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺

State before:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ L⁺
Tactic:
unfold Language.plus
State after:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ fun w => ∃ n, ¬n = 0 ∧ w ∈ L ^ n

State before:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ w ∈ fun w => ∃ n, ¬n = 0 ∧ w ∈ L ^ n
Tactic:
exists (Nat.succ m)
State after:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ ¬Nat.succ m = 0 ∧ w ∈ L ^ Nat.succ m

State before:
case succ.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
m : ℕ
r : w ∈ L ^ Nat.succ m
⊢ ¬Nat.succ m = 0 ∧ w ∈ L ^ Nat.succ m
Tactic:
exact ⟨Nat.succ_ne_zero m, r⟩
State after:
no goals

State before:
case zero
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
r : w ∈ L ^ Nat.zero
⊢ w ∈ L⁺ ∪ {ε}
Tactic:
apply Or.inr
State after:
case zero.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
r : w ∈ L ^ Nat.zero
⊢ w ∈ {ε}

State before:
case zero.h
α : Type u_1
L : Language α
w : Word α
x✝ : w ∈ kstar L
r : w ∈ L ^ Nat.zero
⊢ w ∈ {ε}
Tactic:
exact r
State after:
no goals